TaPL輪講/9章
単純型付きラムダ計算
9.1 関数型
9.2 型判断
変数束縛のことを考える必要がある
文脈(型環境)Γは変数と型のペアの列
9.2.1 演習
基底型のない純粋な単純型付きラムダ計算にはwell-typedな項がない→なぜ?
→基底型がないと型の集合が空になるから。へ~
9.2.2 演習
型導出の木をかけ
9.2.3 演習
項f x yが型Boolをもつような文脈Γを見つけよ
Γ=f:Bool->Bool->Bool, x:Bool, y:Bool
そのような全ての文脈の集合を簡潔に表すことができるか?
$ f:T \rightarrow U \rightarrow Bool, x:T, y:U
9.3 型付けの性質
ここからBoolの入ったlambda calculusについて論じている
9.3.1 補題
型付け関係に関するinversion
9.3.2 演習
Γ |- x x : T となるようなΓとTは存在するか?
存在するなら与えて導出木をかき、存在しないなら証明せよ
→存在しない
(証明)
背理法で示す
いまそのようなΓとTがあると仮定する
すると補題9.3.1.3よりある型T11があって Γ |- x : T11 -> T かつ Γ |- x : T11 となる
これらが両方成り立つには T11 = T11 -> T でなければならない
ところがそのようなT11は無限の長さの関数型となり不適(ほんとうに?)
よって背理法よりそのようなΓとTは存在しない
9.3.3 定理
型の一意性
文脈Γを与えると、(自由変数が全てdom(Γ)に入っている)項tは高々1つの型をもつ
項がtypableならばその型は一意である
型導出は一意
(証明)
$ \forall \Gamma, t, T_1, T_2. \Gamma \vdash t : T_1 \land \Gamma \vdash t : T_2 \Rightarrow T_1 = T_2 を示すとよさそう
$ \Gamma \vdash t : T_1 の導出に関する帰納法
(T-Var の場合)
t = xの形になる
補題9.3.1.1よりx:T1 ∈ Γ
同様にx:T2 ∈ Γ
Γ(x)=T1かつΓ(x)=T2よりT1=T2
よってT-Varの場合に示された
(T-Abs の場合)
t = λx:T'.t' の形になる
IH: 任意のTについて Γ, x:T' |- t' : T ならば T1=T
仮定よりΓ | -λx:T'.t' : T1 かつ Γ | -λx:T'.t' : T2
補題9.3.1.2よりあるR1があってT1=T'->R1かつΓ,x:T' |- t' : R1
同様にあるR2があってT2=T'->R2かつΓ,x:T' |- t' : R2
IHを適用してR1=R2
よってT1=T'->R1=T'->R2=T2
よってT-Absの場合に示された
(T-Appの場合)
t = t1 t2 の形になる
IH1: 任意のTについてΓ |- t1 : T ならば T11 -> T12 = T
IH2: 任意のTについてΓ |- t2 : T ならば T11 = T
仮定よりΓ |- t1 t2 : T1 かつ Γ |- t1 t2 : T2
ワニャー
なんやかんやするとできる
(T-True, T-Falseの場合)
すぐわかる
(T-Ifの場合)
t = if t1 then t2 else t3 の形になる
Γ |- if t1 then t2 else t3 : T1
補題より
Γ |- t1 : Bool
Γ |- t2 : T1
Γ |- t3 : T1
IH1: 任意のTについてΓ |- t1 : Bool ならば Bool = T
IH2: 任意のTについてΓ |- t2 : T1 ならば T1 = T
IH3: 任意のTについてΓ |- t3 : T1 ならば T1 = T
ワニャーとやるとできる
Coqではできた、信じてくれ!!!!
9.3.4 補題
1. Γ |- v : Bool かつvは値 ならば v = true または v = false
2. Γ |- v : T1 -> T2 かつvは値 ならば あるt2が存在して v = λx:T1. t2
(証明)
vが値であることについて場合分けすればよさそう
9.3.5 定理
|- t : T ならばtは値もしくはあるt'があって t -> t'
(証明)
|- t : T の導出に関する帰納法
(T-Varの場合)
ありえない
(T-Absの場合)
t = λx:T1. t2 の形をしている
このtは明らかに値
よって(T-Abs)の場合にいえた
(T-Appの場合)
t = t1 t2 の形をしている
H: |- t1 t2 : T
補題9.3.1.3よりあるT11があって
|- t1 : T11 -> T
|- t2 : T11
IH1: (|- t1 : T11 -> T ならば) t1は値もしくはあるt1'があって t1 -> t1'
IH2: (|- t2 : T11 ならば) t2は値もしくはあるt2'があって t2 -> t2'
IH1について場合分け
(t1が値の場合)
補題9.3.4.2よりt1はlambda abstractionの形をしている
よって(E-AppAbs)が適用できる
さらにIH2について場合分け
(t2が値の場合)
規則(E-AppAbs)が適用できる
(あるt2'があってt2 -> t2'の場合)
規則(E-App2)が適用できる
(IH2の場合分け終了)
(あるt1'があってt1 -> t1'の場合)
規則(E-App1)が適用できる
(IH1の場合分け終了)
よって(T-App)の場合にいえた
(証明終了)
次は型保存を示そうね
9.3.6 補題
Γ |- t : T かつΔがΓの順列であるならばΔ |- t : T
(証明)
Γ |- t : Tの導出に関する帰納法
(T-Varの場合)
t = x
Γ |- x : T
Γ(x) = T
ΔはΓの順列なのでΔ(x) = T
よって Δ |- t : T
(T-Absの場合)
t = λx:T1. t2
Γ |- λx:T1. t2 : T1 -> T2
IH: (Γ |- t2 : T2 かつ)ΔがΓの順列であるならばΔ |- t2 : T2
これはすぐわかる
(T-Appの場合)
t = t1 t2
Γ |- t1 t2 : T2
Γ |- t1 : T1 -> T2
Γ |- t2 : T1
IH1: Γ |- t1 : T1 -> T2 かつ ΔがΓの順列であるならばΔ |- t1 : T1 -> T2
IH2: Γ |- t2 : T1 かつ ΔがΓの順列であるならばΔ |- t2 : T1
これもすぐわかる
はい
(T-True, T-Falseの場合)
すぐわかる
(T-Ifの場合)
これも多分すぐわかる
9.3.7 補題
Γ |- t : T かつ x /∈ dom(Γ) ならば Γ, x:S |- t : T
さらにどちらも導出の深さは同じ
(証明)
補題A: x /∈ dom(Γ) かつ x≠y ならば x /∈ dom(Γ, y:T)
(補題Aの証明)
対偶を示す
x ∈ dom(Γ, y:T) ならば x ∈ dom(Γ) または x=y
これは明らかでは?
Γ |- t : Tの導出に関する帰納法
(T-Varの場合)
t = y (≠x)
y, T∈Γ
補題Aより y, T∈(Γ, x:S)
よって Γ, x:S |- t : T
以上よりT-Varの場合にいえた
(T-Absの場合)
t = λy:T1. t2
Γ |- λy:T1. t2 : T1 -> T2
H1: x /∈ dom(Γ)
H2: Γ, y:T1 |- t2 : T2
Goal: Γ, x:S |- λy:T1. t2 : T1 -> T2
IH: Γ, y:T1 |- t2 : T2 かつ x /∈ dom(Γ, y:T1) ならば Γ, y:T1, x:S |- t2 : T2
H1, H2と補題AからIHが使える
Γ, y:T1, x:S |- t2 : T2
補題9.3.6からΓ, x:S, y:T1 |- t2 : T2
(T-Abs)を適用してΓ, x:S |- λy:T1.t2 : T1 -> T2
以上よりT-Absの場合にいえた
(T-Appの場合)
t = t1 t2
Γ |- t1 t2 : T2
H: x /∈ dom(Γ)
H1: Γ |- t1 : T1 -> T2
H2: Γ |- t2 : T1
IH1: Γ |- t1 : T1 -> T2 かつ x /∈ dom(Γ) ならば Γ, x:S |- t1 : T1 -> T2
IH2: Γ |- t2 : T1 かつ x /∈ dom(Γ) ならば Γ, x:S |- t2 : T1
IH1とIH2に(T-App)を適用していえる
(T-True, T-Falseの場合)
すぐわかる
(T-Ifの場合)
t = if t1 then t2 else t3
H: x /∈ dom(Γ)
H1: Γ |- t1 : Bool
H2: Γ |- t2 : T
H3: Γ |- t3 : T
IH1: Γ |- t1 : Bool かつ x /∈ dom(Γ) ならば Γ, x:S |- t1 : Bool
IH2: Γ |- t2 : T かつ x /∈ dom(Γ) ならば Γ, x:S |- t2 : T
IH3: Γ |- t3 : T かつ x /∈ dom(Γ) ならば Γ, x:S |- t3 : T
H, H1, H2, H3, IH1, IH2, IH3, T-Ifよりわかる
以上よりOK
9.3.8 補題
Γ, x:S |- t : T かつ Γ |- s : S ならば Γ |- (x |-> s)t : T
(証明)
Γ, x:S |- t : Tの導出に関する帰納法
(T-Varの場合)
t = y
Γ, x:S |- y : T
y : T ∈ (Γ, x:S)
H: Γ |- s : S
Goal: Γ |- (x |-> s)y : T
yについて場合分け
(x = yの場合)
(x |-> s)x = x
ところでこのときS = TなのでΓ |- (x |-> s)x : T
(x <> yの場合)
(x |-> s)y = y
なのでただちに Γ |- (x |-> s)x : T
よってT-Varの場合にいえた
(T-Absの場合)
t = λy:T1. t2
Γ, x:S |- λy:T1.t2 : T1 -> T2
Goal: Γ |- (x |-> s)(λy:T1.t2) : T1 -> T2
H0: Γ |- s : S
H1: Γ, x:S, y:T1 |- t2 : T2
補題9.3.6を適用して並べかえてた
IH: Γ, x:S, y:T1 |- t2 : T2 かつ Γ, y:T1 |- s : S ならば Γ, y:T1 |- (x |-> s)t2 : T2
α変換を適切に行うことで(x |-> s)(λy:T1.t2) = λy:T1.(x |-> s)t2 とできる
以下ではsubstitutionができるものとする
(x |-> s)(λy:T1.t2) が定義できるのはy ≠ x かつ y /∈ FV(s)の場合のみ
これは規約5.3.4からy<>xかつy/∈FV(s)としてよいことからいいらしい
いまy /∈ dom(Γ) なのでH0と補題9.3.7よりΓ, y:T1 |- s : S
これとH1, IHより Γ, y:T1 |- (x |-> s)t2 : T2
(T-Abs) より Γ |- λy:T1.(x |-> s)t2 : T1 -> T2
substitutionを引き戻して Γ |- (x |-> s)(λy:T1.t2) : T1 -> T2
よってT-Absの場合にいえた
(T-Appの場合)
t = t1 t2
Γ, x:S |- t1 t2 : T2
Goal: Γ |- (x |-> s)(t1 t2) : T2
H0: Γ |- s : S
H1: Γ, x:S |- t1 : T1 -> T2
H2: Γ, x:S |- t2 : T1
IH1: Γ, x:S |- t1 : T1 -> T2 かつ Γ |- s : S ならば Γ |- (x |-> s)t1 : T1 -> T2
IH2: Γ, x:S |- t2 : T1 かつ Γ |- s : S ならば Γ |- (x |-> s)t2 : T1
H0, H1, IH1よりΓ |- (x |-> s)t1 : T1 -> T2
H0, H2, IH2よりΓ |- (x |-> s)t2 : T1
(T-App)より
Γ |- ((x |-> s)t1)((x |-> s)t2) : T2
substitutionを引き戻してΓ |- (x |-> s)(t1 t2) : T2
よってT-Appの場合にいえた
(T-True, T-Falseの場合)
すぐわかる
(T-Ifの場合)
t = if t1 then t2 else t3
Γ, x:S |- if t1 then t2 else t3 : T
Goal: Γ |- (x |-> s)(if t1 then t2 else t3) : T
H0: Γ |- s : S
H1: Γ, x:S |- t1 : Bool
H2 : Γ, x:S |- t2 : T
H3 : Γ, x:S |- t3 : T
IH1: Γ, x:S |- t1 : Bool かつ Γ |- s : S ならば Γ |- (x |-> s)t1 : Bool
IH2: Γ, x:S |- t2 : T かつ Γ |- s : S ならば Γ |- (x |-> s)t2 : T
IH3: Γ, x:S |- t3 : T かつ Γ |- s : S ならば Γ |- (x |-> s)t3 : T
H0, H1, H2, H3, IH1, IH2, IH3を組み合わせてT-Ifを適用するといえる
以上よりOK
9.3.9 定理
型保存
Γ |- t : T かつ t -> t' ならば Γ |- t' : T
(証明) 演習
9.3.10 演習
演習8.3.6で型つき算術式のsubject expansion性について調べた
tが条件分岐を含まないとして t -> t' かつ Γ |- t' : T ならば Γ |- t : T と常にいってよいか?
いえない気がする
t = (λx.xx)(λx.x)
t' = (λx.x)(λx.x)
これは Γ |- t' : T->T だがtはill-typedでは?
ほんとうに?
→解答見た
t = (λx:Bool. λy:Bool. y)(true true)
t' = (λy:Bool. y)
について確かにt -> t' かつ Γ |- t' : Bool -> Bool だがtはill-typed
9.4 カリーハワード対応
9.4.1 演習
図8-1のBoolの規則のうちどれが導入規則/除去規則に対応しているか?
導入規則は (T-True)と(T-False)
除去規則は (T-If)
図8-2のNatの規則についてはどうか?
導入規則は (T-Zero)と(T-Succ)と(T-Pred)
除去規則は (T-IsZero)と(T-Succ)と(T-Pred)
9.5 (型)消去とtypability
9.5.1 定義
型つき項を型なし項に変換する関数 erase
9.5.2 定理
1. 型つきの評価規則において t -> t' ならば erase(t) -> erase(t')
2. 型つきの評価規則において erase(t) -> m' ならば、ある単純型付きの項t'があって t -> t' かつ erase(t') = m' となる
(証明)
評価規則に関する帰納法
補題B: erase((x |-> s)t) = (x |-> erase(s)) (erase (t))
(補題Bの証明)
tの構造に関する帰納法
(t = yの場合)
(subcase: y = xの場合)
erase((x |-> s)y) = erase(s)
(x |-> erase(s)) (erase(y)) = (x |-> erase(s)) y = erase(s)
よっていえた
(subcase: y <> xの場合)
erase((x |-> s)y) = erase(y) = y
(x |-> erase(s)) (erase(y)) = (x |-> erase(s)) y = y
よっていえた
よってt = yの場合にいえた
(t = λy:T1.t2の場合)
IH: erase((x |-> s)t2) = (x |-> erase(s)) (erase(t2))
erase((x |-> s) (λy:T1.t2)) = erase(λy:T1.(x |-> s)t2) = λy.erase((x |->s)t2) = λy.(x |-> erase(s)) erase(t2)
(x |-> erase(s)) (erase(λy:T1.t2)) = (x |-> erase(s)) λy.erase(t2) = λy.(x |-> erase(s)) erase(t2)
よってt = λy:T1.t2の場合にいえた
(t = t1 t2の場合)
IH1: erase((x |-> s)t1) = (x |-> erase(s)) (erase(t1))
IH2: erase((x |-> s)t2) = (x |-> erase(s)) (erase(t2))
erase((x |-> s)(t1 t2)) = erase((x |-> s)t1 (x |-> s)t2) = erase((x |-> s)t1) erase((x |-> s)t2) = (x |-> erase(s)) (erase(t1)) (x |-> erase(s)) (erase(t2))
(x |-> erase(s)) (erase (t1 t2)) = (x |-> erase(s)) (erase(t1) erase(t2)) = (x |-> erase(s))(erase(t1)) (x |-> erase(s))(erase(t2))
よってt = t1 t2の場合にいえた
(1の証明)
t -> t'の導出に関する帰納法
(E-App1の場合)
t = t1 t2
t' = t1' t2
t1 -> t1'
IH: t1 -> t1' ならば erase(t1) -> erase(t1')
IHより erase(t1) -> erase(t1')
(E-App1)より erase(t1) erase(t2) -> erase(t1') erase(t2)
eraseの定義をたどって erase(t1 t2) -> erase(t1' t2)
よって erase(t) -> erase(t')
なのでE-App1の場合にいえた
E-App2の場合も同様 ただしt1は値であることに注意
(E-AppAbsの場合)
t = (λx:T11.t12) v2
t' = (x |-> v2) t12
erase(t) = erase((λx:T11.t12) v2) = erase(λx:T11.t12) erase(v2) = λx.erase(t12) erase(v2)
erase(t') = erase((x |-> v2) t12) = (x |-> erase(v2)) erase(t12) (補題Bより)
erase(t) -> erase(t') がいえた
ifの規則についてもできるはず
(2の証明)
m = erase(t) とおこう
m -> m' の構造に関する帰納法
じつはtの構造に関する帰納法のほうが簡単?
9.5.3 定義
型なしラムダ計算の項mはλ→においてtypableである
erase(t) = m かつ ある文脈Γがあって Γ |- t : T
9.6 Curry-StyleとChurch-Style
ここまで2つの異なる流儀を見てきた
単純型付きの体系の文法の上に直接に評価関係を定義する
型なしの体系と型なしの評価関係に変換する
項tのふるまいについて、tが実際にwell-typedであるかどうかに関わらず議論できる
Curry-style
項を定義する
項のふるまい(意味論)を定義する
望ましくないふるまいをする項を拒否する型システムを定義する
意味論が先
Church-style
型システムが先
ill-typedな項のふるまいを考えない
Church-styleの体系では項ではなく型導出を評価する(?)
§15.6でこの例を見る
歴史的には、ラムダ計算の暗黙的な型付けがCurry-styleで与えられる
一方でChurch-styleの表現は明示的に型付けされた体系のためにのみある
これが用語の混乱をまねいてきた
Church-style はしばしば明示的に型付けされた文法のことを指して使われた
Curry-style はしばしば暗黙的に型付けされた文法のことを指して使われた