証明.

N は β-基なので、 N≡(λy.X)Y とおく。 また、 R󰎘≡P[x:=Q] とおく。 M の最も外側の構造によって場合分けする。

場合 1:M≡R のとき。 M が β-基ではないので、 これはあり得ない。

場合 2:M≡λw.X[R] と書けるとき。 N≡λw.X[R󰎘] となるが、 N は (λy.X)Y の形なので、 これはあり得ない。

場合 3:M≡TX[R] と書けるとき。 N≡TX[R󰎘] となり N≡(λy.X)Y であったから、 T≡λy.X である。 したがって M≡(λy.X)X[R] となるが、 M は β-基ではないのでこれは不可能である。

場合 4:M≡X[R]T と書けるとき。 N≡X[R󰎘]T となり N≡(λy.X)Y であったから、 X[R󰎘]≡λy.X である。 X に R󰎘 が含まれているとすると、 X[R󰎘]≡λy.Y[R󰎘] と書けて M≡(λy.Y[R])T となるが、 M は β-基ではないので矛盾である。 これより R󰎘≡X[R󰎘]≡λy.X でなければならず、 M≡RT となる。 ここで R󰎘≡P[x:=Q] だったから、

• P≡λy.U と表され U[x:=P]≡X が成り立つ。
• P≡x であり Q≡λy.X である。

のいずれかである。 このそれぞれが、 補題の主張のそれぞれの場合に対応している。

証明.

M の最も外側の構造によって場合分けする。

場合 1:M が変項の場合。 M≡y で y≢x あれば M[x:=N]≡N であるから、 これが β-基であるとすると M が β-基でないことに矛盾する。 したがって、 M≡x であり、 補題の主張の 2 番目の場合に相当する。

場合 2:M≡λw.T と書けるとき。 M[x:=N]≡λw.T[x:=N] であるが、 これは β-基になり得ない。 したがって、 この場合は不可能である。

場合 3:M≡VT と書けるとき。 さらに V の構造によって場合分けをする。 V≡XY と書ける場合は M≡XYT となるが、 このとき M[x:=N] は β-基になり得ず矛盾である。 V≡λv.X と書ける場合は M≡(λv.X)T となり、 M が β-基でないことに矛盾する。 以上により、 V は変項でなければならない。 V≡v かつ v≢x であれば M[x:=N]≡vT[x:=N] となるが、 これは β-基にはなり得ないので矛盾である。 よって V≡x である。 このとき M[x:=N]≡NT[x:=N] となるが、 これは β-基であるから、 N≡λy.U の形でなければならない。 これが補題の主張の 1 番目の場合に相当している。

証明.

ラムダ項 M に含まれる β-基 R≡(λx.P)Q を簡約して得られるラムダ項を N とする。 また、 S を R によって生成される β-基とする。 R󰎘≡P[x:=Q] とおく。 また、 M≡Y[R],N≡Z[S] と表す。 R󰎘 と S の位置によって場合分けする。

場合 1:R󰎘 と S が別の位置にあるとき。 このとき、 S は M にもそのまま出現しており、 それの残基が S なので、 この場合は不可能である。

場合 2:S が R󰎘 を含むとき。 M≡Z[S󰎘] となるような S󰎘 がある。 このとき、 S󰎘 には R が含まれ、 この R を簡約すると S になる。 また、 S󰎘 が β-基だとすると S は S󰎘 の残基になってしまい矛盾するので、 S󰎘 は β-基ではない。 したがって補題 5 が適用できる。

S󰎘≡(λx.P)QT かつ P≡λy.U となるときは、 M ≡ Z[(λx.(λy.U))QT] N ≡ Z[(λy.U[x:=Q])T] となり、 補題の主張の 2 番目のパターンになる。 一方、 S󰎘≡(λx.P)QT かつ P≡x,Q≡λy.U となるときは、 M ≡ Z[(λx.x)(λy.U)T] N ≡ Z[(λy.U)T] となり、 補題の主張の 3 番目のパターンになる。

場合 3:R󰎘 が S を含むとき。 まず、 S は Q には含まれない。 なぜなら、 もしそうだとすると S が残基になって矛盾するからである。 したがって、 P の部分項 P󰎘 であって P󰎘[x:=Q]≡S なるものが存在する。 ここで、 まず P󰎘≢x が分かる。 さらに P󰎘 は β-基ではない。 これは、 もしそうだとすると S が残基になって矛盾するからである。 以上により、 補題 6 が適用でき、 P󰎘≢x であることから、 P󰎘≡xT かつ Q≡λy.U と表せる。 P≡X[P󰎘] と書けば、 M ≡ Y[(λx.X[xT])(λy.U)] N ≡ Y[X[(λy.U)T]] となり、 補題の主張の 1 番目のパターンになる。

