Avendia19
English

初めに

以下で扱う型は、 全て Church 式の単純型とする。 すなわち、 ラムダ項の各変項にはちょうど 1 つの型が定められており、 正しく型付けできない項は初めから排除する。 なお、 原始型は 1 個でも無限個でも良い。

x,y,z, などのラテン小文字後半はラムダ項の変項を表し、 M,N,P, などのラテン大文字後半はラムダ項を表す。 a,b,c, などのラテン小文字前半は原始型定数を表し、 A,B,C, などのラテン小文字前半は型を表す。 また、 変項やラムダ項の型を明示して、 xAMAB などと書くことがある。

あるラムダ項 X に部分項として P が出現しているとき、 それを X[P] で表す。 このとき、 出現 P (位置を区別する) を別のラムダ項 Q にそのまま置き換えたものを X[Q] と書く。 例えば、 X[λx.xy](λz.(λx.xy))(λw.w) とおくとき、 X[z](λz.z)(λw.w) である。 ラムダ項の置き換えにより、 z が新たに束縛されていることに注意すること。

なお、 このノートのテーマである正規化可能性とは、 以下で定義される性質である。

定義 1

ラムダ項 M に対し、 MβN であって Nβ-正規形であるようなラムダ項 N が存在するとき、 Mβ-弱正規化可能weakly normalisable であるという。 βη-弱正規化可能であることも同様に定義される。

定義 2

ラムダ項 M に対し、 M から始まる任意の β-簡約の列 MβN1βN2β は必ず有限回のうちに β-正規形で止まるとき、 Mβ-強正規化可能strongly normalisable であるという。 βη-強正規化可能であることも同様に定義される。

弱正規化定理

以下の証明は、 各ラムダ項に順序数を割り当て、 特定の方法で簡約を行うとその順序数が真に減少することを利用するものである。 そのために、 β-簡約によって β-基がどのように消えたり生まれたりするかを詳しく調べる。 この証明は、 Barendregt2 および Lévy1 を参考にした。

なお、 この節では単に β-基と言ったらその β-基の出現のことであるとする。 したがって、 同じ形の β-基でも場所が異なるものは別物だと見なす。

定義 3

ラムダ項 M に含まれる β-基 R(λx.P)QR󰎘P[x:=Q] に簡約して得られるラムダ項を N とする。 また、 M に含まれる β-基 S をとる。 このとき、 R による S残基residue を以下によって定義する。

RS が同じであるとき。 このときは、 S の残基は存在しない。

RS が別の位置にあるとき。 このとき、 R の簡約により S は変化しないので、 S はそのまま N に部分項として含まれる。 この N に含まれる出現 S を、 S の残基とする。

SR を含むとき。 MX[S],SY[R] と書けるから、 NX[Y[R󰎘]] と書ける。 S󰎘Y[R󰎘] とおくと NX[S󰎘] となるが、 このような出現 S󰎘S の残基とする。

RS を含み、 特に PS を含むとき。 MX[R],PY[S] と書けるから、 R󰎘Y[S][x:=Q] である。 したがって、 S󰎘S[x:=Q] とおくと NX[Y[S󰎘][x:=Q]] となるが、 このような出現 S󰎘S の残基とする。

RS を含み、 特に QS を含むとき。 MX[R],QY[S] と書けるから、 NX[P[x:=D[S]]] と書ける。 この P[x:=D[S]] に含まれる S の形をした出現 (複数個もしくは 0 個になり得る) を、 S の残基とする。

残基については一般論を見るよりは具体例を見るのが分かりやすいので、 各場合におけるシンプルな例を 1 つずつ挙げておく。 RS が別の位置にあるときというのは、 ((λx.xy)xR)((λz.xz)zSw)β(xy)((λz.xz)zS の残基w) などの場合である。 SR を含むときというのは、 (λy.R(λx.xy)x)zSwβ(λy.xy)zS の残基w などである。 R(λx.P)QPS を含むときは、 R(λx.(λy.y)xSw)zβ(λy.y)zS の残基w などの場合である。 最後に、 R(λx.P)QQS を含むときは、 R(λx.wxx)((λy.y)zS)βw((λy.y)zS の残基)((λy.y)zS の残基) などである。 このときは、 P に出現する x の個数分だけ残基が生じる。

