初めに
ラムダ計算の β-簡約から得られる形式理論 λβ に対し、 η-簡約に関する公理
λx.Mx=M(x∉FV(M))
を加えたものを λβη とする。
このとき、 いわゆる外延性
(∀Z∈Λ⊢λβηMZ=NZ)⟹⊢λβηM=N
が成り立つことが知られている。
一方で、 この Z を閉じたラムダ項のみに制限した命題
(∀Z∈Λ∅⊢λβηMZ=NZ)⟹⊢λβηM=N
は一般には成り立たない。
この反例を構成する。
以下、 α-同値なラムダ項は同一視する。
また、 →h と ↠h はそれぞれ 1 回および複数回の冠頭簡約を表す。
なお、 ここでは冠頭簡約とは、
(λx.M1)M2M3⋯Mn↠hM2[x:=M1]M3⋯Mn(n≥2)
という形の β-簡約を指す。
これは一般に言われる冠頭簡約とは少し異なるが、 ここでは Plotkin の論文での用法に合わせた。
以下のコンビネータの記号を用いる。
なお、 ここではコンビネータと閉じたラムダ項は同じ意味で用いる。
I ≡ λx.x K ≡ λxy.x S ≡ λxyz.xz(yz) Y ≡ (λfx.x(ffx))(λfx.x(ffx)) Σ ≡ λufx.f(ufx)
また、 自然数 n に対して、 その Church 数を
n≡λfx.f(f(⋯(f⏟n 個x)))
と表す。
ラムダ項 M の Gödel 数 は #M とし、 M の Gödel 数の Church 数を ⌈M⌉≡#M で表す。
ラムダ項全体は Λ で表し、 閉じたラムダ項全体は Λ∅ で表す。
Gödel 数の逆関数
Gödel 数をとる操作の逆を行うコンビネータ E を構成する。
構成には再帰関数のラムダ項による表現可能性の議論が必要になるが、 ここでは詳しく述べない。
定義 1.
ラムダ項から成る集合 に対し、 ラムダ項から成る集合 Comb() を以下によって再帰的に定義する。
M∈ ⟹ M∈Comb() P,Q∈Comb() ⟹ PQ∈Comb()
このとき、 Comb() の元を の結合 (combination) という。
={M1,⋯,Mn} のときは、 Comb() を単に Comb{M1,⋯,Mn} と書く。
補題 2.
あるコンビネータ X であって、
∀M∈Λ∅∃M∗∈Comb{X}M∗↠βM
を満たすものが存在する。
証明.
X を
X≡λx.xKSK
によって定義する。
このとき、
XXX ↠β K X(XX) ↠β S
が成り立つ。
さて、 任意の閉じたラムダ項 M に対し、 K と S の結合 N が存在して N↠βM が成り立つ。
したがって、 N に含まれる K と S をそれぞれ XXX と X(XX) で置き換えたものを M∗ とおけば、 M∈Comb{X} であって M∗↠βM が成り立つ。
定義 3.
X の結合 M に対し、 自然数 $M を以下によって再帰的に定義する。
$X = 0 $(PQ) = pair($P,$Q)
ここで、 pair は
pair: × ⟶ (m,n) ⟼ (m+n)(m+n+1) 2+n+1
によって定義される全単射な再帰関数である。
補題 4.
閉じたラムダ項 F であって、
∀M∈Comb{X}F$M=βM
を満たすものが存在する。
証明.
まず、 上の定義における関数 pair に対し、 任意の自然数 m,n について
fst(pair(m,n))=msnd(pair(m,n))=n
を満たす関数 fst,snd は再帰的である。
したがって、 それを表現する閉じたラムダ項 fst,snd が存在する。
さらに、
zero≡λu.u(λv.λxy.y)(λxy.x)
と定義する。
これは与えられた Church 数が 0 かどうかを判定するラムダ項である。
これと上で定義した fst,snd を用いて、
F≡Y(λf.λu.zerouX(f(fstu)(f(sndu))))
とおく。
この F が補題の条件を満たしていることを示す。
証明は M に関する帰納法による。
M≡X のときは、
F$X ≡ F0 =β zero0X(F(fst0)(F(snd0))) =β X
であるから、 補題は成り立つ。
M≡PQ のときは、
U≡pair($P,$Q)
とおくと U≠β0 だから、 帰納法の仮定を用いて、
F$(PQ) ≡ FU =β zeroUX(F(fstU)(F(sndU))) =β F(fstU)(F(sndU)) =β Ffst(pair($P,$Q))(Fsnd(pair($P,$Q))) ≡ F$P(F$Q) =β PQ
を得る。
したがって、 この場合も補題は成り立つ。
補題 5.
閉じたラムダ項 G であって、
∀M∈Λ∅G⌈M⌉=β$M∗
を満たすものが存在する。
なお、 M∗ は補題 2 で定義されたものである。
証明.
補題 2 の証明から、 閉じたラムダ項 M に対し、 M∗ は M から再帰的に決定できる。
したがって、
g:#M⟼$M∗
によって定義される部分関数は再帰的である。
これを表現するラムダ項を G とおけば、
G⌈M⌉=βg(#M)≡$M∗
が成り立つ。
定理 6.
コンビネータ E であって、
∀M∈Λ∅E⌈M⌉=βM
を満たすものが存在する。
証明.
補題 4 の F と補題 5 の G を用いて、
E≡λu.uF(Gu)
とおけば良い。
実際、 閉じたラムダ項 M に対して、
E⌈M⌉=βF(G⌈M⌉)=βF$M∗=βM∗=βM
が成り立つ。
標準簡約列
定義 7.
β-簡約から成る標準簡約列 (standard reduction sequence) を、 以下によって再帰的に定義する。
- x は単独で長さ 1 の標準簡約列である。
- 簡約列
M1→⋯→MmN1→⋯→Nn
がそれぞれ長さ m,n の標準簡約列ならば、
M1N1→⋯→MmN1→⋯→MmNn
も長さ m+n の標準簡約列である。
- 簡約列
M1→⋯→Mm
が長さ m の標準簡約列ならば、
λx.M1→⋯→λx.Mm
も長さ m の標準簡約列である。
- 簡約列
M1→⋯→MmN1→⋯→Nn
がそれぞれ長さ m,n の標準簡約列であるとする。
Mm が M1,⋯,Mm の中で最初のラムダ抽象項であり、 あるラムダ項 N に対して MmN→hN1 ならば、
M1N→⋯→MmN→N1→⋯→Nn
は長さ m+n の標準簡約列である。
また、 M から N への標準簡約列が存在することを M↠sN で表す。
補題 8.
簡約列
M1→⋯→Mm
が標準簡約列であり、 Mm はこの簡約列に含まれるラムダ項の中で最初のラムダ抽象項であるとする。
このとき、 この簡約列を構成する全ての簡約は冠頭簡約である。
すなわち、
M1→h⋯→hMm
が成り立つ。
証明.
m に関する帰納法による。
m=1 ならば明らかなので、 m≥2 とする。
Mm は M1,⋯,Mm の中の唯一のラムダ抽象項なので、 標準簡約列
σ:M1→⋯→Mm
が上の定義の 4 番目以外から作られることはない。
すると σ は、
σ:P1Q→⋯→PpQ→Q1→⋯→Qq
という形であり、
τ: P1→⋯→Pp ρ: Q1→⋯→Qq
は標準簡約列である。
また、 PpQ→hQ1 が成り立つ。
ここで p<m および q<m であるから、 帰納法の仮定より τ と ρ を構成する全ての簡約は冠頭簡約である。
したがって、
P1Q→h⋯→hPpQ→hQ1→h⋯→hQq
であり、 σ を構成する全ての簡約も冠頭簡約である。
定理 9 [標準化定理 (standardisation theorem)].
ラムダ項 M,N に対し、 M↠βN ならば M↠sN である。
証明.
証明は Barendregt の 11 章などを参照。
反例の構成
以上の準備のもとで、 初めにに述べた反例を構成する。
この構成は Plotkin によるものである。
以下、
H ≡ λh.λguvw.hgu(hg(Σu)(g(Σu))wv)(Eu) H ≡ YH G ≡ λg.λu.Hg(Σu)(g(Σu))(E(Σu))(gu) G ≡ YG F ≡ HG M ≡ F0(G0) N ≡ λx.MI
とおく。
この M,N が存在を示したい反例になっているのだが、 それを証明するのにいくつか補題を用意する。
補題 10.
任意のラムダ項 U,V,W に対し、
FUVW↠hFU(F(ΣU)(G(ΣU))WV)(EU)
が成り立つ。
証明.
計算すれば、
FUVW ≡ YHGUVW ↠h H(YH)GUVW ≡ HHGUVW ≡ (λh.λguvw.hgu(hg(Σu)(g(Σu))wv)(Eu))HGUVW ↠h HGU((HG)(ΣU)(G(ΣU))WV)(EU) ≡ FU(F(ΣU)(G(ΣU))WV)(EU)
となり、 示された。
補題 11.
任意のラムダ項 U に対し、
GU=βF(ΣU)(G(ΣU))(E(ΣU))(GU)
が成り立つ。
証明.
計算すれば、
GU ≡ YGU =β G(YG)U ≡ GGU =β HG(ΣU)(G(ΣU))(E(ΣU))(GU) ≡ F(ΣU)(G(ΣU))(E(ΣU))(GU)
となり、 示された。
補題 12.
任意の自然数 m,n に対し、
Fn(Gn)(En)=βFn(Gn)(Em+n)
が成り立つ。
証明.
m に関する帰納法による。
m=0 のときは明らかなので、 m≥1 とする。
帰納法の仮定は、 任意の自然数 n に対して、
Fn(Gn)(En)=βFn(Gn)(Em+n−1)
が成り立つことである。
これと補題 10 と補題 11 を用いれば、
Fn(Gn)(En) =β Fn(F(Σn)(G(Σn))(E(Σn))(Gn))(En) =β Fn(Fn+1(Gn+1)(En+1)(Gn))(En) =β Fn(Fn+1(Gn+1)(Em+n)(Gn))(En) =β Fn(Gn)(Em+n)
と計算でき、 補題が示された。
補題 13.
任意の閉じたラムダ項 Z,Z に対して、
MZ=βMZ
が成り立つ。
証明.
n=#Z,n=#Z とおけば、 En=βZ,En=βZ である。
したがって、 補題 12 を用いれば、
MZ =β F0(G0)(En) =β F0(G0)(E0) =β F0(G0)(En) =β MZ
となる。
補題 14.
ラムダ項 U,V,W,Z をとる。
長さ l の標準簡約列
FUVW→⋯→Z
があり、 y∈FV(V) かつ y∉FV(Z) を満たしているとする。
このとき、 長さ l 以下の標準簡約列
V→⋯→V
であって、 y∉FV(V) を満たすものが存在する。
証明.
そうでないと仮定する。
このとき、 長さ l の標準簡約列
σ:FUVW→⋯→Z
が存在して、 y∈FV(V) かつ y∉FV(Z) を満たし、 さらに任意のラムダ項 V に対し、 長さ l 以下の標準簡約列
V→⋯→V
は y∈FV(V) を必ず満たす。
l はこのようなものの中で最小になるようにとる。
σ は標準簡約列の定義における 2 番目の形か 4 番目の形かのどちらかである。
これに応じて場合分けをする。
場合 1:σ が 4 番目の形であるとき。
このとき σ は、
σ:FUVW→⋯→(λw.P)W→Q→⋯→Z
という形であり、
τ : FUV→⋯→λw.P ρ : Q→⋯→Z
はともに長さ l 未満の標準簡約列である。
また、 (λw.P)W→hQ が成り立つ。
λw.P は τ に含まれるラムダ項の中で最初のラムダ抽象項なので、 補題 8 によって τ を構成する全ての簡約は冠頭簡約である。
したがって、 (λw.P)W→hQ と合わせて FUVW↠hQ が成り立つ。
さらに、 (λw.P)W は τ に含まれるラムダ項の中で最初のラムダ抽象項だから、 補題 10 の証明で行った計算を見ることで、
Q≡FU(F(ΣU)(G(ΣU))WV)(EU)
が分かる。
これより、 ρ の最初のラムダ項 Q は FUVW の形であり、 ρ の長さを l とすると l<l である。
したがって、 l の最小性から、 長さ l 以下の標準簡約列
π:F(ΣU)(G(ΣU))WV→⋯→Z
が存在し、 y∉FV(Z) が成り立つ。
π は標準簡約列の定義における 2 番目か 4 番目の形であるが、 F(ΣU)(G(ΣU))W から始まる冠頭簡約列にはラムダ抽象項が含まれ得ないので、 τ は 2 番目の形でなければならない。
すなわち π は、
π:F(ΣU)(G(ΣU))WV→⋯→AV→⋯→AV
の形であり、
θ : F(ΣU)(G(ΣU))W→⋯→A κ : V→⋯→V
はともに長さが l 以下の標準簡約列である。
しかし、 y∉FV(Z)=FV(AV) より y∉FV(V) が成り立つから、 κ の存在は仮定に反し矛盾である。
場合 2:σ が 2 番目の形であるとき。
このとき σ は、
σ:FUVW→⋯→ZW→⋯→ZW
の形であり、
τ:FUV→⋯→Z
は長さ l 以下の標準簡約列である。
また、 y∉FV(Z)=FV(ZW) より y∉FV(Z) を得る。
この τ は標準簡約列の定義の 2 番目か 4 番目の形であるが、 仮に 2 番目の形であるとすると、
τ:FUV→⋯→AV→⋯→AV
の形となり、
V→⋯→V
という標準簡約列が存在することになるが、 y∉FV(Z)=FV(AV) より y∉FV(V) なので矛盾である。
これにより、 τ は 4 番目の形である。
すなわち τ は、
τ:FUV→⋯→(λv.P)V→Q→⋯→Z
という形であり、
π:Q→⋯→Z
は長さ l 未満の標準簡約列である。
また、 補題 8 により FUV↠hQ が成り立つ。
これより、 補題 10 の証明の計算を見れば、
Q≡λw.FU(F(ΣU)(G(ΣU))wV)(EU)
が分かる。
したがって、 π は標準簡約列の 3 番目の形でなければならないから、
ρ:FU(F(ΣU)(G(ΣU))wV)(EU)→⋯→Z
という標準簡約列がある。
ρ の長さは l 未満で y∉FV(Z) であるから、 場合 1 の ρ に対して行った議論と同様の議論をすれば、 矛盾が導かれる。
補題 15.
ラムダ項 U,V,W,Z をとる。
標準簡約列
FUVW→⋯→Z
があり、 y∈FV(W) かつ y∉FV(Z) を満たしているとする。
このとき、 あるラムダ項 W であって、 W↠βW かつ W∉FV(W) を満たすものが存在する。
証明.
そうでないと仮定する。
このとき、 長さ l の標準簡約列
σ:FUVW→⋯→Z
が存在して、 y∈FV(W) かつ y∉FV(Z) を満たし、 さらに任意のラムダ項 W に対し、 W↠βW ならば y∈FV(W) が成り立つ。
l はこのようなものの中で最小になるようにとる。
σ が標準簡約列の定義における 2 番目の形か 4 番目の形のどちらであるかに応じて場合分けをする。
場合 1:σ が 2 番目の形であるとき。
このとき σ は、
σ:FUVW→⋯→PW→⋯→PW
の形であり、
W→⋯→W
という標準簡約列が存在する。
これより W↠βW であり、 y∉FV(Z)=FV(PW) より y∉FV(W) であるから、 矛盾である。
場合 2:σ が 4 番目の形であるとき。
このとき σ は、
σ:FUVW→⋯→(λw.P)W→Q→⋯→Z
の形であり、
τ:Q→⋯→Z
は長さ l 未満の標準簡約列である。
τ の長さを l とする。
また、 補題 8 により FUVW↠hQ が成り立つから、
Q≡FU(F(ΣU)(G(ΣG))WV)(EU)
が分かる。
y∈FV(F(ΣU)(G(ΣG))WV) かつ y∉FV(Z) だから、 補題 14 より、 長さ l 以下の標準簡約列
ρ:F(ΣU)(G(ΣG))WV→⋯→Z
が存在して、 y∉FV(Z) である。
ここで F(ΣU)(G(ΣG))W から始まる冠頭簡約列にはラムダ抽象項が含まれ得ないので、 ρ は標準簡約列の定義の 2 番目の形でなければならない。
すなわち ρ は、
ρ:F(ΣU)(G(ΣG))WV→⋯→ZV→⋯→ZV
の形であり、
π:F(ΣU)(G(ΣG))W→⋯→Z
は長さ l 以下の標準簡約列である。
また、 y∉FV(Z)=FV(ZV) より y∉FV(Z) である。
したがって、 l<l だから、 l の最小性より、 ある W が存在して W↠βW かつ y∉FV(W) となるが、 これは仮定に反し矛盾である。
補題 16.
変項 x,y に対し、
x≢y⟹Mx≠βηMy
が成り立つ。
証明.
x≢y かつ Mx=βηMy と仮定する。
Church–Rosser の定理より、 あるラムダ項 Z が存在して、 Mx↠βηZ および My↠βηZ が成り立つ。
また、 η-簡約は延期できるので、 あるラムダ項 Z が存在して、 My↠βZ↠Z が成り立つ。
標準化定理より、 My↠sZ である。
M は閉じているので y∉FV(Mx) であり、 FV(Mx)⊇FV(Z)=FV(Z) が成り立つから、 y∉FV(Z) でもある。
また、 明らかに y∈FV(y) である。
さらに、 My≡F0(G0)y であるから、 これは補題 15 が使える形である。
したがって、 補題 15 により、 あるラムダ項 W が存在して、 y↠βW かつ y∉FV(W) が成り立つ。
y は変項なので、 W≡y でなければならず、 これより y∉FV(y) となり矛盾である。
定理 17.
上で定義した M,N は、
(∀Z∈Λ∅MZ=βηNZ)⟹M=βηN
を満たさない。
証明.
任意に閉じたラムダ項 Z をとると、 I も閉じたラムダ項だから、 補題 13 によって MZ=βMI である。
一方、 N の定義により、 NZ=βMI である。
したがって、 MZ=βηNZ を得る。
M=βηN と仮定する。
任意の変項 x,y に対し、 Mx=βηNx および Mx=βηNy である。
さらに N の定義から、 Nx=βηMI および Ny=βηMI も成り立つ。
以上により Mx=βηMy を得るが、 これは補題 16 に反する。
したがって、 M≠βηN である。
補足
前節で示したように、 閉じたラムダ項に対してのみの外延性
(∀Z∈Λ∅MZ=βηNZ)⟹M=βηN
は一般には成り立たないが、 M と N が特定の条件を満たしている範囲であれば成り立つ。
その条件の 1 つとして、 以下のものが知られている。
定義 18.
ラムダ項 M について、
∀N∈Λ∃M∈ΛM↠βηMANDN∈Sub(M)
が成り立つとき、 M を βη-普遍生成子 (universal generator) という。
なお、 Sub(M) は M の部分項全体の集合を表す。
定理 19.
ラムダ項 M,N のうち、 どちらか一方が βη-普遍生成子でなければ、
(∀Z∈Λ∅MZ=βηNZ)⟹M=βηN
が成り立つ。
証明.
証明は Barendregt の 17 章などを参照。
参考文献
- H. P. Barendregt (1984) 『The Lambda Calculus』 North Holland
- G. D. Plotkin (1974) 「The λ-calculus is ω-incomplete」 『Journal of Symbolic Logic』 39:313–317