証明.

残基の定義から明らかである。

証明.

補題 7 の 3 パターンを全て調べれば良い。

場合 1:1 番目のパターンは、 (λxA⇀B.X[xA⇀BTA]C)(λyA.UB)→βX[(λyA.UB)TA]C と型付けられているはずである。 この場合において、 簡約した β-基の深さ R と生成された β-基 S の深さは、 dpt(R)=dpt((A⇀B)⇀C)dpt(S)=dpt(A⇀B) であり、 深さの定義から dpt(R)>dpt(S) である。

場合 2:2 番目のパターンは、 (λxA.(λyB.UC))QATB→β(λyB.U[xA:=QA]C)TB となり、 このとき、 dpt(R)=dpt(A⇀(B⇀C))dpt(S)=dpt(B⇀C) である。

場合 3:3 番目のパターンは、 (λxA⇀B.xA⇀B)(λyA.UB)TA→β(λyA.UB)TA であり、 dpt(R)=dpt((A⇀B)⇀(A⇀B))dpt(S)=dpt(A⇀B) となる。 これらの場合も、 深さの定義から dpt(R)>dpt(S) が成り立つ。

証明.

ラムダ項 M が β-正規形ではないとする。 M に部分項として含まれる β-基のうち、 その深さが最大のものの中で最も右にあるものを R とする。 ここで、 β-基 (λx.P)Q の位置は λ の位置で判断するものとする。 このとき、 M に含まれる R を簡約したものを red(M) と書くことにする。

M に含まれる R 以外の β-基のうち、 Q に含まれないものを S1,⋯,Sl とし、 Q に含まれるもの T1,⋯,Tm とする。 R による S1,⋯,Sl の残基はそれぞれ 1 つなので、 各 Si の残基を Si󰎘 とおく。 一方、 R による T1,⋯,Tm の残基は複数になり得る。 そこで、 各 Ti の残基を Ti1󰎘,⋯,Tiki󰎘 とおくことにする。 また、 R によって生成される red(M) 内の β-基を U1󰎘,⋯,Un󰎘 とする。 このとき、 red(M) に含まれる β-基は、 S1󰎘,⋯,Sl󰎘,T1󰎘,⋯,Tm󰎘,U1󰎘,⋯,Un󰎘 で全てである。

補題 10 より、 dpt(Si󰎘)=dpt(Si) また dpt(Tij󰎘)=dpt(Ti) である。 さらに、 各 Ti は Q に含まれているので、 R より右側にある。 R は最も右側にとっていたので、 dpt(Tij󰎘)=dpt(Ti)<dpt(R) が成り立つ。 また、 補題 11 より、 dpt(Ui󰎘)<dpt(R) も成り立つ。 したがって、 ord(red(M)) = l󰄚i=1ωdpt(Si󰎘)+m󰄚i=1ki󰄚j=1ωdpt(Tij󰎘)+n󰄚i=1ωdpt(Ui󰎘) ≤ l󰄚i=1ωdpt(Si)+m󰄚i=1ωdpt(Ti)+m󰄚i=1ki󰄚j=1ωdpt(Tij󰎘)+n󰄚i=1ωdpt(Ui󰎘) ≤ l󰄚i=1ωdpt(Si)+m󰄚i=1ωdpt(Ti)+m󰄚i=1ki󰄚j=1ωdpt(R)−1+n󰄚i=1ωdpt(R)−1 = l󰄚i=1ωdpt(Si)+m󰄚i=1ωdpt(Ti)+ωdpt(R)−1(k1+⋯+km+n) < l󰄚i=1ωdpt(Si)+m󰄚i=1ωdpt(Ti)+ωdpt(R) = ord(M) が分かる。

以上により、 β-簡約の列 M→βred(M)→βred(red(M))→β⋯ が無限に続くと仮定すると、 順序数の無限減少列 ord(M)>ord(red(M))>ord(red(red(M)))>⋯ を得るが、 これは不可能である。 これにより、 上記の β-簡約の列は有限回のうちに β-正規形で止まる。

証明.