β-基 R を簡約することで、 すでに存在していた別の β-基 S が変形する可能性があるが、 その変形した結果というのが S の残基であると解釈できる。 一方、 β-基の簡約によって、 全く新しい β-基が生じることもある。

定義 4

ラムダ項 M に含まれる β-基 R を簡約して得られるラムダ項を N とする。 このとき、 N に含まれる β-基であって、 M に含まれるどんな β-基の残基でもないようなものを、 R によって生成された基created redex という。

3 つほど例を挙げる。 簡約 (λx.X[xT])(λy.U)βX[(λy.U)T] では、 (λx.X[xT])(λy.U) の簡約により (λy.U)T が生成されている。 次に、 (λx.(λy.U))QTβ(λy.U[x:=Q])T では、 (λx.(λy.U))Q の簡約により (λy.U[x:=Q])T が生成されている。 最後に、 (λx.x)(λy.U)Tβ(λy.U)T では、 (λx.x)(λy.U) の簡約により (λy.U)T が生成されている。

さて、 β-簡約により新たに β-基が生成されるパターンを 3 つ挙げたが、 実は β-基が生成されるときは必ずこの 3 パターンのどれかになる。 このことを以下に 2 つの補題を示しながら証明する。

補題 5

ラムダ項 M に含まれる β-基 R(λx.P)Q を簡約して得られるラムダ項を N とする。 Mβ-基でなく Nβ-基であるとすると、

のどちらか一方である。

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

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

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

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

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

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

補題 6

ラムダ項 M,N を考える。 Mβ-基でなく M[x:=N]β-基であるとすると、

のどちらか一方である。

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

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

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

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

補題 7

β-簡約により新たな β-基が生成されるとき、 その β-簡約について、

のいずれかである。

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

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

場合 2:SR󰎘 を含むとき。 MZ[S󰎘] となるような S󰎘 がある。 このとき、 S󰎘 には R が含まれ、 この R を簡約すると S になる。 また、 S󰎘β-基だとすると SS󰎘 の残基になってしまい矛盾するので、 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 かつ Px,Qλy.U となるときは、 M Z[(λx.x)(λy.U)T] N Z[(λy.U)T] となり、 補題の主張の 3 番目のパターンになる。

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

以上によって、 β-基の簡約により、 それ以外の β-基がどう変化し、 またどのような β-基が生成されるかが分かった。

さて、 型の複雑度を測る一種の指標として、 深さの概念を導入する。

定義 8

A に対し、 dpt(A) を以下によって再帰的に定義する。 dpt(a) = 1 dpt(AB) = max(dpt(A),dpt(B))+1 このとき、 dpt(A)A深さdepth という。

定義 9

β-基 R(λxA.PB)QA に対し、 dpt(R)=dpt(AB) と定義し、 dpt(R)R深さdepth という。

補題 10

ラムダ項 M に含まれる β-基 R を簡約することを考える。 M に含まれる β-基 S をとり、 R による S の残基の 1 つを S󰎘 とする。 このとき、 SS󰎘 について、 その全体の型と束縛変項の型は等しい。 特に dpt(S)=dpt(S󰎘) である。

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

補題 11

あるラムダ項に含まれる β-基 R を簡約した結果、 β-基 S が生成されたとする。 このとき、 dpt(R)>dpt(S) が成り立つ。

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

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

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

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

以下では順序数を扱うが、 順序数の和については、 表記の順番に関わらず ω の指数が大きいものから順に和をとることにする。 例えば、 ω2+ω3+ω3 と書かれていても ω3+ω3+ω2=ω32+ω2 のことであると解釈する。

定義 12

ラムダ項 M に対し、 順序数 ord(M) を、 ord(M)=󰄚Rωdpt(R) と定義する。 なお、 和は M に部分項として出現する全ての β-基 R を回るものとする。

