TaPL輪講/11章/11.3.1 定理の証明
11.3.1 定理
sequencingは派生形式である
λE を単純型付きラムダ計算+Unit型+sequencingの規則
λI を単純型付きラムダ計算+Unit型 とする
e : λE -> λI をt1; t2 を (λx:Unit. t2) t1 (xはfresh) に置換する関数であるとする
λEの項tについて以下が成り立つ
$ t \rightarrow_E t' \iff e(t) \rightarrow_I e(t')
$ \Gamma \vdash^E t : T \iff \Gamma \vdash^I e(t) : T
(証明)
補題A:λIの項について e(t) = t
(補題Aの証明)
tの構造に関する帰納法
(t=unit, xの場合)
これは明らか
(t=λx:T1.t2の場合)
IH:e(t2) = t2
e(t) = e(λx:T1.t2) = λx:T1.e(t2) = λx:T1.t2
よっていえた
(t=t1 t2の場合)
IH1:e(t1)=t1
IH2:e(t2)=t2
e(t) = e(t1 t2) = e(t1) e(t2) = t1 t2 = t
よっていえた
(補題Aの証明終了)
tの構造に関する帰納法で示せるらしい(ほんとうに?????)
$ t \rightarrow_E t' \iff e(t) \rightarrow_I e(t') について
(=>)
$ t \rightarrow_E t' \Rightarrow e(t) \rightarrow_I e(t') を示す
tの構造に関する帰納法
(t = unitの場合)
ありえない
(t = xの場合)
ありえない
(t = λx:T1.t2の場合)
ありえない
(t = t1 t2の場合)
H: t1 t2 ->E t'
IH1: 任意のt1'について t1 ->E t1' ならば e(t1) ->I e(t1')
IH2: 任意のt2'について t2 ->E t2' ならば e(t2) ->I e(t2')
Hについて場合分け
(subcase: E-App1の場合)
t1 ->E t1'である
IH1より e(t1) ->I e(t1')
よって(E-App1)より e(t1) e(t2) ->I e(t1') e(t2)
eの定義をもどして e(t1 t2) ->I e(t1' t2)
ゆえに e(t) ->I e(t')
E-App2も同様
(subcase: E-AppAbsの場合)
t1 = λx:T1.t12
t2 = v2
e((x |-> v2)t12) = (x |-> v2)e(t12)
なので e((λx:T1.t12)v2) ->I (x |-> v2)e(t12) = e((x |-> v2)t12)
よって e(t) ->I e(t')
以上よりt = t1 t2の場合にいえた
(t = t1; t2の場合)
H: t1; t2 ->E t'
IH1: 任意のt1'について t1 ->E t1' ならば e(t1) ->I e(t1')
IH2: 任意のt2'について t2 ->E t2' ならば e(t2) ->I e(t2')
Hについて場合分け
(subcase: E-Seqの場合)
t1 ->E t1'
IH1より e(t1) ->I e(t1')
したがって
e(t1; t2) = (λx:Unit.e(t2))e(t1) (xはfresh)
規則(E-App2)より(λx:Unit.e(t2))e(t1) ->I (λx:Unit.e(t2))e(t1') = e(t1'; t2)
(subcase: E-SeqNextの場合)
t1 = unit
e(unit; t2) = (λx:Unit.e(t2))unit ->I (x |-> unit)e(t2)
いまxはfreshなので(x |-> unit)e(t2) = e(t2)
よって e(unit; t2) ->I e(t2)
以上より=>についていえた
(<=)
$ e(t) \rightarrow_I e(t') \Rightarrow t \rightarrow_E t' を示す
補題B:λEの項tについて e(t) ->I t' ならばあるλEの項t0があってt'=e(t0)と表せる
(補題Bの証明)
tの構造に関する帰納法
(t = unit, x, λx:T1.t2)
ありえない
(t = t1 t2)
IH1: e(t1) ->I t1' ならばあるλEの項t01があってt1'=e(t01)と表せる
IH2: e(t2) ->I t2' ならばあるλEの項t02があってt2'=e(t02)と表せる
Goal: あるλEの項t0があってt'=e(t0)と表せる
e(t1 t2) = e(t1) e(t2)
e(t1) e(t2) ->I t' について場合分け
(subcase: E-App1)
e(t1) ->I t1'
IH1よりあるλEの項t01があってt1'=e(t01)と表せる
E-App1よりe(t1) e(t2) ->l e(t01) e(t2)
eの定義を逆にたどって e(t1 t2) ->I e(t01 t2)
ここではt0=t01 t2とおくことでt' = e(t0)と表せる
E-App2も同様
(subcase: E-AppAbs)
e(t1) = λx:T1.t2
e(t2) = v2
(λx:T1.t2) v2 ->I (x |-> v2) t2
t' = (x |-> v2) t2
t'はλIの項なのでt0=t'とおくことでt'=e(t0)と表せる
(subcase終了)
(補題Bの証明終了)
同じようにやると示せそう→ほんとうですか?
(t = unit, x, λx:T1,t2 の場合)
ありえない
(t = t1 t2の場合)
IH1: 任意のt1'について e(t1) ->I e(t1') ならば t1 ->E t1'
IH2: 任意のt2'について e(t2) ->I e(t2') ならば t2 ->E t2'
e(t1) e(t2) ->I e(t') について場合分け
(subcase: E-App1の場合)
e(t1) ->I t1'
補題Bよりあるt01があってt1'=e(t01)と表せる
よってe(t1) ->I e(t01)
IH1より t1 ->E t01
E-App1より t1 t2 ->E t01 t2
よってE-App1について示された
E-App2も同様
(subcase: E-AppAbsの場合)
e(t1) = λx:T1.t2
e(t2) = v2
e(t1) e(t2) = (λx:T1.t2) v2
(λx:T1.t2) v2 ->I (x |-> v2) t2
ところで t2 = e(t2)
定義を逆にたどって t1 = λx:T1.t2
よって (λx:T1.t2) v2 ->E (x |-> v2) t2
ここ怪しい議論をしている
(subcase終了)
(t = t1; t2の場合)
e(t1; t2) ->I t'
補題Bよりあるt0があってt'=e(t0)と表せる
e(t1; t2) = (λx:Unit.e(t2))e(t1)
IH1: 任意のt1'について e(t1) ->I e(t1') ならば t1 ->E t1'
IH2: 任意のt2'について e(t2) ->I e(t2') ならば t2 ->E t2'
(λx:Unit.e(t2))e(t1) ->I t'はE-AppAbsしかありえないので
t' = (x |-> e(t1))e(t2)
いまxはt2に現れないfreshな変数なのでt' = e(t2)
t1; t2 ->E t2
むずい
補題C:x/∈FV(t)ならば(x |-> s)t = t
(補題Cの証明)
tの構造に関する帰納法
(t = y)
x = yとするとx/∈FV(t)という仮定に反するのでありえない
よってx <> y
すると(x |-> s)y = y
(t = λy:T1.t2)
IH:x/∈FV(t2)ならば(x |-> s)t2 = t2
(x |-> s)t = (x |-> s)λy:T1.t2 = λy:T1.(x |-> s)t2
IHを使いたいのでx/∈FV(t2)であることを確かめる
いま仮定よりx/∈FV(t)
FV(t) = FV(λy:T1.t2) = FV(t2) - {y}
よってx/∈FV(t2) - {y}
(さらに補題)
いっぱんに x/∈S - {y} かつ x <> y ならば x/∈S となる?
対偶「x∈Sならばx∈S - {y} または x = y」を示すことで示したい
いまx∈Sと仮定する
Goal: x∈S - {y} または x = y
x = y とすると明らかに成り立つ
x <> yとする
Goal: x∈S - {y}
Goal: x∈S かつ x/∈{y}
左は仮定からわかる
右はx<>yからわかる
よって成り立つぽい
(さらに補題証明終了)
「さらに補題」からx/∈FV(t2)
なのでIHが使える
よって (x |-> s)t = λy:T1.(x |-> s)t2 = λy:T1.t2
(t = t1 t2)
H: x/∈FV(t) = FV(t1)∪FV(t2)
IH1: x/∈FV(t1) ならば (x |-> s)t1 = t1
IH2: x/∈FV(t2) ならば (x |-> s)t2 = t2
(x |-> s)t = (x |-> s)(t1 t2) = (x |-> s)t1 (x |-> s)t2
IH1とIH2が使えればわかるので前提が成り立つことを確かめたい
x/∈FV(t1)∪FV(t2) から x/∈FV(t1) かつ x/∈FV(t2) は対偶をとるとすぐわかる
よってIH1とIH2が使えるのでいえた
(t = t1; t2)
t = t1 t2の場合と同様にいえる
(補題Cの証明終了)
$ \Gamma \vdash^E t : T \iff \Gamma \vdash^I e(t) : T について
(補題1)
Γ |- t : T かつ x/∈FV(t) ならば Γ, x:S |- t : T
(補題1の証明)
Γ |- t : T の導出に関する帰納法
(T-Unit)
すぐわかる
(T-Var)
t = y
y:T∈Γ
x/∈ FV(t) より x<>y
明らかに y:T∈(Γ, x:S)
T-Varより Γ, x:S |- t : T
よっていえた
(T-Abs)
t = λy:T1.t2
T = T1 -> T2
Γ, y:T1 |- t2 : T2
IH: Γ, y:T1 |- t2 : T2 かつ x/∈FV(t2) ならば Γ, y:T1, x:S |- t2 : T2
x/∈FV(t) = FV(t2) - {y}
「さらに補題」から x/∈FV(t2)
よってIHが使えて Γ, y:T1, x:S |- t2 : T2
permutation lemmaから Γ, x:S, y:T1 |- t2 : T2
T-Absより Γ, x:S |- λY:T1.t2 : T1 -> T2
よっていえた
(T-App)
t = t1 t2
Γ |- t1 : T1 -> T
Γ |- t2 : T1
IH1: Γ |- t1 : T1 -> T かつ x/∈FV(t1) ならば Γ, x:S |- t1 : T1 -> T
IH2: Γ |- t2 : T1 かつ x/∈FV(t2) ならば Γ, x:S |- t2 : T1
x/∈FV(t) = FV(t1) ∪ FV(t2)
対偶をとることで x/∈FV(t1) かつ x/∈FV(t2)
IH1, IH2より Γ, x:S |- t1 : T1 -> T かつ Γ, x:S |- t2 : T1
T-Appよりいえた
(T-Seq)
t = t1; t2
T-Appと同様にしていえる
(補題1の証明終了)
(=>)
Γ |-E t : Tの導出に関する帰納法
(T-Unit, T-Varの場合) すぐわかる
(T-Absの場合)
t = λx:T1.t2
T=T1->T2
IH:Γ,x:T1 |-E t2 : T2 ならば Γ,x:T1 |-I e(t2) : T2
Γ |-E λx:T1.t2 : T2
inversion lemma より(?) Γ,x:T1 |-E t2 : T2
IHより Γ,x:T1 |-I e(t2) : T2
(T-Abs)より Γ |-I λx:T1.e(t2) : T2
eの定義より Γ |-I e(λx:T1.t2) : T2
よっていえた
(T-Appの場合)
t = t1 t2
H1: Γ |-E t1 : T1 -> T
H2: Γ |-E t2 : T1
IH1: Γ |-E t1 : T1 -> T ならば Γ |-I e(t1) : T1 -> T
IH2: Γ |-E t2 : T1 ならば Γ |-I e(t2) : T1
H1, H2, IH1, IH2より Γ |-I e(t1) e(t2) : T
eの定義より Γ |-I e(t1 t2) : T
よっていえた
(T-Seqの場合)
t = t1; t2
H1: Γ |-E t1 : Unit
H2: Γ |-E t2 : T
IH1: Γ |-E t1 : Unit ならば Γ |-I e(t1) : Unit
IH2: Γ |-E t2 : T ならば Γ |-I e(t2) : T
H2, IH2より Γ |-I e(t1) : T
freshな変数xを用いて補題1より Γ,x:Unit |-I e(t2) : T
(T-Abs)より Γ |-I λx:Unit.e(t2) : Unit -> T
H1, IH1より Γ |-I e(t1) : Unit
(T-App)より Γ |-I (λx:Unit.e(t2)) e(t1) : T
eの定義を引き戻して Γ |-I e(t1; t2) : T
よっていえた
以上より(=>)はOK
(<=)
$ P(t) : \forall T, \Gamma. \Gamma \vdash^I e(t) : T \Rightarrow \Gamma \vdash^E t : T
∀t.P(t) をtの構造に関する帰納法で示す
ここでTとΓを任意にとる
(t = unit)
Γ |-I e(unit) : T
e(unit) = unit
inversion lemmaよりT = unit
Γ |-E unit : Unit は(T-Unit)からいえる
(t = x)
Γ |-I e(x) : T
e(x) = x
inversion lemmaよりx:T ∈ Γ
Γ |-E x : T は(T-Var)からいえる
(t = λx:T1.t2)
Γ |-I e(λx:T1.t2) : T
IH: ∀T,Γ. Γ |-I e(t2) : T => Γ |-E t2 : T
e(λx:T1.t2) = λx:T1.e(t2)
Γ |-I λx:T1.e(t2) : T
inversion lemmaより
T=T1->T2
Γ,x:T1 |-I e(t2) : T2
IHよりΓ,x:T1 |-E t2 : T2
(T-Abs)よりΓ |-E λx:T1.t2 : T2
よっていえた
(t = t1 t2)
Γ |-I e(t1 t2) : T
IH1: ∀T,Γ. Γ |-I e(t1) : T => Γ |-E t1 : T
IH2: ∀T,Γ. Γ |-I e(t2) : T => Γ |-E t2 : T
e(t1 t2) = e(t1) e(t2)
inversion lemmaより
Γ |-I e(t1) : T1->T
Γ |-I e(t2) : T1
IH1より Γ |-E t1 : T1 -> T
IH2より Γ |-E t2 : T1
(T-App)より Γ |-E t1 t2 : T
よっていえた
(t = t1; t2)
Γ |-I e(t1; t2) : T
Goal: Γ |-E t1; t2 : T
IH1: ∀T,Γ. Γ |-I e(t1) : T => Γ |-E t1 : T
IH2: ∀T,Γ. Γ |-I e(t2) : T => Γ |-E t2 : T
e(t1; t2) = (λx:Unit.e(t2))e(t1) (xはfresh)
inversion lemmaより
Γ |-I (λx:Unit.e(t2)) : Unit -> T
Γ |-I e(t1) : Unit
IH1よりΓ |-I t1 : Unit
inversion lemmaより
Γ,x:Unit |-I e(t2) : T
IH2より Γ,x:Unit |-E t2 : T
xはt2に自由に現われないので補題1より Γ |-E t2 : T
よって Γ |-E t1; t2 : T
よっていえた
以上より(<=)も示された
ハアハア 何がstraightforward induction on the structure of tだ