任意にラムダ項 M をとる。 定理 13 により、 M は β-正規形 N をもつ。 η-簡約により β-基が新たに生じることはなく、 さらにラムダ項の長さは減少するので、 N から始まる η-簡約列は有限回のうちに βη-正規形 L で止まる。 M↠βN↠ηL であるから、 L は M の βη-正規形である。

証明.

初めに、 1 つ目の条件から 2 つ目の条件を導く。 これは n に関する帰納法による。

n=0 のときは、 証明すべきことはない。 n≥1 のとき、 任意に強計算可能なラムダ項 N1A1,⋯,NnAn をとる。 A󰎘≡A2⇀⋯⇀An⇀a とおくと A≡A1⇀A󰎘 である。 M は強計算可能だから、 強計算可能性の定義から MN1 も強計算可能である MN1 は型 A󰎘 だから、 帰納法の仮定により (MN1)N2⋯Nn は強計算可能である。 以上により 2 つ目の条件が示された。

逆に、 2 つ目の条件から 1 つ目の条件を導く。 これも n に関する帰納法による。

n=0 のときは、 証明すべきことはない。 n≥1 のとき、 A󰎘≡A2⇀⋯⇀An⇀a とおくと A≡A1⇀A󰎘 である。 任意に強計算可能なラムダ項 N1A1 をとる。 仮定から、 任意の強計算可能なラムダ項 N2A2,⋯,NnAn に対して (MN1)N2⋯Nn は強計算可能である。 MN1 は型 A󰎘 だから、 帰納法の仮定より MN1 は強計算可能である。 N1 は任意だったから、 強計算可能性の定義により M も強計算可能である。 以上により 1 つ目の条件が示された。

証明.

M のある部分項 N が強正規化可能でないとすると、 N から始まる無限の長さの β-簡約列が存在する。 これと同じ簡約を M から始めれば、 M から始まる無限の長さの β-簡約列が得られ、 M が強正規化可能であることに矛盾する。

証明.

M が正規化可能でないとすると、 M から始まる無限の長さの β-簡約列 M→βM1→βM2→β⋯ が存在する。 このとき、 M[x:=P]→βM1[x:=P]→βM2[x:=P]→β⋯ も正しい β-簡約列であるから、 M[x:=P] が強正規化可能であることに矛盾する。

証明.

A の構造に関する帰納法により、 2 つの主張を同時に示す。

A が原始型のとき。 M1,⋯,Mn が強正規化可能だとすると、 xM1⋯Mn も強正規化可能である。 xM1⋯Mn の型は原始型だから、 強計算可能性の定義により xM1⋯Mn は強計算可能である。 2 つ目の主張は、 強計算可能性の定義から明らかである。

A≡B⇀C のとき。 M1,⋯,Mn が強正規化可能であるとする。 さらに、 任意に強計算可能なラムダ項 NB をとる。 2 つ目の主張に関する帰納法の仮定により、 N は強正規化可能である。 1 つ目の主張に関する帰納法の仮定により、 xM1⋯MnN は強計算可能である。 N は任意だったから、 強計算可能性の定義により xM1⋯Mn は強計算可能である。

MA が強計算可能であるとする。 M に出現しない変項 xB を 1 つとると、 1 つ目の主張に関する帰納法の仮定によって x は強計算可能である。 したがって、 強計算可能性の定義から Mx も強計算可能である。 Mx は型 C だから、 2 つ目の主張に関する帰納法の仮定により、 Mx は強正規化可能である。 したがって、 補題 17 により、 その部分項である M も強正規化可能である。

証明.

A を A≡A1⇀⋯⇀An⇀a と表す。 また、 任意に強計算可能なラムダ項 N1A1,⋯,NnAn をとる。 M[x:=P] は強計算可能だから、 補題 16 によって M[x:=P]N1⋯Nn も強計算可能である。 M[x:=P]N1⋯Nn の型は原始型 a なので、 強計算可能性の定義により、 これは強正規化可能でもある。 したがって、 補題 17 によって、 その部分項である M[x:=P],N1,⋯,Nn は全て強正規化可能である。 さらに補題 18 により、 M も強正規化可能である。 また、 x∈FV(M) であれば M[x:=P] に P が部分項として含まれるから、 M[x:=P] が強正規化可能であることから P も強正規化可能である。 一方で x∉FV(M) であれば、 仮定によって P は強計算可能だから、 補題 19 を用いて P は強正規化可能でもある。 よって、 どちらの場合でも P は強正規化可能である。