例えば、 M(λyaaa.yaaa((λxa.xa)xa)((λxa.xa)xa))yaaa に含まれる β-基は、 R1 (λyaaa.yaaa((λxa.xa)xa)((λxa.xa)xa))yaaa R2 (λxa.xa)xa の 2 種類だが、 R2 は 2 回出現しているので、 ord(M) = ωdpt(R1)+ωdpt(R2)+ωdpt(R2) = ωdpt((aaa)a)+ωdpt(aa)+ωdpt(aa) = ω4+ω22 となる。

以上の準備により、 任意のラムダ項が正規形をもつことが示される。

定理 13 [弱正規化定理 weak normalisation theorem]

任意の型付きラムダ項は β-弱正規化可能である。

ラムダ項 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) である。 さらに、 各 TiQ に含まれているので、 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)))> を得るが、 これは不可能である。 これにより、 上記の β-簡約の列は有限回のうちに β-正規形で止まる。

定理 14 [弱正規化定理 weak normalisation theorem]

任意の型付きラムダ項は βη-弱正規化可能である。

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

強正規化定理 (Tait)

以下の証明は、 強正規化可能性と似た強計算可能性というクラスを考え、 それについて調べることで強正規化定理を示すものである。 この証明は、 Tait による証明を修正したもので、 その証明の流れは Hindley4 を参考にした。

なお、 β-簡約に関する強正規化定理を示すまでは、 単に強正規化可能と言ったら β-簡約に関して強正規化可能であることとする。 すなわち、 そのラムダ項から始まるどんな β-簡約列も有限のうちに β-正規形で止まることを意味する。

まず初めに、 強計算可能性を定義する。

定義 15

ラムダ項 M強計算可能 strongly computable であることを、 以下によって型に関して再帰的に定義する。

補題 16

AAA1Ana(n0) と表す。 このとき、 ラムダ項 MA に対して 2 つの条件

は同値である。

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

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

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

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

次に、 強正規化可能性についての補題をいくつか用意しておく。

補題 17

ラムダ項 M が強正規化可能ならば、 M の任意の部分項も強正規化可能である。

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

補題 18

ラムダ項 M,P に対し、 M[x:=P] が強正規化可能ならば、 M も強正規化可能である。

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

以下の補題により、 強計算可能性と強正規化可能性が結びつく。

補題 19

A に対し、 2 つの主張

がともに成り立つ。

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

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

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

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

補題 20

ラムダ項 MA[xB:=PB] について、 2 つの条件

がともに成り立っているならば、 (λx.M)P は強計算可能である。

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

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

補題 21

ラムダ項 MA を考える。 任意の変項 x1B1,,xnBn と任意のラムダ項 P1B1,,PnBn に対し、 P1,,Pn は強計算可能であり、 各 ix1,,xi1FV(Ni) が成り立っているとする。 このとき、 󰂡MM[xn:=Pn][x1:=P1] は強計算可能である。 なお、 n1 とする。

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

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

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

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

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

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

定理 22 [強正規化定理 strong normalisation theorem]

任意の型付きラムダ項 は β-強正規化可能である。

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

定理 23 [強正規化定理 strong normalisation theorem]

任意の型付きラムダ項は βη-強正規化可能である。

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

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

強正規化定理 (Statman)

以下の証明は、 上で述べた弱正規化定理の証明と同じように、 β-簡約および η-簡約によってラムダ項がどのように変わるかを詳細に調べることによって行うものである。 前項で述べた Tait の証明のようなテクニカルな部分はないが、 単純型以外の他の型理論への応用が狭いという難点がある。 以下に述べる証明は Statman による証明を修正したもので、 その証明の流れは Barendregt2 を参考にした。

まず、 β-簡約について詳しく調べるため、 β-基をいくつかに分類する。

定義 24

β-基 R(λx.P)Q を考える。 xFV(P) であるとき RβI-redex といい、 xFV(P) であるとき RβK-という。

定義 25

β-基 R(λx.P)Q を考え、 これが βK-基であるとする。 xP の型がともに原始型であるとき RβK-といい、 そうでないとき βK+-という。

