§E15.8型なしラムダ計算

証明. アルファ同値類上の演算を仮定して証明すると循環するため、最初にアルファ同値で商を取る前の項に対して代入の候補を定める。$\mathcal S_x(A,N)$を、上の再帰規則を用いて$A$へ$N$を代入するときに得られる項の集合とする。改名が必要な抽象では、条件を満たす新しい変数の全てを許す。示すべき最初の主張は、

である。

この主張を証明するため、項の大きさに関する強い構造帰納法によって、次の三つの主張を同時に示す。

1. $\mathcal S_x(A,N)$の任意の二項はアルファ同値である。
2. $b\notin\operatorname{Var}(A)\cup\{a\}$かつ$c\notin\operatorname{Var}(A)\cup\{a,b\}$のとき、新鮮な変数による改名には $$\rho_{b\to c}\bigl(\rho_{a\to b}(A)\bigr) =\rho_{a\to c}(A) \tag{2}$$ という合成則が成り立つ。また、$a\ne d$、$b\notin\operatorname{Var}(A)\cup\{a,d\}$、$e\notin\operatorname{Var}(A)\cup\{a,d,b\}$のとき、 $$\rho_{a\to b}\bigl(\rho_{d\to e}(A)\bigr) = \rho_{d\to e}\bigl(\rho_{a\to b}(A)\bigr)$$ である。
3. $R\in\mathcal S_x(A,N)$、$a\ne x$、$a\notin\operatorname{FV}(N)$とする。さらに $$b\notin \operatorname{Var}(A)\cup\operatorname{Var}(N)\cup \operatorname{Var}(R)\cup\{a,x\} \tag{3}$$ とする。このとき、ある$R_b\in\mathcal S_x(\rho_{a\to b}(A),N)$が存在して $$\rho_{a\to b}(R)\equiv_\alpha R_b \tag{4}$$ となる。すなわち、新鮮な改名と代入はアルファ同値を除いて交換する。

各大きさでは、最初に改名則、次に代入結果の選択独立性、最後に改名と代入の交換を示す。この順序なら、同じ大きさの主張を循環して用いない。改名の合成則と交換則は、変数では定義を直接比較し、適用では二つの部分項へ帰納法の仮定を適用する。抽象$\lambda u.A_0$では、改名する変数が$u$ならば両辺の改名が同じ抽象で遮蔽される。そうでなければ改名は本体へ入り、$A_0$に対する帰納法の仮定から結論を得る。

代入結果の選択独立性を示す。変数の場合には候補が一つしかない。適用$A_1A_2$の場合には、二つの部分項に対する帰納法の仮定を用いる。抽象の束縛変数が$x$ならば代入は遮蔽され、候補はもとの抽象だけである。$A=\lambda y.A_0$、$y\ne x$、$y\notin\operatorname{FV}(N)$ならば、全ての候補は$\lambda y.R_0$の形であり、本体の候補は帰納法の仮定によってアルファ同値である。

$y\in\operatorname{FV}(N)$のため改名が必要な場合を考える。二つの新しい変数を$z,z'$とし、対応する本体の候補を

とする。ここで、共通の新しい変数$w$を

となるように選ぶ。元の項だけでなく、再帰によってすでに得た二つの本体に現れる全変数も避けているため、外側の束縛変数を$w$へ改名するアルファ変換は正当である。小さい項$\rho_{y\to z}(A_0)$に対する改名と代入の交換から、$\rho_{z\to w}(R_z)$は

のある要素とアルファ同値である。改名の合成則 (2) により、この集合は

である。$z'$に対しても同じ結論を得る。この共通の集合の候補は、小さい項に対する選択独立性によってアルファ同値である。従って、

である。変数、適用、遮蔽される抽象、安全な抽象、および改名を必要とする抽象について得た同時帰納法の結論から、 (1) を得た。

