米澤研究室 全体ミーティング 2010/12/22 M2 渡邊裕貴
研究内容 型システムによる CPS 変換の検証 型を使って項の semantics を表す From λ→ to λ≤{} From λP to ?
CPS 変換 継続を受け取って評価結果を継続に渡す ように項を変換する [[x]] = λk. k x [[λx. t]] = λk. k (λx. [[t]]) [[t1 t2]] = λk. [[t1]] (λv1. v1[[t2]] k) call-by-name [[t1 t2]] = λk. [[t1]] (λv1. [[t2]] (λv2. v1 v2 k)) call-by-value G.D. Plotkin. “Call-by-name, call-by-value and the lambda-calculus.” 1975
[[Γ]] ⊢ [[t]] : ([[T]] → ⊥) → ⊥ 何を証明するのか? CPS 変換前の項が型付けされているなら 変換後の項も必ず型付けされること If Γ ⊢ t : T then [[Γ]] ⊢ [[t]] : ([[T]] → ⊥) → ⊥
やろうとしていたこと 依存型付きラムダ計算の CPS 変換における型付けの保存の証明 Call-by-name の場合は既に証明されている G. Barthe, et al. “CPS Translations and Applications: The Cube and Beyond.” 1999. Call-by-value の場合を証明したい
⊢ natlist 2 ≡ natlist ((λx. x + 1) 1) 依存型付きラムダ計算 型の中に項が現れる ⊢ (100 :: 200 :: []) : natlist 2 型に対する型付けを行う ⊢ natlist :: nat → type 型の等価性の判定を行う ⊢ natlist 2 ≡ natlist ((λx. x + 1) 1) 項の型付けと型の型付けが 相互再帰的に定義される
うまくいかない…… [[Γ]], k : [[T[x ↦ t]]] → ⊥, … ⊢ k : [[T]][x ↦ v] → ⊥ ⋮ v = t ? [[Γ]], k : [[T[x ↦ t]]] → ⊥, … ⊢ k : [[T]][x ↦ v] → ⊥ ⋮ [[Γ]] ⊢ [[f t]] : ([[T[x ↦ t]]] → ⊥) → ⊥
Singleton Types 項を具体的に指定できる型 ⊢ 1+3 : {4 : Nat} ⊢ 1+3 : Nat ⊢ λn. n+1 : Πn:Nat. {n+1 : Nat} ⊢ λn. n+1 : Nat → Nat ⊢ λn. n+1 : Πn:{3 : Nat}. {4 : Nat} ⊢ λn. n+1 : Nat → Nat D. Aspinall. “Subtyping with singleton types.” 1995
[[Γ]] ⊢ [[t]] : ({[[t]] (λx. x) : [[T]]} → ⊥) → ⊥ 証明する命題を変更 継続が受け取る値を singleton type によって表わす If Γ ⊢ t : T then [[Γ]] ⊢ [[t]] : ({[[t]] (λx. x) : [[T]]} → ⊥) → ⊥
関数の戻り値を singleton type で表したい しかし自己言及的な型が必要 これまでの規則では型付けできない…… f : Πx:Nat. {f x : Nat} 関数の戻り値を singleton type で表したい