型付きラムダ計算の自由帳[]
この記事では各項目ごとに提示した型付きラムダ式について、確かに正しく型付けされていることの推論を載せたいと考えています。
内容は適宜増やすつもりです。
間違いがあれば訂正します。
型の推論についてはWikipediaの記事"Calculas of Constructions"やローダー数解説記事を参考にしています。
表記について[]
推論は、推件式 を集めたもののことです。 や にはいくつか(空でもよい)のラムダ式が入ります。公理から推論を始めて、推論規則のみを使って推件式の左辺が空になった場合、右辺のラムダ式は正しく型付けされていることになります。
しかし推論の図を描くことは私には難しく、また同じ式を複数回使用することがあることから、一行につき一つの推件式を記載し、それらに整理番号を付けることにしました。また、その推論がどの番号から導出されて、どの推論規則を使用しているかを併記しています。これにより、提示した推論を追いやすくなると考えたからです。
樹形図を描いた方が見通しがよくなります。
１．一行表記[]
このページでは推件式を以下のように並べます。
推件式 （整理番号:引用する番号:推論規則）
（推論の例）
公理 （0:_:axiom）
推論１ （1:0:????）
推論２ （2:1,1:????）
推論３ （3:1,2:????）
・・・・・
２．推論規則[]
├*:□ (0::Axiom)
x∉Γ├A:{*,□} (1::)
Γ,x:A├x:A (2:1:Variable)
x∉Γ├t:T (3::)
x∉Γ├A:{*,□} (4::)
Γ,x:A├t:T (5:3,4:Weakening)
Γ,x:A├B:{*,□} (6::)
Γ├(Πx:A.B):{*,□} (7:6:Formation)
Γ,x:A├M:B (8::)
Γ├(Πx:A.B):{*,□} (9::)
Γ├(λx:A,M):(Πx:A.B) (10:8,9:Abstraction)
Γ├M:(Πx:A.B) (11::)
Γ├y:A (12::)
Γ├(My):(B[x:=y]) (13:11,12:Application)
以上
恒等関数[]
(λT:*.λx:T.x):(ΠT:*.Πx:T.T)
型と変数を適用すると、変数をそのまま返す関数。
推論
├*:□ (0:_:Axiom)
T:*├T:* (1:0:Var)
T:*,x:T├T:* (2:1,1:weak)
T:*├(Πx:T.T):* (3:2:Form)
T:*├(λx:T.x):(Πx:T.T) (4:2,3:Abst)
├(ΠT:*,Πx:T.T):* (5:3:Form)
├(λT:*.λx:T.x):(ΠT:*.Πx:T.T) (6:4,5:Abst) 終わり
真理値[]
真、True[]
推論
├*:□ (0:_:axiom)
R:*├R:* (1:0:var)
R:*,a:R├R:* (2:1,1:weak)
R:*,a:R,b:R├R:* (3:2,2:weak)
R:*,a:R├(Πb:R.R):(*) (4:3:form)
R:*├(Πa:R.Πb:R.R):(*) (5:4:form)
├(ΠR:*.Πa:R.Πb:R.R):(*) (6:5:form)
R:*,b:R├R:* (7:1:weak)
R:*,a:R,b:R├a:R (8:7:var)
R:*,a:R├(λb:R.a):(Πb:R.R) (9:3,8:abst)
R:*├(λa:R.λb:R.a):(Πa:R.Πb:R.R) (10:5,9:abst)
├(λR:*.λa:R.λb:R.a):(ΠR:*.Πa:R.Πb:R.R) (11:6,10:abst) 終わり
偽、false[]
推論
自然数[]
自然数を扱う上では、ここで宣言した自然数および自然数の型が、確かに自然数としての性質を満たすことを含めて提示したいと考えています。（現在は未実装）
自然数および自然数の型[]
(λR:*.λf:(Πt:R.R).λx:R.f^n(x)):(ΠR:*.Πf:(Πt:R.R).Πx:R.R))
ゼロ[]
0:N ⇔ (λR:*.λf:(Πt:R.R).λx:R.x):(ΠR:*.Πf:(Πt:R.R).Πx:R.R)
推論
├*:[] (0:_:axiom)
R:*├R:* (1:0:var)
R:*,x:R├R:* (2:1,1:weak)
R:*,t:R├R:* (3:1,1:weak)
R:*├(Πx:R.R):* (4:2:form)
R:*├(Πt:R.R):* (5:3:form)
R:*,f:(Πt:R.R)├(Πx:R.R):* (6:4,5:weak)
R:*├(Πf:(Πt:R.R).Πx:R.R):* (7:6:form)
├(ΠR:*.Πf:(Πt:R.R).Πx:R.R):* (8:7:form)
R:*,f:(Πt:R.R)├R:* (9:1,5:weak)
R:*,f:(Πt:R.R),x:R├x:R (10:9:var)
R:*,f:(Πt:R.R)├(λx:R.x):(Πx:R.R) (11:6,10:abst)
R:*├(λf:(Πt:R.R).λx:R.x):(Πf:(Πt:R.R).Πx:R.R) (12:7,11:abst)
├(λR:*.λf:(Πt:R.R).λx:R.x):(ΠR:*.Πf:(Πt:R.R).Πx:R.R)(13:8,12:abst) 終わり
後者関数[]
succ:N->N⇔(λn:(ΠR:*.Πf:(Πt:R.R).Πx:R.R).λR:*.λf:(Πt:R.R).λx:R.f(nRfx)):(Πn:(ΠR:*.Πf:(Πt:R.R).Πx:R.R).ΠR:*.Πf:(Πt:R.R).Πx:R.R)
推論
|=*:□ [0:_:axiom]
R:*|=R:* [1:0:var]
R:*,x:R|=R:* [2:1,1:weak]
R:*,t:R|=R:* [3:1,1:weak]
R:*|=(Πx:R.R):* [4:2:form]
R:*|=(Πt:R.R):* [5:3:form]
R:*,f:(Πt:R.R)|=(Πx:R.R):* [6:4,5:weak]
R:*|=(Πf:(Πt:R.R).Πx:R.R):* [7:6:form]
|=(ΠR:*.Πf:(Πt:R.R).Πx:R.R):* [8:7:form] (自然数の型 N)
n:(ΠR:*.Πf:(Πt:R.R).Πx:R.R)|=(ΠR:*.Πf:(Πt:R.R).Πx:R.R):* [9:8,8:weak]
|=(Πn:(ΠR:*.Πf:(Πt:R.R).Πx:R.R).(ΠR:*.Πf:(Πt:R.R).Πx:R.R)):* [10:9:form] (自然数から自然数への関数型 N->N)
R:*,f:(Πt:R.R)|=R:* [11:1,5:weak]
R:*|=(ΠR:*.Πf:(Πt:R.R).Πx:R.R):* [12:0,8:weak]
R:*,f:(Πt:R.R)|=(ΠR:*.Πf:(Πt:R.R).Πx:R.R):* [13:12,5:weak]
R:*,f:(t:R.R),x:R|=(ΠR:*.Πf:(Πt:R.R).Πx:R.R):* [14:13,11:weak]
R:*,x:R,t:R|=R:* [15:2,2:weak]
R:*,x:R|=(Πt:R.R):* [16:15:form]
R:*,f:(Πt:R.R),x:R|=f:(Πt:R.R) [17:16,16:var]
R:*,f:(Πt:R.R),x:R|=x:R [18:11:var]
n:(ΠR:*.Πf:(Πt:R.R).Πx:R.R),R:*,f:(Πt:R.R),x:R|=x:R [19:18,14:weak]
n:(ΠR:*.Πf:(Πt:R.R).Πx:R.R),R:*,f:(Πt:R.R),x:R|=f:(Πt:R.R) [20:17,14:weak]
R:*,f:(Πt:R.R),x:R|=R:* [21:11,11:weak]
n:(ΠR:*.Πf:(Πt:R.R).Πx:R.R),R:*,f:(Πt:R.R),x:R|=R:* [22:21,14:weak]
n:(ΠR:*.Πf:(Πt:R.R).Πx:R.R),R:*,f:(Πt:R.R),x:R|=n:(ΠR:*.Πf:(Πt:R.R).Πx:R.R) [23:14:var]
n:(ΠR:*.Πf:(Πt:R.R).Πx:R.R),R:*,f:(Πt:R.R),x:R|=nR:(Πf:(Πt:R.R).Πx:R.R) [24:23,22:app]
n:(ΠR:*.Πf:(Πt:R.R).Πx:R.R),R:*,f:(Πt:R.R),x:R|=nRf:(Πx:R.R) [25:24,20:app]
n:(ΠR:*.Πf:(Πt:R.R).Πx:R.R),R:*,f:(Πt:R.R),x:R|=nRfx:R [26:25,19:app]
n:(ΠR:*.Πf:(Πt:R.R).Πx:R.R),R:*,f:(Πt:R.R),x:R|=f(nRfx):R [27:20,26:app]
n:(ΠR:*.Πf:(Πt:R.R).Πx:R.R),R:*,f:(Πt:R.R)|=(Πx:R.R):* [28:15:form]
n:(ΠR:*.Πf:(Πt:R.R).Πx:R.R),R:*,f:(Πt:R.R)|=(λx:R.f(nRfx)):(Πx:R.R) [29:27,28:abst]
n:(ΠR:*.Πf:(Πt:R.R).Πx:R.R),R:*|=(Πf:(Πt:R.R).Πx:R.R):* [30:28:form]
n:(ΠR:*.Πf:(Πt:R.R).Πx:R.R),R:*|=(λf:(Πt:R.R).λx:R.f(nRfx)):(Πf:(Πt:R.R).Πx:R.R) [31:29,30:abst]
n:(ΠR:*.Πf:(Πt:R.R).Πx:R.R)|=(λR:*.λf:(Πt:R.R).λx:R.f(nRfx)):(ΠR:*.Πf:(Πt:R.R).Πx:R.R) [32:31,9:abst]
|=(λn:(ΠR:*.Πf:(Πt:R.R).Πx:R.R).λR:*.λf:(Πt:R.R).λx:R.f(nRfx)):(Πn:(ΠR:*.Πf:(Πt:R.R).Πx:R.R).ΠR:*.Πf:(Πt:R.R).Πx:R.R) [33:32,10:abst]（後者関数succ:N->N）終わり