改名と代入の交換も同じ場合分けで示す。変数と適用の場合は再帰式から直接従う。抽象の束縛変数が$x$ならば代入は両側で遮蔽される。安全な抽象$\lambda y.A_0$では、$y=a$ならば改名もその抽象で遮蔽され、$y\ne a$ならば本体に対する帰納法の仮定を用いる。

改名を必要とする抽象では$y\in\operatorname{FV}(N)$である一方、$a\notin\operatorname{FV}(N)$なので$y\ne a$である。候補を作るときに選ばれた新しい変数を$z$とする。$z=a$ならば、新鮮性から$a$は$A_0,N$に現れず、外側の$\lambda a$が改名を遮蔽するため、改名前と同じ$z=a$を用いた候補を改名後にも選ぶことができる。$z\ne a$ならば、条件 (3) により$z\ne b$でもある。改名後にも同じ$z$を選び、より小さい項$\rho_{y\to z}(A_0)$へ帰納法の仮定を適用する。相異なる変数に対する新鮮な改名の交換則から

であるため、得られる本体は改名後の抽象に対する代入候補である。変数、適用、および三種類の抽象に対する場合分けにより、(4) も全ての構文の場合について示された。同じ改名則をアルファ同値の生成規則へ適用すると、捕獲を起こさない自由変数の改名もアルファ同値を保つ。改名生成規則では合成則と交換則を用い、文脈閉包と同値関係の規則では同じ規則を保つことから従う。

変数、適用、および三種類の抽象に対して行った同時帰納法から、特に$x\notin\operatorname{FV}(A)$ならば

も構造帰納法で従う。改名を必要とする抽象でも、改名後の本体へ帰納法の仮定を適用し、最後に外側のアルファ変換を戻せばよい。

ここまでの議論はアルファ同値で商を取る前の項だけを用いており、代入がアルファ同値類上で定まることを仮定していない。そこで、$A[x:=N]$を$\mathcal S_x(A,N)$の任意の要素のアルファ同値類として定める。(1) により、この定義は新しい変数の選択によらない。

次に、項$A$の代表元によらないことを示す。アルファ同値の改名生成規則

を考える。$x=y$または$x=z$の場合には、一方では代入が外側の抽象で遮蔽され、他方では$x$が本体に自由に現れない。(6) により、代入後の両項は (7) の両辺とそれぞれアルファ同値である。

$x\notin\{y,z\}$とする。両辺から選んだ代入候補の本体に現れる変数も含めた有限集合を避けて、新しい変数$w$を選ぶ。左辺では、$y\in\operatorname{FV}(N)$ならば代入時の改名に$w$を選び、$y\notin\operatorname{FV}(N)$ならば代入後の外側の$y$を$w$へ改名する。改名と代入の交換により、どちらの場合にも結果は

とアルファ同値である。右辺でも同様に外側の$z$を$w$へそろえる。改名の合成則

により、右辺からも (8) の形を得る。(1) によって (8) の本体の選択は結果を変えないので、改名生成規則は代入によって保たれる。

アルファ同値の導出を文脈へ広げる段階も確認する。適用の文脈では、変化する部分項へ導出に関する帰納法の仮定を適用する。抽象$\lambda u.Q$の文脈では、$u=x$ならば代入は両項で遮蔽される。$u\ne x$ならば、二つの本体、$N$、および再帰で得た本体の候補に現れる変数を全て避ける共通の新しい変数$v$を選ぶ。$u\notin\operatorname{FV}(N)$の場合も外側の束縛変数を$v$へアルファ変換してから比較してよい。自由変数の改名がアルファ同値を保つことから、改名後の二つの本体にも導出に関する帰納法の仮定を適用することができる。従って、両方の代入結果は共通の$\lambda v$の本体の下でアルファ同値になる。反射性、対称性、推移性については$\equiv_\alpha$が同値関係であることを用いる。従って、

である。