以上により、 M[x:=P],M,P,N1,⋯,Nn は全て強正規化可能である。 もし (λx.M)PN1⋯Nn から始まる無限の長さの β-簡約列が存在したとすれば、 その全ての β-簡約が M,P,N1,⋯,Nn の中で行われることはない。 すなわち、 そのような無限の長さの β-簡約列は、 (λx.M)PN1⋯Nn ↠β (λx.M󰎘)P󰎘N1󰎘⋯Nn󰎘 →β M󰎘[x:=P󰎘]N1󰎘⋯Nn󰎘 →β ⋯ という形になっているはずである。 ここで、 M↠βM󰎘,P↠βP󰎘 などとおいている。 したがって、 この簡約列を用いて、 M[x:=P]N1⋯Nn ↠β M󰎘[x:=P󰎘]N1󰎘⋯Nn󰎘 →β ⋯ という無限の長さの β-簡約列を構成することができるが、 これは M[x:=P]N1⋯Nn が強正規化可能であることに矛盾する。 以上により、 (λx.M)PN1⋯Nn は強正規化可能である。 N1,⋯,Nn は任意だったから、 補題 16 によって (λx.M)P は強正規化可能である。

証明.

M の構造に関する帰納法による。

場合 1:ある i について M≡xi のとき。 このとき、 󰂡M≡Pi である。 仮定から Pi は強計算可能なので、 󰂡M も強計算可能である。

場合 2:M≡y であって y はどの xi とも等しくないとき。 このとき、 󰂡M≡y であるから、 補題 19 によって M は強計算可能である。

場合 3:M≡UV のとき。 このとき、 󰂡M≡󰂡U󰂡V であり、 帰納法の仮定から 󰂡U と 󰂡V はともに強計算可能である。 したがって、 強計算可能性の定義より 󰂡M も強計算可能である。

場合 4:M≡λyB.UC のとき。 M に適当な α-変換を施して、 y は x1,⋯,xn,P1,⋯,Pn のいずれにも自由に出現しないものとする。 すると、 󰂡M≡λy.󰂡U が成り立つ。

任意に強計算可能なラムダ項 NB をとる。 ここで、 󰂡MN ≡ (λy.󰂡U)N →β 󰂡U[y:=N] ≡ U[xn:=Pn]⋯[x1:=P1][y:=N] であるが、 N,P1,⋯,Pn は強計算可能であって、 各 i で y∉FV(Pi) だから、 帰納法の仮定が適用できて、 上式の最右辺は強計算可能である。 したがって、 補題 20 によって (λy.󰂡U)N≡󰂡MN も強計算可能である。

証明.

任意にラムダ項 M をとると、 補題 21 において、 n=1 として P1≡x1 とすれば 󰂡M≡M だから、 M が強計算可能である。 したがって、 補題 19 により M は強正規化可能である。

証明.

上記の定理 22 の証明において、 β-簡約に関する強正規化可能性を βη-簡約に関する強正規化可能性だと思って読めば、 そのままそれが証明として成立する。 ただし、 補題 20 の証明だけは以下の修正を要する。

補題 20 の証明において、 (λx.M)PN1⋯Nn から始まる無限の長さの βη-簡約列は、 上の証明で述べた形の他に、 (λx.M)PN1⋯Nn ↠βη (λx.M󰎘)P󰎘N1󰎘⋯Nn󰎘 ≡ (λx.Tx)P󰎘N1󰎘⋯Nn󰎘 →η TP󰎘N1󰎘⋯Nn󰎘 →βη ⋯ という形があり得る。 ここで、 M󰎘≡Tx かつ x∉FV(T) であり、 M↠βηM󰎘,P↠βηP󰎘 などとおいている。 この場合は、 M[x:=P]N1⋯Nn ↠βη M󰎘[x:=P󰎘]N1󰎘⋯Nn󰎘 ≡ TP󰎘N1󰎘⋯Nn󰎘 →βη ⋯ という無限の長さの βη-簡約列が構成できるので、 同様に矛盾する。 残りの証明の部分は、 上で述べた通りである。

証明.

Barendregt†1 の定理 11.3.4 を参照。

証明.

M→βK∘X→βIβK+N であるとき、 あるラムダ項 Y によって M→βIβK+Y→βK∘N とできることを示せば、 これによって βK∘-簡約を次々と後に移動させることができるので、 補題の主張が示される。 以下、 M→βK∘X のときに簡約された β-基を R≡(λx.P)Q とし、 X→βIβK+N のときに簡約された β-基を S≡(λy.U)V とする。