ββ-基の簡約を表すのと同じように、 基の名前を矢印の右下に書いてその種類の基の 1 回の簡約を表す。 例えば βIβI-基の 1 回の簡約を表し、 βKβK-基の 1 回の簡約を表す。 また、 βIβK+βI-基もしくは βK+-基の 1 回の簡約を表すものとする。 さらに、 に変えたものは、 その簡約を複数回 (0 回も可) 行ったことを表す。

βI-簡約については、 以下の定理が知られている。

定理 26 [保存定理conservation theorem]

ラムダ項 M,N に対し、 MβIN であるとする。 このとき、 M から始まる無限の長さの βI-簡約が存在するならば、 N から始まる無限の長さの βI-簡約も存在する。

Barendregt1 の定理 11.3.4 を参照。

補題 27

ラムダ項 M,N に対し、 MβN が成り立っているならば、 あるラムダ項 Y が存在して MβIβK+YβKN が成り立つ。

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

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

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

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

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

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

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

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

一般のラムダ項を調べる前に、 しばらく以下のような特殊なラムダ項について考える。

定義 28

ラムダ項 M に含まれる λx.P という形の部分項について、 xFV(P) であるか xP の型がともに原始型であるとする。 このとき、 M単純simple であるという。

補題 29

ラムダ項 M が単純ならば、 MβI-強正規化可能である。

補題 30

ラムダ項 M が単純ならば、 {NMβN} は有限集合である。

まず、 󰒯 = {NMβN} 󰒰1 = {YMβIβK+Y} 󰒰2(Y) = {NYβKN} とおく。

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βKN が成り立つ。 すなわち、 Y󰒰1 および N󰒰2(Y) が成り立つ。 これにより、 󰒯󰆊Y󰒰1󰒰2(Y) が示された。 ここで、 上に示したように 󰒰1󰒰2(Y) は全て有限集合なので、 上式の右辺も有限集合である。 したがって、 その部分集合である 󰒯 も有限集合である。

補題 31

循環する β-簡約の列 MβM1βM2ββMnβM は存在しない。

補題 32

ラムダ項 M に対し、 M が単純ならば Mβ-強正規化可能である。

補題 33

ラムダ項 M,N,X に対し、 MηXβ+N が成り立っているならば、 あるラムダ項 Y が存在して Mβ+YηN が成り立つ。 なお、 β+ は 1 回以上の β-簡約を表す。

Barendregt1 の系 15.1.6 を参照。

補題 34

ラムダ項 M に対し、 M が単純ならば Mβη-強正規化可能である。

定理 35 [強正規化定理 strong normalisation theorem]

任意のラムダ項は βη-強正規化可能である。

M に含まれる RλxA.PB という形の部分項を考える。 まず、 A A1Ama B B1Bnb と表し、 R󰎘λxA.λy1B1ynBn.(λza.Py1B1ynBn)(xAu1A1umAm) とおく。 ここで、 y1,,yn,u1,,um,zM に含まれていない新たな変項であるとする。 このとき、 R󰎘βηR が成り立ち、 R󰎘 は単純である。 したがって、 M に含まれる全ての Rλx.P に対して上記のような R󰎘 を作り、 各 RR󰎘 に置き換えたものを M󰎘 とすれば、 M󰎘βηM であって、 M󰎘 は単純である。 補題 34 により、 M󰎘βηMβηM1βηM2βη という列は有限回で止まるから、 定理の主張が従う。

参考文献

  1. H. P. Barendregt (1984) 『The Lambda Calculus: Its Syntax and Semantics』 North Holland
  2. H. P. Barendregt, W. Dekkers, R. Statman (2013) 『Lambda Calculus with Types』 Cambridge University Press
  3. J. J. Lévy (1978) 「Réductions correctes et optimales dans le lambda-calcul」 Ph. D. thesis, Université de Paris VII
  4. J. R. Hindley, J. P. Seldin (2008) 『Lambda-Calculus and Combinators: an Introduction』 Cambridge University Press