最後に、$N\equiv_\alpha N'$ならば$A[x:=N]\equiv_\alpha A[x:=N']$であることを、$A$の構文に関する帰納法で示す。アルファ同値な項は自由変数集合が等しい。従って、抽象の束縛変数が代入項に自由に現れるかどうかの判定は$N,N'$で一致する。変数と適用の場合は直ちに従い、束縛変数が$x$である抽象では両代入が遮蔽される。安全な抽象では本体へ帰納法の仮定を適用する。改名が必要な抽象では、

となる共通の新しい変数$z$を選び、$\rho_{y\to z}(A_0)$に対する帰納法の仮定を用いる。変数、適用、遮蔽される抽象、安全な抽象、および改名を必要とする抽象の各場合を検討した。(9) と代入項の変更に対する結論を推移性で結べば、二つの引数を同時にアルファ同値な代表元へ変えても結果は変わらない。従って、代入はアルファ同値類上の演算として定まる。▨

証明.$M$の構文に関する帰納法を用いる。$M=x$の場合には両辺が$N[y:=P]$になり、$M=y$の場合には、条件$x\notin\operatorname{FV}(P)$により両辺が$P$になる。それ以外の変数の場合には両辺はその変数のままである。適用の場合には、二つの部分項へ帰納法の仮定を適用する。

$M=\lambda z.M_0$とする。アルファ同値類上で代入を扱っているので、

となるように、外側の束縛変数をあらかじめ改名してよい。このとき、どちらの辺でも代入は抽象の内側へ入り、比較すべき本体は

になる。両者は帰納法の仮定によってアルファ同値である。変数、適用、抽象の三つの構文形について等式を示した。▨

証明.$M$の構文に関する帰納法を用いる。変数の場合には第1規則を用いる。抽象の場合には帰納法の仮定と第2規則を用い、適用の場合には二つの部分項に対する帰納法の仮定と第3規則を用いる。▨

証明. 代入の再帰で新たに選ぶ束縛変数については、$b$も避けた代表元を用いる。各再帰で避ける集合は有限であり、そのような代表元を選ぶことができる。代入の適切性と、同じ証明ですでに示した自由変数の改名によるアルファ同値の保存により、この代表元の選択は結論に影響しない。

最初に (10) を$A$の構文に関する帰納法で示す。$A=x$の場合には、$a=x$でも$a\ne x$でも両辺は$\rho_{a\to b}(B)$である。$A=a\ne x$の場合には両辺は$b$であり、それ以外の変数の場合には改名と代入の定義を直接比較すれば両辺が一致する。適用の場合には、二つの部分項に帰納法の仮定を適用する。

$A=\lambda u.A_0$の場合には、

となるアルファ同値な代表元を最初に選ぶ。この選択では、代入と改名がともに抽象の本体へ入る。$A_0$に対する帰納法の仮定へ抽象の文脈を加えると (10) を得る。もとの束縛変数が$a$または$x$である場合も、外側の束縛変数を先に新鮮な$u$へ変更した同じ比較に含まれる。

(11) も$A$の構文に関する帰納法で示す。$A=x$では両辺が$B$になり、$A\ne x$である変数では両辺がその変数になる。適用では二つの帰納法の仮定を用いる。抽象では、束縛変数を$\operatorname{Var}(B)\cup\{b,x\}$の外へ先に変更すると、両辺の代入が本体へ入り、本体に対する帰納法の仮定から結論を得る。したがって、二つの恒等式はアルファ同値で商を取る前の代表元の選択に依存せず成り立つ。▨

証明.$\mathcal D$の最後の規則に関する帰納法を用いる。

変数規則の結論が$u\Rightarrow_\beta u$であるとする。$u=a$ならば改名後の結論は$b\Rightarrow_\beta b$であり、$u\ne a$ならば$u\Rightarrow_\beta u$のままである。いずれも変数規則から従う。

抽象規則の結論を