βK∘-簡約によって、 新たな β-基が生成されることはない。 実際、 補題 7 の 3 パターンのうちどれを見ても、 簡約されている β-基が βK∘-基になることはできない。 したがって、 S は M に含まれるある β-基 S󰎘 の残基である。 R と S󰎘 の位置関係によって場合分けする。

場合 1:R と S󰎘 が別の位置にあるとき。 このとき、 S󰎘≡S である。 また、 R の簡約により S は変化せず、 S の簡約によっても R は変化しないから、 M において先に S を簡約したものを Y とすれば、 Y にそのまま含まれている R を簡約すると N になる。 このとき、 M→βIβK+Y→βK∘N であるから、 主張が示された。

場合 2:S󰎘 が R を含むとき。 このとき、 M≡X[S󰎘],S󰎘≡Y[R] と書け、 N≡C[U[y:=V]] である。 R≡(λx.P)Q は βK∘-基なので x∉FV(P) であるから、 R を簡約すると P になる。 したがって、 S󰎘 の残基が S なので、 S≡Y[P] が成り立つ。 P の型は原始型だから P≡S となることはないので、 P は U か V のどちらかに含まれる。 これに応じてさらに場合分けをする。

P が U に含まれているときは、 U≡Z[P] と書ける。 このとき、 S≡(λy.Z[P])V であるから S󰎘≡(λy.Z[R])V が分かる。 したがって、 M≡X[S󰎘] であったから、 Y≡X[E[R][y:=V]] とおけば、 S を簡約することで M→βIβK+Y が成り立つ。 また、 Y に含まれる R を簡約することで Y→βK∘X[E[P][y:=V]] となるが、 U≡Z[P] および N≡C[U[y:=V]] なので、 Y→βK∘N である。 以上で、 主張が示された。

また、 P が V に含まれているときは、 V≡Z[P] と書ける。 このとき、 S≡(λy.U)Z[P] であるから S󰎘≡(λy.U)Z[R] が分かる。 したがって、 Y≡X[U[y:=E[R]]] とおけば、 上の場合と同様にして M→βIβK+Y→βK∘N が成り立つ。

場合 3:R が S󰎘 を含むとき。 S󰎘 は P か Q のどちらかに含まれるが、 R を簡約すると Q は消えるので、 S󰎘 が Q に含まれているとすると S󰎘 の残基は存在せず矛盾する。 したがって、 S󰎘 は P に含まれる。 また、 R の簡約により P は変化しないので、 S󰎘≡S である。 以上により、 M≡X[R],P≡Y[S] と書ける。

S󰎙≡U[y:=V] とおく。 M≡X[(λx.Y[S])Q] だから、 Y≡X[(λx.Y[S󰎙])Q] とおけば S の簡約により M→βIβK+Y が成り立つ。 x∉FV(P)=FV(Y[S]) であり、 簡約によって自由変項は増加しないので、 x∉FV(Y[S󰎙]) である。 したがって、 Y に含まれる (λx.Y[S󰎙])Q を簡約することで Y→βK∘X[Y[S󰎙]] を得る。 N≡X[Y[S󰎙]] だから Y→βK∘N となり、 主張が示された。

証明.

まず、 󰒯 = {N∣M↠βN} 󰒰1 = {Y∣M↠βIβK+Y} 󰒰2(Y) = {N∣Y↠βK∘N} とおく。

M は単純だから、 M に含まれる β-基は βI-基か βK∘-基のどちらかである。 βI-簡約によって βK+-簡約が生じることはないので、 M↠βIβK+Y ならば M↠βIY である。 補題 29 により、 M から始まる全ての βI-簡約列は有限の長さなので、 M↠βIY を満たす Y は有限個しかない。 したがって、 󰒰1 は有限集合である。

また、 βK∘-簡約はラムダ項の長さを真に小さくするので、 無限の長さの βK∘-簡約列は作られ得ない。 したがって、 󰒰2(Y) も有限集合である。

ここで、 任意の N∈󰒯 に対し、 補題 27 によってあるラムダ項 Y が存在して、 M↠βIβK+Y↠βK∘N が成り立つ。 すなわち、 Y∈󰒰1 および N∈󰒰2(Y) が成り立つ。 これにより、 󰒯⊆󰆊Y∈󰒰1󰒰2(Y) が示された。 ここで、 上に示したように 󰒰1 と 󰒰2(Y) は全て有限集合なので、 上式の右辺も有限集合である。 したがって、 その部分集合である 󰒯 も有限集合である。