とする。$u=a$ならば、改名は両方の抽象の本体へ入らないため、もとの前提$P\Rightarrow_\beta P'$へ抽象規則を適用すればよい。$u\ne a$ならば、$b$の新鮮性から$u\ne b$でもある。前提の導出に対する帰納法の仮定

へ抽象規則を適用すると、改名後の結論を得る。

第3規則の結論を$PQ\Rightarrow_\beta P'Q'$とする。二つの前提の導出へ帰納法の仮定を適用し、得られた二つの平行簡約へ第3規則を適用すればよい。

第4規則の結論を

とする。ただし、$P\Rightarrow_\beta P'$かつ$Q\Rightarrow_\beta Q'$である。$u=a$の場合には、もとの第1前提と、第2前提に対する帰納法の仮定を第4規則へ入れて

を得る。(10) の第1の場合により、右辺は$\rho_{a\to b}(P'[a:=Q'])$とアルファ同値である。

$u\ne a$の場合には、$u\ne b$であり、二つの前提に対する帰納法の仮定から

を得る。(10) の第2の場合により、右辺は$\rho_{a\to b}(P'[u:=Q'])$とアルファ同値である。平行簡約はアルファ同値な代表元を同一視して定義されているため、$u=a$と$u\ne a$の場合で得た関係はいずれも求める結論になる。変数規則、抽象規則、適用規則、β基規則の四規則を確認した。▨

証明. 改名保存補題を$P\Rightarrow_\beta P'$と自由変数の改名$\rho_{x\to z}$へ適用し、得られた平行簡約へ抽象規則を適用すると (12) を得る。同じ改名保存補題と$Q\Rightarrow_\beta Q'$を第4規則へ適用すると (13) を得る。(14) は補題 4.3の (11) である。したがって、抽象規則でも第4規則でも、束縛変数を導出の両辺で同時に新鮮な名前へ変更することができる。▨

証明.$M\Rightarrow_\beta M'$の導出に関する帰納法を用いる。

変数の場合を考える。$M=x$ならば、示すべき関係は仮定$N\Rightarrow_\beta N'$そのものである。$M=y\ne x$ならば、両辺は$y$であり、平行簡約の第1規則を用いる。

抽象の規則から導かれた場合を考える。系 4.5により、抽象の束縛変数$y$を導出の両辺で同時に

となるように変更することができる。改名後の二つの本体も$M_0,M_0'$と書く。本体に対する帰納法の仮定と抽象の規則から、

を得る。この平行簡約が求める関係である。

適用の第3規則から導かれた場合には、二つの前提へ帰納法の仮定を適用し、得られた二つの平行簡約へ第3規則を適用する。

最後に、第4規則から

が導かれている場合を考える。ただし、$P\Rightarrow_\beta P'$かつ$Q\Rightarrow_\beta Q'$である。系 4.5により、束縛変数$y$を導出の両辺で同時に変更し、$y$が$x$と異なり、$N,N',P,P',Q,Q'$に現れる必要な有限個の変数を避けるようにする。改名後の本体も$P,P'$と書く。この変更後の二つの前提へ帰納法の仮定を適用すると、

である。したがって、第4規則から

を得る。$y\notin\operatorname{FV}(N')$であるから、代入の合成補題により最後の項は

とアルファ同値である。表示したアルファ同値の右辺は、簡約後の項へ$[x:=N']$を施した結果である。変数、抽象、適用、およびβ基の導出規則を検討した。▨

証明. 完全展開の途中の代入で新たに選ぶ束縛変数は、固定した$b$も避けるものとする。そのような選択は常に可能であり、代入の適切性により選択を変えてもアルファ同値類は変わらない。完全展開の再帰は、もとの項にない自由変数を導入しない。さらに新たな束縛変数にも$b$を用いないので、選んだ$M^\star$の代表元には$b$が現れない。したがって、以下の右辺に現れる$\rho_{a\to b}(M^\star)$は、この代表元に対して定義されている。

$M$の構文に関する帰納法を用いる。変数の場合には、$M=a$かどうかで分けて定義を直接比較する。抽象$M=\lambda u.P$では、$u=a$ならば改名は本体へ入らず、両辺は$\lambda a.P^\star$である。$u\ne a$ならば$u\ne b$でもあり、本体に対する帰納法の仮定へ抽象の文脈を加える。

$M=PQ$であり、$P$が抽象でない場合には、$\rho_{a\to b}(P)$も抽象ではない。二つの部分項に対する帰納法の仮定へ、完全展開の第4式を適用すると (15) を得る。

$M=(\lambda u.P)Q$とする。$u=a$の場合には、

最後の関係は$Q$に対する帰納法の仮定と代入の適切性から従う。一方、補題 4.3の (10) の第1の場合により、

である。

$u\ne a$の場合には$u\ne b$である。二つの帰納法の仮定と代入の適切性により、

補題 4.3の (10) の第2の場合により、右辺は

とアルファ同値である。変数、抽象、抽象でない作用子をもつ適用、β基を作用子にもつ適用の各構文形を確認した。▨

証明. アルファ同値の生成導出に関する帰納法を用いる。定義から、生成導出は、抽象の束縛変数を新鮮な変数へ変更する生成規則を項文脈内で一回用いる段階と、反射性、対称性、および推移性の段階からなる。反射性、対称性、および推移性の段階には、帰納法の仮定と$\equiv_\alpha$の同じ性質を適用する。

一回の改名生成規則を項文脈内で用いる段階を、その改名位置から構文木の根までの文脈の構造に関する帰納法で確認する。生成規則で選ぶ新鮮な変数を$y$とする。完全展開の途中の代入で新たに選ぶ束縛変数にも$y$を用いない代表元を選ぶ。この選択は有限集合の外から行うことができ、代入の適切性により結論に影響しない。完全展開は入力にない自由変数を導入しないので、この選択の下では$y\notin\operatorname{Var}(P^\star)$でもある。改名位置が根である場合には、

という二項を比較する。完全展開と新鮮な自由変数改名に関する補題から、

を得る。

改名位置が抽象の本体内にある場合には、文脈に関する帰納法の仮定へ抽象の文脈を加える。改名位置が適用の引数内にある場合を$RQ_0$と$RQ_1$の比較として書く。$R$が抽象でなければ、二つの完全展開は$R^\star Q_0^\star$と$R^\star Q_1^\star$であり、引数に対する帰納法の仮定を用いる。$R=\lambda u.S$ならば、二つの完全展開は

であり、引数に対する帰納法の仮定と代入の適切性からアルファ同値である。

最後に、改名位置が適用の作用素内にある場合を確認する。作用素の外形が抽象でなければ、完全展開の第4式と作用素に対する帰納法の仮定を用いる。作用素が共通の束縛変数をもつ$\lambda u.S_0$と$\lambda u.S_1$であり、改名位置が二つの本体内にあるならば、比較する完全展開は

である。本体に対する帰納法の仮定と代入の適切性から両者はアルファ同値である。

作用素そのものが (17) の二つの抽象である場合には、比較する完全展開は

である。第2項は、完全展開と改名に関する補題により

とアルファ同値であり、補題 4.3の (11) により第1項とアルファ同値である。一穴項文脈の空、抽象の本体、適用の引数、および適用の作用素の四構成法を用いた場合分けにより、任意の項文脈内の一回の改名生成規則が完全展開によって保存される。空文脈、抽象の本体、適用の引数、および適用の作用素は一穴項文脈の全ての構成法であるため、場合分けは尽くされている。生成導出に関する帰納法に戻ると (16) を得る。▨

証明.$M\Rightarrow_\beta N$の導出に関する帰納法を用いる。

変数の規則の場合には$M=N=x=x^\star$であり、平行簡約の反射性を用いる。抽象の規則の場合には、前提に対する帰納法の仮定へ抽象の規則を適用する。

適用の第3規則から

が導かれているとする。ただし、$P\Rightarrow_\beta P'$かつ$Q\Rightarrow_\beta Q'$である。

$P$が抽象でない場合には、

である。帰納法の仮定$P'\Rightarrow_\beta P^\star$と$Q'\Rightarrow_\beta Q^\star$へ第3規則を適用すれば、

を得る。

$P=\lambda x.R$の場合には、平行簡約の規則から、ある$R'$が存在して$P'=\lambda x.R'$かつ$R\Rightarrow_\beta R'$である。帰納法の仮定により

である。第4規則を用いると、

を得る。

最後に、第4規則から

が導かれているとする。ただし、$P\Rightarrow_\beta P'$かつ$Q\Rightarrow_\beta Q'$である。帰納法の仮定は

を与える。平行簡約の代入補題により、

である。変数規則、抽象規則、適用の第3規則、β基の第4規則を検討した。▨

証明. 完全展開補題により、

である。したがって、$P=M^\star$とすればよい。▨

証明.(1)を、一段のベータ簡約の導出に関する帰納法で示す。根のβ基

については、平行簡約の反射性を$P$と$Q$に適用した後、第4規則を用いる。抽象または適用の文脈内で起こる簡約については、帰納法の仮定へ平行簡約の第2規則または第3規則を適用する。

(2)を、平行簡約の導出に関する帰納法で示す。変数の場合には反射性を用いる。抽象の場合には、帰納法の仮定で得た有限簡約列の各段を抽象の内側で行う。第3規則の場合には、まず左の部分項を有限回簡約し、次に右の部分項を有限回簡約する。

第4規則の場合には、前提が$P\Rightarrow_\beta P'$と$Q\Rightarrow_\beta Q'$であり、結論が

である。帰納法の仮定を抽象と適用の文脈内で用いることにより、

を得る。

根のβ基、抽象の文脈、適用の文脈における一段ベータ簡約を平行簡約で模倣したので、$\to_\beta\subseteq\Rightarrow_\beta\subseteq{\twoheadrightarrow_\beta}$である。三関係の反射推移閉包を取れば、一致する。▨

証明. 最初に、$aRb$かつ$aR^*c$ならば、ある$d$が存在して

となることを、$a$から$c$までの列の長さに関する帰納法で示す。

列の長さが$0$ならば$c=a$である。$d=b$とすれば、$bR^*b$かつ$cRb$である。列の長さが正の場合には、

と書く。ダイヤモンド性を$aRb$と$aRc_1$に適用して、

となる$e$を得る。帰納法の仮定を$c_1Re$と$c_1R^*c$に適用すると、

となる$d$が存在する。したがって、$bReR^*d$かつ$cRd$である。

次に、$aR^*b$の列の長さに関する帰納法で合流性を示す。長さが$0$ならば$b=a$なので、$d=c$とすればよい。長さが正の場合には、

と書く。前段の結果を$aRa_1$と$aR^*c$に適用すると、ある$e$が存在して

となる。帰納法の仮定を$a_1R^*b$と$a_1R^*e$に適用すると、ある$d$が存在して

となる。ゆえに、$bR^*d$かつ$cReR^*d$である。▨

証明. 平行簡約はダイヤモンド性をもつので、ダイヤモンド関係の閉包に関する補題により、平行簡約の反射推移閉包は合流的である。ベータ簡約と平行簡約の比較補題により、この閉包は$\twoheadrightarrow_\beta$と一致する。したがって、第1の主張が従う。

第2の主張を示す。$M=_\beta N$を与える有限の変換列

を取り、各隣接項の間では$A_i\to_\beta A_{i+1}$または$A_{i+1}\to_\beta A_i$が成り立つとする。$i$に関する帰納法で、$M$と$A_i$が共通の簡約先$P_i$をもつことを示す。$i=0$では$P_0=M$とすればよい。