ラムダ計算と Turing 機械の同値性 | 計算理論

1 弱い値呼び評価

ラムダ項、変数捕獲を避ける代入、および $\beta$ 簡約には§E15.8 定義 1.1、§E15.8 定義 2.4、§E15.8 定義 3.1の定義を用いる。

定義 1.1. 値 (value) と評価文脈 (evaluation context) を

V::=\lambda x.M,\qquad E::=[\,]\mid E\,M\mid V\,E

によって定める。弱い値呼び評価の一段関係 $\longrightarrow_v$ は

E[(\lambda x.M)V]\longrightarrow_v E[M[x:=V]]

だけからなる。抽象の本体では簡約しない。

有限回の評価で値 $V$ に達することを $M\longrightarrow_v^*V$ と書く。全ての段階で次の一段が存在し、有限段で値に達しないことを $M\longrightarrow_v^\infty$ と書く。

評価文脈の文法は、作用子を先に評価し、作用子が値になった後に引数を評価する順序を定める。

補題 1.2. 閉項 $M$ は、値であるか、一意な閉項 $N$ へ $M\longrightarrow_vN$ と一段評価されるかのいずれか一方を満たす。

証明. $M$ の構造に関する帰納法を用いる。閉じた変数項は存在しない。抽象は値である。 $M=P\,Q$ とする。適用が閉項ならば $P$ と $Q$ も閉項である。 $P$ が値でなければ、帰納法の仮定により $P$ の次の一段が一意に定まり、評価文脈 $[\,]Q$ が全体の一段を一意に定める。 $P$ が値で $Q$ が値でなければ、 $Q$ の次の一段と評価文脈 $P[\,]$ が全体の一段を一意に定める。 $P$ と $Q$ がともに値ならば、 $P=\lambda x.R$ であるから、根のβ基 $(\lambda x.R)Q$ が一意な一段を与える。三つの場合は互いに排他的である。代入後の項が閉じていることは、閉項 $Q$ を閉項 $(\lambda x.R)Q$ の束縛変数へ代入することから従う。▨

したがって、閉項の評価は停止して値を返すか、無限に評価を続けるかのいずれかであり、停止しない閉項が途中で行き詰まることはない。

2 値呼び Church 符号

弱い評価は抽象の本体を簡約しないため、通常の Church 数と $\beta$ 同値であるだけでは、停止時に同じ構文の数値を得ることができるとは限らない。本記事では、弱い評価に適した正準代表を再帰的に固定する。

定義 2.1. $n\in\mathbb N$ に対する値呼び Church 数 (call-by-value Church numeral) $\mathbf c_n$ を

\mathbf c_0=\lambda f.\lambda x.x,\qquad \mathbf c_{n+1}=\lambda f.\lambda x.f(\mathbf c_n\,f\,x)

によって定める。

各 $\mathbf c_n$ は閉じた抽象であり、通常の $\lambda f.\lambda x.f^nx$ と $\beta$ 同値である。以後、次の閉じた値を用いる。

定義 2.2 (値呼び基本符号). 以下の閉じた値の族を値呼び基本符号 (call-by-value basic encoding) という。

\begin{aligned} \mathsf I&=\lambda z.z,\\ \mathsf T&=\lambda t.\lambda e.t,& \mathsf F&=\lambda t.\lambda e.e,\\ \mathsf{If}&=\lambda b.\lambda u.\lambda v.b\,u\,v\,\mathsf I,\\ \mathsf{Succ}&=\lambda n.\lambda f.\lambda x.f(n\,f\,x),\\ \mathsf{IsZero}&=\lambda n.n(\lambda z.\mathsf F)\mathsf T,\\ \mathsf{Pair}&=\lambda a.\lambda b.\lambda p.p\,a\,b,\\ \mathsf{Fst}&=\lambda p.p(\lambda a.\lambda b.a),& \mathsf{Snd}&=\lambda p.p(\lambda a.\lambda b.b). \end{aligned}

値 $A,B$ に対して

\langle A,B\rangle_v=\lambda p.p\,A\,B

と書く。 $\mathsf{If}$ の第2引数と第3引数には、分枝の本体 $A,B$ をそれぞれ $\lambda d.A,\lambda d.B$ として渡す。変数 $d$ は本体に自由に現れないものとする。

分枝を抽象で包む理由は、選ばれなかった分枝を値呼び評価が先に計算することを防ぐためである。

補題 2.3. 全ての $n\in\mathbb N$ と閉じた値 $A,B$ について、次の評価則が成り立つ。

\begin{aligned} \mathsf{Succ}\,\mathbf c_n&\longrightarrow_v^*\mathbf c_{n+1},\\ \mathsf{IsZero}\,\mathbf c_0&\longrightarrow_v^*\mathsf T,& \mathsf{IsZero}\,\mathbf c_{n+1}&\longrightarrow_v^*\mathsf F,\\ \mathsf{Fst}\langle A,B\rangle_v&\longrightarrow_v^*A,& \mathsf{Snd}\langle A,B\rangle_v&\longrightarrow_v^*B,\\ \mathsf{If}\,\mathsf T\,(\lambda d.A)\,(\lambda d.B)&\longrightarrow_v^*A,& \mathsf{If}\,\mathsf F\,(\lambda d.A)\,(\lambda d.B)&\longrightarrow_v^*B. \end{aligned}

さらに、閉じた値 $S,W_0,\ldots,W_n$ が $S\,W_j\longrightarrow_v^*W_{j+1}$ を $0\le j<n$ について満たすならば、

\mathbf c_n\,S\,W_0\longrightarrow_v^*W_n

である。

証明. $\mathsf{Succ}\,\mathbf c_n$ の根を一段評価すると $\lambda f.\lambda x.f(\mathbf c_n\,f\,x)=\mathbf c_{n+1}$ を得る。射影の二式は、対を選択子へ適用して得られる。条件分岐では、真偽値が二つの分枝の一方を選んだ後、選ばれた抽象を $\mathsf I$ へ適用する。選ばれなかった抽象の本体は評価されない。

反復則を $n$ に関する帰納法で示す。 $n=0$ では $\mathbf c_0\,S\,W_0\longrightarrow_v^*W_0$ である。 $n$ の場合に成立すると仮定する。定義を二回展開すると

\mathbf c_{n+1}\,S\,W_0 \longrightarrow_v^*S(\mathbf c_n\,S\,W_0) \longrightarrow_v^*S\,W_n \longrightarrow_v^*W_{n+1}

となる。中央の評価では値呼び規則が引数 $\mathbf c_n\,S\,W_0$ を先に値 $W_n$ まで評価する。帰納法により反復則を得る。

$\mathsf{IsZero}\,\mathbf c_0$ は $\mathbf c_0(\lambda z.\mathsf F)\mathsf T$ へ進み、 $\mathsf T$ を返す。 $\mathbf c_{n+1}$ の場合には、反復則において $S=\lambda z.\mathsf F$ 、 $W_0=\mathsf T$ 、 $W_j=\mathsf F\ (1\le j\le n+1)$ と置く。 $S\,W_j$ は全て $\mathsf F$ へ評価されるので、 $\mathsf{IsZero}\,\mathbf c_{n+1}$ は $\mathsf F$ を返す。▨

例 2.4 (選ばれない分枝の発散). $\Omega=(\lambda x.x\,x)(\lambda x.x\,x)$ とする。 $\Omega\longrightarrow_v^\infty$ であるが、

\mathsf{If}\,\mathsf T\,(\lambda d.\mathbf c_0)\,(\lambda d.\Omega) \longrightarrow_v^*\mathbf c_0

である。二つの分枝は入力時には値であり、偽の分枝の本体 $\Omega$ は評価位置に現れない。

再帰的な探索には、値呼び評価用の固定点結合子を用いる。

定義 2.5 (値呼び固定点結合子).

\mathsf Z =\lambda g. (\lambda x.g(\lambda u.x\,x\,u)) (\lambda x.g(\lambda u.x\,x\,u)).

$\mathsf Z$ を値呼び固定点結合子 (call-by-value fixed-point combinator) という。閉じた値 $G$ に対して

A_G=\lambda x.G(\lambda u.x\,x\,u),\qquad R_G=\lambda u.A_G\,A_G\,u

と書く。

補題 2.6. 閉じた値 $G,V$ について

\mathsf Z\,G\longrightarrow_v^*G\,R_G,\qquad R_G\,V\longrightarrow_v^*G\,R_G\,V

である。

証明. $G$ が値であるため、

\mathsf Z\,G \longrightarrow_v A_G\,A_G \longrightarrow_v G(\lambda u.A_G\,A_G\,u) =G\,R_G

となる。また、 $V$ が値であるため、

R_G\,V \longrightarrow_v A_G\,A_G\,V \longrightarrow_v G\,R_G\,V

となる。各列は有限であり、 $G$ や $V$ の本体を途中で評価しない。▨

3 部分ミュー再帰関数の表現

定義 3.1. 部分関数 $f\colon\mathbb N^k\rightharpoonup\mathbb N$ を考える。全ての $\vec x=(x_1,\ldots,x_k)$ について次の二条件を満たす閉項 $F$ が存在するとき、 $f$ は値呼びラムダ計算可能 (call-by-value lambda-computable) であるという。

$f(\vec x)=n$ ならば $F\,\mathbf c_{x_1}\cdots\mathbf c_{x_k}\longrightarrow_v^*\mathbf c_n$ である。
$f(\vec x)\mathord\uparrow$ ならば $F\,\mathbf c_{x_1}\cdots\mathbf c_{x_k}\longrightarrow_v^\infty$ である。

二条件を満たす $F$ が $f$ を強く表現する (strongly represents) という。

構成の帰納法では、正のアリティ $k$ をもつ関数の代表項を、閉じた $k$ 引数のカリー化された値として選ぶ。数値を $j<k$ 個だけ与えた部分適用は、残りの引数を受け取る抽象へ有限回で評価される。零アリティの代表は閉項とする。部分適用の不変条件により、合成では内側の部分計算が左から右へ順に強制される。

命題 3.2. 全ての部分ミュー再帰関数は値呼びラムダ計算可能である。有限な生成式から強く表現する閉項を構成することができ、アリティが正なら代表をカリー化された閉じた値として選ぶことができる。

証明では、初期関数、合成、原始再帰、非有界最小化の順に構成を与える。原始再帰では「現在の添字と現在値の対」を Church 数で反復更新し、非有界最小化では、候補の検査結果が得られた後に限って次の候補を評価する。

証明. 生成式の構造に関する帰納法を用いる。 $k$ 変数零関数、後続者関数、射影関数は、それぞれ

\lambda x_1.\cdots\lambda x_k.\mathbf c_0,\qquad \mathsf{Succ},\qquad \lambda x_1.\cdots\lambda x_k.x_i

によって表現される。補題 2.3により出力は正準数値である。各項は必要な個数の先頭抽象をもち、部分適用に関する不変条件も満たす。

合成

h(\vec x)=f(g_1(\vec x),\ldots,g_m(\vec x))

を考える。帰納法の仮定から得た代表を $F,G_1,\ldots,G_m$ とし、

H=\lambda x_1.\cdots\lambda x_k. F(G_1\,\vec x)\cdots(G_m\,\vec x)

と定める。値呼び評価は $G_1\,\vec x,\ldots,G_m\,\vec x$ を左から右へ数値まで評価する。 $G_j\,\vec x$ が最初に発散する位置では、全体も同じ部分計算の内部で発散する。全ての内側の計算が停止した後には、 $F$ が得られた数値を順に受け取る。 $F$ の部分適用は残りの引数を待つ値へ停止するため、後続の $G_j$ より先に余分な発散は生じない。全ての $g_j(\vec x)$ が定義されていても $f(g_1(\vec x),\ldots,g_m(\vec x))$ が未定義ならば、最後に $F$ の評価が発散する。したがって、合成は定義域と値をともに保存する。

原始再帰

\begin{aligned} h(\vec x,0)&=f(\vec x),\\ h(\vec x,n+1)&=g(\vec x,n,h(\vec x,n)) \end{aligned}

を考える。 $F,G$ を帰納法の仮定から得た代表とし、 $\vec x$ を自由変数として含む値

\mathsf{Step}_{\vec x} =\lambda p. \mathsf{Pair}\, (\mathsf{Succ}(\mathsf{Fst}\,p))\, (G\,\vec x\,(\mathsf{Fst}\,p)\,(\mathsf{Snd}\,p))

を用いる。代表を

H=\lambda x_1.\cdots\lambda x_k.\lambda n. \mathsf{Snd}\bigl( n\,\mathsf{Step}_{\vec x} (\mathsf{Pair}\,\mathbf c_0\,(F\,\vec x)) \bigr)

と定める。

$z_0=f(\vec x)$ および $z_{j+1}=g(\vec x,j,z_j)$ が $0\le j<n$ について定義される場合、反復開始時の対は $\langle\mathbf c_0,\mathbf c_{z_0}\rangle_v$ まで評価される。補題 2.3を用いると

\mathsf{Step}_{\vec x} \langle\mathbf c_j,\mathbf c_{z_j}\rangle_v \longrightarrow_v^* \langle\mathbf c_{j+1},\mathbf c_{z_{j+1}}\rangle_v

である。 $j$ に関する帰納法と Church 数の反復則により、 $n$ 回後の対は $\langle\mathbf c_n,\mathbf c_{z_n}\rangle_v$ となり、 $\mathsf{Snd}$ は $\mathbf c_{z_n}$ を返す。 $F\,\vec x$ が発散すれば、初期対を値にする途中で全体が発散する。最小の $j<n$ で $G\,\vec x\,\mathbf c_j\,\mathbf c_{z_j}$ が発散すれば、第 $j+1$ の対を作る途中で全体が発散する。値呼び評価は次の反復へ進む前に現在の対を値にするので、後段の反復が発散を回避することはない。原始再帰の定義域と値が保存される。

上の構成は $k\ge 1$ の場合を扱った。 $k=0$ の場合を明示する。§E15.7 定義 2.1は $k=0$ の原始再帰を許し、そのとき基底は関数 $f$ ではなく一つの自然数 $c$ であり、 $h(0)=c$ かつ $h(n+1)=g(n,h(n))$ である。 $g$ は二変数関数であるから、帰納法の仮定はカリー化された閉じた値 $G$ を与える。 $\vec x$ が空であることに合わせて

\mathsf{Step} =\lambda p. \mathsf{Pair}\, (\mathsf{Succ}(\mathsf{Fst}\,p))\, (G\,(\mathsf{Fst}\,p)\,(\mathsf{Snd}\,p)), \qquad H=\lambda n. \mathsf{Snd}\bigl( n\,\mathsf{Step}\,(\mathsf{Pair}\,\mathbf c_0\,\mathbf c_c) \bigr)

と定める。 $\mathsf{Step}$ は自由変数をもたない値である。 $\mathbf c_0$ と $\mathbf c_c$ はともに値であるから、定義 2.2の $\mathsf{Pair}$ により、初期対 $\mathsf{Pair}\,\mathbf c_0\,\mathbf c_c$ は二段の評価で $\langle\mathbf c_0,\mathbf c_c\rangle_v$ になる。以後の反復と発散に関する議論は $k\ge 1$ の場合と同じであり、基底が数であるため、 $F\,\vec x$ の発散に関する場合分けだけが不要になる。 $H$ は先頭抽象 $\lambda n$ を一つもつ閉じた値であり、一変数関数 $h$ に対する強い表現と部分適用の不変条件を満たす。

最後に、§E15.7 定義 3.1の非有界最小化

h(\vec x)=\mu y[g(\vec x,y)=0]

を考える。 $G$ を $g$ の代表とし、

\begin{aligned} B_G ={}&\lambda r.\lambda x_1.\cdots\lambda x_k.\lambda y.\\ &\mathsf{If}\, (\mathsf{IsZero}(G\,\vec x\,y))\, (\lambda d.y)\, (\lambda d.r\,\vec x\,(\mathsf{Succ}\,y)),\\ H ={}&\lambda x_1.\cdots\lambda x_k. (\mathsf Z\,B_G)\,\vec x\,\mathbf c_0 \end{aligned}

と定める。 $B_G$ は値であり、補題 2.6により、各候補 $y$ の検査後に同じ探索手続きを次の候補へ展開する。

$g(\vec x,z)$ が全ての $z<y$ で定義されて正であり、 $g(\vec x,y)=0$ ならば、探索は候補 $0,\ldots,y$ を順に検査する。正の結果では偽の分枝だけを、零の結果では真の分枝だけを評価するので、有限回の展開後に $\mathbf c_y$ を返す。正の値が続いた後、最初の未定義値 $g(\vec x,z)$ に達した場合、 $\mathsf{IsZero}$ の引数を評価する途中で発散する。全ての候補で $g(\vec x,y)$ が定義されて正ならば、各有限段階の後に次の候補の評価が現れ、決定性により無限評価を生じる。後の候補で零になる場合でも、それより前に未定義値があれば探索は未定義値の位置で発散する。以上の停止、途中発散、無限探索の場合分けは§E15.7 定義 3.1の部分最小化の定義域と一致する。

正のアリティをもつ各構成は先頭抽象を必要な個数だけもつ。合成、原始再帰、最小化で数値を必要数未満だけ与えた場合にも、残りの引数を束縛する抽象で評価が止まる。零アリティでは、構成した閉項そのものが停止値または無限評価を与える。したがって、強い表現と正のアリティに対する部分適用の不変条件が生成式全体で保たれる。▨

4 Turing 機械からラムダ計算へ

定理 4.1.§E15.7 定義 1.1の意味で部分関数 $f\colon\mathbb N^k\rightharpoonup\mathbb N$ を計算する Turing 機械 $M$ から、 $f$ を強く表現する閉じたラムダ項 $F_M$ を構成することができる。 $f(\vec x)=n$ の場合には

F_M\,\mathbf c_{x_1}\cdots\mathbf c_{x_k}\longrightarrow_v^*\mathbf c_n

であり、 $f(\vec x)\mathord\uparrow$ の場合には対応するラムダ評価も停止しない。

証明.§E15.7 定理 5.3は、 $M$ が計算する部分関数と定義域および値が一致する部分ミュー再帰関数の有限な生成式を与える。命題 3.2を生成式へ適用し、強く表現する値 $F_M$ を構成する。定義 3.1 (1)が停止時の出力を保存し、定義 3.1 (2)が $M$ の定義域外における無限評価を保証する。一般の $\beta$ 簡約の標準化は用いていない。▨

5 Turing 機械の配置の直接符号化

前節の構成は§E15.7 定理 5.3を経由するので、 $M$ の一段の遷移がラムダ項の評価として現れない。本節では、 $M$ の配置そのものをラムダ項へ符号化し、遷移関数を一つの閉じた値として表し、固定点結合子によって停止まで反復する構成を与える。到達する結論は定理 4.1と同じであるが、部分ミュー再帰関数を用いない。

最初に、有限集合の要素、対、および有限列を弱い値呼び評価で扱うための符号を定める。

証明.(1)は

\mathsf{Pair}\,A\,B \longrightarrow_v(\lambda b.\lambda p.p\,A\,b)B \longrightarrow_v\lambda p.p\,A\,B =\langle A,B\rangle_v

から従う。

(2)を示す。各 $\lambda d.A_j$ は抽象であるから値である。 $\mathsf{tag}^m_i$ の $m$ 個の先頭抽象を順に縮約すると $\lambda d.A_i$ を得る。 $\mathsf I$ は値であるから、さらに一段で $A_i[d:=\mathsf I]=A_i$ を得る。 $\mathsf T=\mathsf{tag}^2_0$ 、 $\mathsf F=\mathsf{tag}^2_1$ であり、定義 2.2により、真偽値 $V$ と二つの分枝 $K_0,K_1$ について $\mathsf{If}\,V\,K_0\,K_1$ は $V\,K_0\,K_1\,\mathsf I$ へ評価されるので、後半の主張も従う。

(3)を示す。二つの分枝を $K_0=\lambda d.A$ 、 $K_1=\lambda u.\lambda t.\lambda d.B$ と書く。 $[\,]_v\,K_0\longrightarrow_v\lambda c.K_0$ であり、 $(\lambda c.K_0)K_1\longrightarrow_vK_0$ である。さらに $K_0\,\mathsf I\longrightarrow_vA$ を得る。 $p\ge1$ のときには、 $S=[U_2,\ldots,U_p]_v$ として

[U_1,\ldots,U_p]_v\,K_0 \longrightarrow_v\lambda c.c\,U_1\,S, \qquad (\lambda c.c\,U_1\,S)\,K_1 \longrightarrow_vK_1\,U_1\,S

である。 $K_1\,U_1\,S$ は二段で $\lambda d.B[u:=U_1][t:=S]$ へ評価され、 $\mathsf I$ を適用するとさらに一段で $B[u:=U_1][t:=S]$ を得る。

(4)は、 $\mathsf{Pop}\,Z\,S$ が

S\,(\lambda d.\mathsf{Pair}\,Z\,\mathsf{Nil})\, (\lambda u.\lambda t.\lambda d.\mathsf{Pair}\,u\,t)\,\mathsf I

へ二段で評価されることと、(3)および(1)から従う。▨

次に、機械の配置を符号化する。

定義 5.3. $M=(Q,\Sigma,\Gamma,\delta,q_0,q_{\mathrm{acc}},q_{\mathrm{rej}})$ を§E15.4 定義 1.1の単テープ決定性 Turing 機械とする。有限集合の並び $Q=\{p_0,\ldots,p_{k-1}\}$ と $\Gamma=\{a_0,\ldots,a_{m-1}\}$ を一つ固定し、

\overline{p_j}=\mathsf{tag}^k_j, \qquad \overline{a_i}=\mathsf{tag}^m_i

と書く。§E15.4 定義 1.2の配置 $C=(q,h,T)$ と閉じた値 $W$ について、 $W$ が $C$ を表す (represents a Turing configuration) とは、ある $\ell\ge0$ が存在して

W=\Bigl\langle\bar q,\ \bigl\langle L,\ \langle\overline{T(h)},R\rangle_v\bigr\rangle_v\Bigr\rangle_v,

L=[\overline{T(h-1)},\overline{T(h-2)},\ldots,\overline{T(0)}]_v, \qquad R=[\overline{T(h+1)},\ldots,\overline{T(h+\ell)}]_v

であり、かつ $h+\ell$ より大きい全ての位置で $T$ の値が $\sqcup$ となることをいう。 $h=0$ のとき $L=[\,]_v$ である。 $T$ は有限個の位置を除いて $\sqcup$ を値にとるので、そのような $\ell$ は存在する。したがって、各配置は少なくとも一つの表現をもつ。逆に、リスト値の長さと成分は項から定まるので、一つの閉じた値が二つの異なる配置を表すことはない。

配置の構成と成分の取り出しを

\begin{aligned} \mathsf{Conf}&=\lambda q.\lambda l.\lambda b.\lambda r. \mathsf{Pair}\,q\,(\mathsf{Pair}\,l\,(\mathsf{Pair}\,b\,r)),\\ \mathsf{St}&=\lambda w.\mathsf{Fst}\,w, &\mathsf{Lf}&=\lambda w.\mathsf{Fst}(\mathsf{Snd}\,w),\\ \mathsf{Cu}&=\lambda w.\mathsf{Fst}(\mathsf{Snd}(\mathsf{Snd}\,w)), &\mathsf{Rg}&=\lambda w.\mathsf{Snd}(\mathsf{Snd}(\mathsf{Snd}\,w)) \end{aligned}

と定める。

定義 5.4. 上の記号のもとで、停止判定項 (halting-test term) を

\mathsf{Halt}_M=\lambda w.(\mathsf{St}\,w)\, (\lambda d.H_0)\cdots(\lambda d.H_{k-1})\,\mathsf I

と定める。ここで、 $p_j\in\{q_{\mathrm{acc}},q_{\mathrm{rej}}\}$ ならば $H_j=\mathsf T$ 、そうでなければ $H_j=\mathsf F$ である。

遷移項 (transition term) を

\mathsf{Tr}_M=\lambda w.(\mathsf{St}\,w)\, (\lambda d.B_0)\cdots(\lambda d.B_{k-1})\,\mathsf I

と定める。 $p_j\in\{q_{\mathrm{acc}},q_{\mathrm{rej}}\}$ ならば $B_j=w$ とする。そうでなければ

B_j=(\mathsf{Cu}\,w)\,(\lambda d.E_{j,0})\cdots(\lambda d.E_{j,m-1})\,\mathsf I

とし、 $\delta(p_j,a_i)=(q',a',D)$ に応じて $E_{j,i}$ を次のように定める。

$D=S$ のとき $E_{j,i}=\mathsf{Conf}\,\overline{q'}\,(\mathsf{Lf}\,w)\,\overline{a'}\,(\mathsf{Rg}\,w).$
$D=R$ のとき $E_{j,i}= \Bigl(\lambda z.\mathsf{Conf}\,\overline{q'}\, \bigl(\mathsf{Cons}\,\overline{a'}\,(\mathsf{Lf}\,w)\bigr)\, (\mathsf{Fst}\,z)\,(\mathsf{Snd}\,z)\Bigr) \bigl(\mathsf{Pop}\,\overline{\sqcup}\,(\mathsf{Rg}\,w)\bigr).$
$D=L$ のとき $\begin{aligned} E_{j,i}={}&(\mathsf{Lf}\,w)\, \bigl(\lambda d.\mathsf{Conf}\,\overline{q'}\,\mathsf{Nil}\,\overline{a'}\,(\mathsf{Rg}\,w)\bigr)\\ &\bigl(\lambda u.\lambda t.\lambda d. \mathsf{Conf}\,\overline{q'}\,t\,u\, (\mathsf{Cons}\,\overline{a'}\,(\mathsf{Rg}\,w))\bigr)\,\mathsf I. \end{aligned}$

変数 $d,z,u,t$ は、これらの式の他の位置に自由に現れない。 $B_j$ と $E_{j,i}$ の自由変数は $w$ だけであり、先頭の $\lambda w$ で束縛される。 $Q$ と $\Gamma$ は有限であるから、 $\mathsf{Halt}_M$ と $\mathsf{Tr}_M$ は $M$ から定まる有限の閉じた値である。

補題 5.5. 閉じた値 $W$ が配置 $C=(q,h,T)$ を表すとする。

$q\in\{q_{\mathrm{acc}},q_{\mathrm{rej}}\}$ ならば $\mathsf{Halt}_M\,W\longrightarrow_v^*\mathsf T$ であり、そうでなければ $\mathsf{Halt}_M\,W\longrightarrow_v^*\mathsf F$ である。
$q\notin\{q_{\mathrm{acc}},q_{\mathrm{rej}}\}$ とし、 $C\vdash_MC'$ とする。このとき、 $C'$ を表す閉じた値 $W'$ が存在して $\mathsf{Tr}_M\,W\longrightarrow_v^*W'$ である。

証明. $W$ が表す配置の右側の長さを $\ell$ とし、 $W$ の成分を上の定義のとおり $\bar q,L,\overline{T(h)},R$ と書く。補題 2.3の射影の評価則により、

\mathsf{St}\,W\longrightarrow_v^*\bar q, \qquad \mathsf{Lf}\,W\longrightarrow_v^*L, \qquad \mathsf{Cu}\,W\longrightarrow_v^*\overline{T(h)}, \qquad \mathsf{Rg}\,W\longrightarrow_v^*R

である。

(1)を示す。 $q=p_j$ とする。 $\mathsf{Halt}_M\,W$ は一段で $(\mathsf{St}\,W)(\lambda d.H_0)\cdots(\lambda d.H_{k-1})\mathsf I$ へ進み、値呼び評価は最も内側の作用子 $\mathsf{St}\,W$ を先に $\bar q=\mathsf{tag}^k_j$ へ評価する。補題 5.2 (2)により $H_j$ を得る。 $H_j$ の定義から結論が従う。

(2)を示す。 $q=p_j$ 、 $T(h)=a_{i_0}$ 、 $\delta(p_j,a_{i_0})=(q',a',D)$ とする。同じ議論を二度用いると、

\mathsf{Tr}_M\,W\longrightarrow_v^*B_j[w:=W]\longrightarrow_v^*E_{j,i_0}[w:=W]

である。§E15.4 定義 1.2により $C'=(q',h',T')$ であり、 $T'$ は位置 $h$ だけを $a'$ に変え、 $h'$ は $D=S$ で $h$ 、 $D=R$ で $h+1$ 、 $D=L$ かつ $h>0$ で $h-1$ 、 $D=L$ かつ $h=0$ で $0$ である。

$D=S$ の場合。 $E_{j,i_0}[w:=W]$ は $\mathsf{Conf}\,\overline{q'}\,(\mathsf{Lf}\,W)\,\overline{a'}\,(\mathsf{Rg}\,W)$ であり、値呼び評価は四つの引数を左から順に値へ落とす。補題 5.2 (1)を三度用いると

W'=\Bigl\langle\overline{q'},\ \bigl\langle L,\ \langle\overline{a'},R\rangle_v\bigr\rangle_v\Bigr\rangle_v

を得る。 $h'=h$ であり、 $T'$ は位置 $h$ 以外で $T$ と一致するから、 $L$ は $\overline{T'(h'-1)},\ldots,\overline{T'(0)}$ のリスト値、 $R$ は $\overline{T'(h'+1)},\ldots,\overline{T'(h'+\ell)}$ のリスト値であり、 $\overline{a'}=\overline{T'(h')}$ である。 $h+\ell$ より大きい位置では $T'$ と $T$ が一致して $\sqcup$ であるから、 $W'$ は $C'$ を表す。

$D=R$ の場合。値呼び評価は作用子 $\lambda z.\cdots$ が値であるから引数を先に評価する。補題 5.2 (4)により、 $\mathsf{Pop}\,\overline\sqcup\,R$ は、 $\ell\ge1$ のとき $\langle\overline{T(h+1)},[\overline{T(h+2)},\ldots,\overline{T(h+\ell)}]_v\rangle_v$ へ、 $\ell=0$ のとき $\langle\overline\sqcup,\mathsf{Nil}\rangle_v$ へ評価される。 $\ell=0$ のときは表現の条件から $T(h+1)=\sqcup$ であるから、いずれの場合も第1成分は $\overline{T(h+1)}$ であり、第2成分は $\overline{T(h+2)}$ 以降を並べたリスト値である。また $\mathsf{Cons}\,\overline{a'}\,L\longrightarrow_v^*[\overline{a'},\overline{T(h-1)},\ldots,\overline{T(0)}]_v$ である。 $h'=h+1$ 、 $T'(h)=a'$ であるから、この左側リストは長さ $h'$ をもち、 $\overline{T'(h'-1)},\ldots,\overline{T'(0)}$ と一致する。新しい右側の長さを $\ell'$ とすると、 $\ell\ge1$ で $\ell'=\ell-1$ 、 $\ell=0$ で $\ell'=0$ である。どちらの場合も $h'+\ell'\ge h+\ell$ であり、 $h'+\ell'$ より大きい位置で $T'$ の値は $\sqcup$ である。したがって、得られた値は $C'$ を表す。

$D=L$ の場合。作用子 $\mathsf{Lf}\,W$ は $L$ へ評価される。 $h=0$ ならば $L=[\,]_v$ であり、補題 5.2 (3)により $\mathsf{Conf}\,\overline{q'}\,\mathsf{Nil}\,\overline{a'}\,R$ へ進む。 $h'=0$ 、 $T'(0)=a'$ であるから、その値は $C'$ を表す。 $h\ge1$ ならば $L=[\overline{T(h-1)},\ldots,\overline{T(0)}]_v$ であり、同じ補題 5.2 (3)により $u:=\overline{T(h-1)}$ 、 $t:=[\overline{T(h-2)},\ldots,\overline{T(0)}]_v$ を代入した $\mathsf{Conf}\,\overline{q'}\,t\,u\,(\mathsf{Cons}\,\overline{a'}\,R)$ へ進む。 $h'=h-1$ 、 $T'(h-1)=T(h-1)$ 、 $T'(h)=a'$ であるから、左側は $\overline{T'(h'-1)},\ldots,\overline{T'(0)}$ のリスト値、現在記号は $\overline{T'(h')}$ 、右側は長さ $\ell+1$ のリスト値 $\overline{T'(h'+1)},\ldots,\overline{T'(h'+\ell+1)}$ である。 $h'+(\ell+1)=h+\ell$ であり、それより大きい位置では $T'$ と $T$ が一致して $\sqcup$ である。したがって、得られた値は $C'$ を表す。

三つの移動方向を尽くしたので、(2)が成り立つ。▨

入力と出力の変換を定める。以下では $1\in\Sigma$ とし、 $k\ge2$ の場合には $\#\in\Sigma$ とする。

定義 5.6.

\mathsf{One}=\lambda s.\mathsf{Cons}\,\bar1\,s, \qquad \mathsf{Sep}=\lambda s.\mathsf{Cons}\,\overline{\#}\,s

と定める。項 $S_k,\ldots,S_1$ を

S_k=x_k\,\mathsf{One}\,\mathsf{Nil}, \qquad S_j=x_j\,\mathsf{One}\,(\mathsf{Sep}\,S_{j+1}) \quad(1\le j<k)

と定める。 $S_j$ の自由変数は $x_j,\ldots,x_k$ であり、次の項の先頭抽象で束縛される。初期配置項 (initial-configuration term) を

\mathsf{Init}_M =\lambda x_1.\cdots\lambda x_k. \Bigl(\lambda z.\mathsf{Conf}\,\overline{q_0}\,\mathsf{Nil}\,(\mathsf{Fst}\,z)\,(\mathsf{Snd}\,z)\Bigr) \bigl(\mathsf{Pop}\,\overline\sqcup\,S_1\bigr)

と定める。

記号 $1$ の判定項 (symbol-test term) を

\mathsf{Is}_1=\lambda v.v\,(\lambda d.J_0)\cdots(\lambda d.J_{m-1})\,\mathsf I

と定める。ここで、 $a_{i_1}=1$ である添字 $i_1$ に対して $J_{i_1}=\mathsf T$ 、それ以外の添字 $i$ に対して $J_i=\mathsf F$ である。出力抽出項 (output-extraction term) を

\begin{aligned} \mathsf{Cnt}&=\mathsf Z\Bigl(\lambda r.\lambda p. \bigl(\lambda z.\mathsf{If}\,(\mathsf{Is}_1(\mathsf{Fst}\,z))\, (\lambda d.r\,(\mathsf{Pair}\,(\mathsf{Succ}(\mathsf{Fst}\,p))\,(\mathsf{Snd}\,z)))\, (\lambda d.\mathsf{Fst}\,p)\bigr)\\ &\qquad\qquad\quad \bigl(\mathsf{Pop}\,\overline\sqcup\,(\mathsf{Snd}\,p)\bigr)\Bigr),\\ \mathsf{Out}&=\lambda w.\mathsf{Cnt}\, \bigl(\mathsf{Pair}\,\mathbf c_0\,(\mathsf{Cons}\,(\mathsf{Cu}\,w)\,(\mathsf{Rg}\,w))\bigr) \end{aligned}

と定める。

補題 5.7. $U_1,\ldots,U_\ell$ を $\Gamma$ の記号のタグとし、その列の先頭から連続して $\bar1$ である項の個数を $n$ とする。このとき、全ての $j\in\mathbb N$ について

\mathsf{Cnt}\,\langle\mathbf c_j,[U_1,\ldots,U_\ell]_v\rangle_v \longrightarrow_v^*\mathbf c_{j+n}

である。

証明. $\mathsf{Cnt}=\mathsf Z\,G$ の引数 $G$ は閉じた値であるから、補題 2.6により $\mathsf Z\,G\longrightarrow_v^*G\,R_G$ であり、閉じた値 $V$ について $R_G\,V\longrightarrow_v^*G\,R_G\,V$ である。

$\ell$ に関する帰納法を用いる。 $P=\langle\mathbf c_j,[U_1,\ldots,U_\ell]_v\rangle_v$ とすると、 $G\,R_G\,P$ は

\bigl(\lambda z.\mathsf{If}\,(\mathsf{Is}_1(\mathsf{Fst}\,z))\, (\lambda d.R_G(\mathsf{Pair}(\mathsf{Succ}(\mathsf{Fst}\,P))(\mathsf{Snd}\,z)))\, (\lambda d.\mathsf{Fst}\,P)\bigr) \bigl(\mathsf{Pop}\,\overline\sqcup\,(\mathsf{Snd}\,P)\bigr)

へ評価される。作用子は値であるから、引数が先に評価される。補題 2.3の射影の評価則と補題 5.2 (4)により、引数は $\ell=0$ のとき $\langle\overline\sqcup,\mathsf{Nil}\rangle_v$ へ、 $\ell\ge1$ のとき $\langle U_1,[U_2,\ldots,U_\ell]_v\rangle_v$ へ評価される。 $\mathsf{Is}_1$ は補題 5.2 (2)により、 $\bar1$ に対して $\mathsf T$ を、 $\Gamma$ の他の記号のタグに対して $\mathsf F$ を返す。§E15.4 定義 1.1により $\sqcup\notin\Sigma$ であるから $\sqcup\ne1$ である。

$\ell=0$ の場合、または $\ell\ge1$ かつ $U_1\ne\bar1$ の場合には $n=0$ であり、偽の分枝が $\mathsf{Fst}\,P\longrightarrow_v^*\mathbf c_j$ を返す。

$\ell\ge1$ かつ $U_1=\bar1$ の場合には $n\ge1$ であり、真の分枝が評価される。補題 2.3により $\mathsf{Succ}(\mathsf{Fst}\,P)\longrightarrow_v^*\mathbf c_{j+1}$ であり、補題 5.2 (1)により、真の分枝は $R_G\,\langle\mathbf c_{j+1},[U_2,\ldots,U_\ell]_v\rangle_v$ へ評価される。この項は $G\,R_G\,\langle\mathbf c_{j+1},[U_2,\ldots,U_\ell]_v\rangle_v$ へ評価される。列 $U_2,\ldots,U_\ell$ の先頭から連続する $\bar1$ の個数は $n-1$ であるから、長さ $\ell-1$ に対する帰納法の仮定により、この項は $\mathbf c_{(j+1)+(n-1)}=\mathbf c_{j+n}$ へ評価される。▨

定義 5.8 (停止までの反復項).

G_M=\lambda r.\lambda w. \mathsf{If}\,(\mathsf{Halt}_M\,w)\,(\lambda d.w)\, (\lambda d.r\,(\mathsf{Tr}_M\,w)), \qquad \mathsf{Run}_M=\mathsf Z\,G_M

と定める。 $\mathsf{Run}_M$ を停止までの反復項 (iteration-until-halting term) という。さらに、

\mathsf{Sim}_M =\lambda x_1.\cdots\lambda x_k. \mathsf{Out}\bigl(\mathsf{Run}_M\,(\mathsf{Init}_M\,x_1\cdots x_k)\bigr)

と定める。

定理 5.9. $M$ を、§E15.7 定義 1.1の意味で部分関数 $f\colon\mathbb N^k\rightharpoonup\mathbb N$ を計算する単テープ決定性 Turing 機械とする。上で構成した閉項 $\mathsf{Sim}_M$ は $f$ を強く表現する。すなわち、 $f(\vec x)=n$ ならば

\mathsf{Sim}_M\,\mathbf c_{x_1}\cdots\mathbf c_{x_k}\longrightarrow_v^*\mathbf c_n

であり、 $f(\vec x)\mathord\uparrow$ ならば $\mathsf{Sim}_M\,\mathbf c_{x_1}\cdots\mathbf c_{x_k}\longrightarrow_v^\infty$ である。

証明. 入力語を $w_{\vec x}=1^{x_1}\#\cdots\#1^{x_k}$ 、その長さを $N$ とし、§E15.4 定義 1.2の初期配置を $C_0=(q_0,0,T_{w_{\vec x}})$ とする。

最初に初期配置項を追う。 $\mathsf{One}$ は閉じた値であり、任意のリスト値 $S$ に対して $\mathsf{One}\,S$ は $S$ の先頭へ $\bar1$ を付け加えたリスト値へ評価される。したがって補題 2.3の反復則の仮定が満たされる。 $\mathbf c_{x_j}$ を代入した後、 $j$ を大きい方から順に見ると、反復則により $S_j$ は語 $1^{x_j}\#\cdots\#1^{x_k}$ の記号のタグを順に並べたリスト値へ評価される。したがって $S_1$ は $[\overline{w_{\vec x}(0)},\ldots,\overline{w_{\vec x}(N-1)}]_v$ へ評価される。補題 5.2 (4)により、 $\mathsf{Pop}\,\overline\sqcup\,S_1$ は $N\ge1$ のとき $\langle\overline{T_{w_{\vec x}}(0)},[\overline{T_{w_{\vec x}}(1)},\ldots, \overline{T_{w_{\vec x}}(N-1)}]_v\rangle_v$ へ、 $N=0$ のとき $\langle\overline\sqcup,\mathsf{Nil}\rangle_v$ へ評価される。 $N=0$ のときは全マスが空白であるから、どちらの場合も第1成分は $\overline{T_{w_{\vec x}}(0)}$ である。続いて $\mathsf{Conf}$ を適用すると、 $C_0$ を表す閉じた値 $W_0$ を得る（右側の長さは $N\ge1$ で $N-1$ 、 $N=0$ で $0$ である）。

次に反復を追う。 $G_M$ は閉じた値であるから、補題 2.6により $\mathsf{Run}_M\longrightarrow_v^*G_M\,R_{G_M}\longrightarrow_vV_M$ である。ここで

V_M=\lambda w.\mathsf{If}\,(\mathsf{Halt}_M\,w)\,(\lambda d.w)\, (\lambda d.R_{G_M}(\mathsf{Tr}_M\,w))

である。閉じた値 $W$ が配置 $C=(q,h,T)$ を表すとき、補題 5.5と補題 5.2 (2)により次が成り立つ。

$q\in\{q_{\mathrm{acc}},q_{\mathrm{rej}}\}$ ならば $V_M\,W\longrightarrow_v^*W$ である。
そうでなければ、 $C\vdash_MC'$ を満たす $C'$ を表す閉じた値 $W'$ が存在して、 $V_M\,W$ から $V_M\,W'$ への空でない有限の評価列がある。実際、偽の分枝は $R_{G_M}(\mathsf{Tr}_M\,W)$ であり、 $R_{G_M}$ は値、 $\mathsf{Tr}_M\,W$ は $W'$ へ評価され、 $R_{G_M}\,W'\longrightarrow_v^*G_M\,R_{G_M}\,W'\longrightarrow_v^*V_M\,W'$ である。

$f(\vec x)=n$ の場合を考える。§E15.7 定義 1.1により $M$ は $w_{\vec x}$ で停止し、§E15.4 定義 1.3の極大有限計算 $C_0,\ldots,C_t$ が存在する。 $C_0,\ldots,C_{t-1}$ の状態は停止状態ではなく、 $C_t$ の状態は $q_{\mathrm{acc}}$ である。上の(2)を $t$ 回、続いて(1)を用いると、各 $C_s$ を表す閉じた値 $W_s$ が得られ、 $V_M\,W_0\longrightarrow_v^*W_t$ である。 $C_t$ は正規出力配置であるから、ヘッド位置は $0$ であり、テープ内容を $T$ とすると位置 $0,\ldots,n-1$ で $1$ 、それ以外の位置で $\sqcup$ である。 $W_t$ の左側は $[\,]_v$ であり、 $W_t$ の右側の長さを $\ell$ とすると $\mathsf{Cons}\,(\mathsf{Cu}\,W_t)\,(\mathsf{Rg}\,W_t)$ は $[\overline{T(0)},\ldots,\overline{T(\ell)}]_v$ へ評価される。 $n\ge1$ のときは、表現の条件と $T(n-1)=1$ から $\ell\ge n-1$ であり、この列の先頭から連続する $\bar1$ の個数はちょうど $n$ である。 $n=0$ のときは先頭が $\overline\sqcup$ であるから、その個数は $0$ である。補題 5.7を $j=0$ で用いると $\mathsf{Out}\,W_t\longrightarrow_v^*\mathbf c_n$ を得る。以上を合わせると $\mathsf{Sim}_M\,\mathbf c_{x_1}\cdots\mathbf c_{x_k}\longrightarrow_v^*\mathbf c_n$ である。

$f(\vec x)\mathord\uparrow$ の場合を考える。§E15.7 定義 1.1により $M$ は $w_{\vec x}$ で停止せず、§E15.4 定義 1.3の第1の場合により無限の配置列 $C_0,C_1,\ldots$ が存在する。どの $C_s$ の状態も停止状態ではない。上の(2)を繰り返すと、各 $s$ について $C_s$ を表す閉じた値 $W_s$ と、 $V_M\,W_s$ から $V_M\,W_{s+1}$ への空でない有限の評価列が得られる。 $\mathsf{Out}$ は値であるから、定義 1.1の評価文脈 $V\,E$ により、引数の評価列はそのまま全体の評価列になる。したがって、 $\mathsf{Sim}_M\,\mathbf c_{x_1}\cdots\mathbf c_{x_k}$ から始まる評価列は無限に長く、その途中に値は現れない。補題 1.2により閉項の評価は決定的であるから、この列が唯一の評価である。すなわち $\mathsf{Sim}_M\,\mathbf c_{x_1}\cdots\mathbf c_{x_k}\longrightarrow_v^\infty$ である。▨

二つの経路は同じ結論に達する。定理 4.1は関数の生成式に沿って項を組み立て、定理 5.9は機械の配置を項として保持し、一段の遷移を項の評価として実行する。後者は§E15.7 定理 5.3を用いないので、前者の第2の証明にもなっている。

6 de Bruijn 符号と代入

逆向きの模倣では、変数名の変更に依存しない有限構文を機械へ渡す。

定義 6.1. de Bruijn 項 (de Bruijn term) を

D::=\mathsf v_i\mid\mathsf lD\mid\mathsf a(D,D) \qquad(i\in\mathbb N)

によって定める。深さ $d$ で自由変数をもたないことを表す述語 $\operatorname{WF}_d$ を

\begin{aligned} \operatorname{WF}_d(\mathsf v_i)&\iff i<d,\\ \operatorname{WF}_d(\mathsf lP)&\iff\operatorname{WF}_{d+1}(P),\\ \operatorname{WF}_d(\mathsf a(P,Q)) &\iff\operatorname{WF}_d(P)\land\operatorname{WF}_d(Q) \end{aligned}

と定める。 $\operatorname{WF}_0(D)$ を満たす項を閉項とする。

有限二進符号を

\begin{aligned} \ulcorner\mathsf v_i\urcorner&=00\,1^i0,\\ \ulcorner\mathsf lP\urcorner&=01\,\ulcorner P\urcorner,\\ \ulcorner\mathsf a(P,Q)\urcorner&=1\,\ulcorner P\urcorner\ulcorner Q\urcorner \end{aligned}

と定める。

接頭辞 $00,01,1$ は互いに区別することができ、変数符号は末尾の $0$ まで読めば終わる。したがって、構文木は左から一意に復号することができる。名前付き項をこの構文へ移す翻訳は、次節で束縛変数の列を引数に取る再帰として定める。

代入を機械で実行するため、切断位置以上の指標を増加させる全域操作を

\begin{aligned} \uparrow_r^c(\mathsf v_i) &=\begin{cases} \mathsf v_i&i<c,\\ \mathsf v_{i+r}&i\ge c, \end{cases}\\ \uparrow_r^c(\mathsf lP)&=\mathsf l(\uparrow_r^{c+1}P),\\ \uparrow_r^c(\mathsf a(P,Q)) &=\mathsf a(\uparrow_r^cP,\uparrow_r^cQ) \end{aligned}

と定める。また、束縛子を一つ除きながら代入する全域操作を

\begin{aligned} \operatorname{sub}_j(N,\mathsf v_i) &=\begin{cases} \mathsf v_i&i<j,\\ N&i=j,\\ \mathsf v_{i-1}&i>j, \end{cases}\\ \operatorname{sub}_j(N,\mathsf lP) &=\mathsf l\bigl(\operatorname{sub}_{j+1}(\uparrow_1^0N,P)\bigr),\\ \operatorname{sub}_j(N,\mathsf a(P,Q)) &=\mathsf a(\operatorname{sub}_j(N,P),\operatorname{sub}_j(N,Q)) \end{aligned}

と定める。最上位の束縛変数への代入を $\operatorname{SubTop}(N,P)=\operatorname{sub}_0(N,P)$ と書く。

代入の再帰は抽象を通るたびに切断位置を一つ上げるので、以下の議論では、切断位置が等しい二つのシフトを合成した結果を一つのシフトで書き直す等式を繰り返し用いる。先にこの等式を示す。

補題 6.2. 全ての de Bruijn 項 $P$ と全ての非負整数 $b,c$ について

\uparrow_1^b\bigl(\uparrow_c^bP\bigr)=\uparrow_{c+1}^bP

である。

証明. $\uparrow_r^c$ の再帰呼出しは真部分項に対して行われるので、 $\uparrow_r^c$ は有限な de Bruijn 項上の全域関数である。以下、 $c$ を固定し、全ての $b$ について同時に成り立つことを $P$ の構造に関する帰納法で示す。抽象の場合に切断位置を一つ上げた帰納法の仮定を用いるため、 $b$ を全称化した形で帰納法を回す必要がある。

$P=\mathsf v_i$ の場合。 $i<b$ ならば $\uparrow_c^b(\mathsf v_i)=\mathsf v_i$ であり、 $i<b$ であるから $\uparrow_1^b(\mathsf v_i)=\mathsf v_i$ である。一方 $\uparrow_{c+1}^b(\mathsf v_i)=\mathsf v_i$ であるから、両辺は一致する。 $i\ge b$ ならば $\uparrow_c^b(\mathsf v_i)=\mathsf v_{i+c}$ であり、 $c\ge 0$ から $i+c\ge b$ であるので $\uparrow_1^b(\mathsf v_{i+c})=\mathsf v_{i+c+1}$ である。一方 $\uparrow_{c+1}^b(\mathsf v_i)=\mathsf v_{i+c+1}$ であるから、両辺は一致する。

$P=\mathsf a(P_1,P_2)$ の場合。シフトは適用について準同型であるから

\uparrow_1^b\bigl(\uparrow_c^b\mathsf a(P_1,P_2)\bigr) =\mathsf a\bigl(\uparrow_1^b(\uparrow_c^bP_1),\ \uparrow_1^b(\uparrow_c^bP_2)\bigr)

である。 $P_1$ と $P_2$ に対する帰納法の仮定を同じ $b$ で用いると、右辺は $\mathsf a(\uparrow_{c+1}^bP_1,\uparrow_{c+1}^bP_2)=\uparrow_{c+1}^b\mathsf a(P_1,P_2)$ に等しい。

$P=\mathsf lP_0$ の場合。定義により

\uparrow_1^b\bigl(\uparrow_c^b(\mathsf lP_0)\bigr) =\uparrow_1^b\bigl(\mathsf l(\uparrow_c^{b+1}P_0)\bigr) =\mathsf l\bigl(\uparrow_1^{b+1}(\uparrow_c^{b+1}P_0)\bigr)

である。 $P_0$ に対する帰納法の仮定を $b+1$ で用いると、右辺は $\mathsf l\bigl(\uparrow_{c+1}^{b+1}P_0\bigr)=\uparrow_{c+1}^b(\mathsf lP_0)$ に等しい。

変数、適用、抽象の三つの構文形を尽くしたので、主張が成り立つ。▨

補題 6.3. 上のシフト、 $\operatorname{sub}$ 、 $\operatorname{SubTop}$ は有限な de Bruijn 項上の全域関数である。さらに、次が成り立つ。

$\operatorname{WF}_{d+c}(P)$ ならば $\operatorname{WF}_{d+r+c}(\uparrow_r^cP)$ である。
$\operatorname{WF}_d(N)$ かつ $\operatorname{WF}_{d+c+1}(P)$ ならば $\operatorname{WF}_{d+c} \bigl(\operatorname{sub}_c(\uparrow_c^0N,P)\bigr)$ である。
特に、 $\operatorname{WF}_d(N)$ かつ $\operatorname{WF}_{d+1}(P)$ ならば $\operatorname{WF}_d(\operatorname{SubTop}(N,P))$ である。

証明. 各操作の再帰呼出しは真部分項に対して行われるので、有限構文木の構造に関する帰納法から全域性が従う。

(1)を $P$ の構造に関する帰納法で示す。変数の場合、 $i<c$ なら指標は変わらず $i<c\le d+r+c$ である。 $i\ge c$ なら、仮定 $i<d+c$ から $i+r<d+r+c$ を得る。適用では二つの帰納法の仮定を用いる。抽象では深さと切断位置をともに一つ増やし、帰納法の仮定を本体へ適用する。

(2)も $P$ の構造に関する帰納法で示す。 $P=\mathsf v_i$ とする。 $i<c$ では $\mathsf v_i$ が深さ $d+c$ でも整形式である。 $i=c$ では結果が $\uparrow_c^0N$ であり、(1)から $\operatorname{WF}_{d+c}(\uparrow_c^0N)$ を得る。 $i>c$ では $i<d+c+1$ から $i-1<d+c$ を得る。適用の場合は二つの部分項へ帰納法の仮定を適用する。抽象の場合には、補題 6.2を $b=0$ として用いると

\uparrow_1^0(\uparrow_c^0N)=\uparrow_{c+1}^0N

である。切断位置を $c+1$ として本体へ帰納法の仮定を適用すると、結果は深さ $d+c+1$ で整形式となる。(3)は(2)で $c=0$ とした場合である。▨

7 名前付き項から de Bruijn 項への翻訳

de Bruijn 項は変数名をもたないので、名前付き項との対応を与えなければ、前節の操作を§E15.8 定義 2.4の代入と結び付けることができない。以下では、変数出現から対応する束縛子までに通過する抽象の個数を指標とする翻訳を、束縛変数の列を引数に取る再帰として定め、翻訳がアルファ同値と代入を保存することを証明する。

定義 7.1. 束縛文脈 (binding context) とは、変数の有限列 $\Xi=(y_0,\ldots,y_{d-1})$ である。同じ変数が二回以上現れてよい。長さを $|\Xi|=d$ と書き、空列を $\varepsilon$ 、長さ $1$ の列を $(x)$ 、先頭への追加を $x\cdot\Xi$ 、二つの列の連結を $\Delta\Xi$ と書く。 $\Xi$ に現れる変数の集合を $\operatorname{set}(\Xi)$ と書く。 $x\in\operatorname{set}(\Xi)$ のとき、

\operatorname{idx}_\Xi(x)=\min\{i<d\mid y_i=x\}

と定める。最小の添字を取るので、同じ変数を束縛する抽象が入れ子になっている場合には、最も内側の束縛子が選ばれる。

名前付き項 $M$ と束縛文脈 $\Xi$ に対する de Bruijn 項 $\operatorname{dB}_\Xi(M)$ を、 $M$ の構文に関する再帰によって

\begin{aligned} \operatorname{dB}_\Xi(x)&=\mathsf v_{\operatorname{idx}_\Xi(x)} &&(x\in\operatorname{set}(\Xi)),\\ \operatorname{dB}_\Xi(\lambda x.M_0) &=\mathsf l\bigl(\operatorname{dB}_{x\cdot\Xi}(M_0)\bigr),\\ \operatorname{dB}_\Xi(M_1M_2) &=\mathsf a\bigl(\operatorname{dB}_\Xi(M_1),\operatorname{dB}_\Xi(M_2)\bigr) \end{aligned}

と定める。 $x\notin\operatorname{set}(\Xi)$ である変数に対しては定めない。閉項 $M$ については $\operatorname{dB}(M)=\operatorname{dB}_\varepsilon(M)$ と書く。

この再帰は、アルファ同値で商を取る前の代表元に対して定める。結果が代表元によらないことは補題 7.4で示す。

補題 7.2. 次の二つが成り立つ。

$\operatorname{FV}(M)\subseteq\operatorname{set}(\Xi)$ かつ $|\Xi|=d$ ならば、 $\operatorname{dB}_\Xi(M)$ は定義され、 $\operatorname{WF}_d\bigl(\operatorname{dB}_\Xi(M)\bigr)$ を満たす。
束縛文脈 $\Xi,\Xi'$ が、 $\operatorname{FV}(M)$ の各変数 $z$ について $\operatorname{idx}_\Xi(z)$ と $\operatorname{idx}_{\Xi'}(z)$ をともに定義し、かつ二つの指標が等しいならば、 $\operatorname{dB}_\Xi(M)=\operatorname{dB}_{\Xi'}(M)$ である。

証明.(1)を $M$ の構造に関する帰納法で示す。 $M=z$ の場合、 $z\in\operatorname{set}(\Xi)$ であるから $\operatorname{idx}_\Xi(z)$ が定義され、その値は $d$ 未満である。したがって $\operatorname{WF}_d(\mathsf v_{\operatorname{idx}_\Xi(z)})$ である。 $M=\lambda u.M_0$ の場合、 $\operatorname{FV}(M_0)\subseteq\operatorname{FV}(M)\cup\{u\}\subseteq\operatorname{set}(u\cdot\Xi)$ であり、 $|u\cdot\Xi|=d+1$ である。本体に対する帰納法の仮定と $\operatorname{WF}_d(\mathsf lP)\iff\operatorname{WF}_{d+1}(P)$ から結論を得る。 $M=M_1M_2$ の場合、 $\operatorname{FV}(M_i)\subseteq\operatorname{FV}(M)$ であるから、二つの帰納法の仮定を合わせる。

(2)も $M$ の構造に関する帰納法で示す。変数の場合は仮定そのものである。適用の場合は二つの帰納法の仮定を用いる。抽象 $\lambda u.M_0$ の場合には、二つの文脈を $u\cdot\Xi$ と $u\cdot\Xi'$ へ延ばす。 $z\in\operatorname{FV}(M_0)$ とする。 $z=u$ ならば、最小の添字を取る規約により両方の指標が $0$ である。 $z\ne u$ ならば $z\in\operatorname{FV}(M)$ であり、

\operatorname{idx}_{u\cdot\Xi}(z)=1+\operatorname{idx}_\Xi(z) =1+\operatorname{idx}_{\Xi'}(z)=\operatorname{idx}_{u\cdot\Xi'}(z)

である。本体に対する帰納法の仮定から結論を得る。▨

補題 7.3. 束縛文脈 $\Delta,\Xi$ と項 $N$ が

\operatorname{FV}(N)\subseteq\operatorname{set}(\Xi), \qquad \operatorname{set}(\Delta)\cap\operatorname{FV}(N)=\varnothing

を満たすならば、 $c=|\Delta|$ として

\operatorname{dB}_{\Delta\Xi}(N)=\uparrow_c^0\operatorname{dB}_\Xi(N)

である。

証明. 束縛文脈 $\Theta$ （長さ $b$ ）を加えた次の主張を、 $N$ の構造に関する帰納法で示す。

\operatorname{FV}(N)\subseteq\operatorname{set}(\Theta)\cup\operatorname{set}(\Xi), \qquad \operatorname{set}(\Delta)\cap\bigl(\operatorname{FV}(N)\setminus\operatorname{set}(\Theta)\bigr) =\varnothing

ならば

\operatorname{dB}_{\Theta\Delta\Xi}(N) =\uparrow_c^b\operatorname{dB}_{\Theta\Xi}(N)

である。 $\Theta=\varepsilon$ とすれば補題の等式を得る。

$N=z$ とする。 $z\in\operatorname{set}(\Theta)$ ならば、両辺の内側の指標は $\operatorname{idx}_\Theta(z)<b$ であり、 $\uparrow_c^b$ は $b$ 未満の指標を変えない。 $z\notin\operatorname{set}(\Theta)$ ならば、第2の仮定により $z\notin\operatorname{set}(\Delta)$ であり、第1の仮定により $z\in\operatorname{set}(\Xi)$ である。左辺の指標は $b+c+\operatorname{idx}_\Xi(z)$ であり、右辺では内側の指標 $b+\operatorname{idx}_\Xi(z)$ が $b$ 以上であるから $\uparrow_c^b$ が $c$ を加える。両辺は一致する。

$N=N_1N_2$ の場合には、 $\uparrow_c^b$ が適用について準同型であることと、二つの帰納法の仮定を用いる。

$N=\lambda u.N_0$ の場合には、 $\Theta$ を $u\cdot\Theta$ へ、 $b$ を $b+1$ へ置き換える。 $\operatorname{FV}(N_0)\subseteq\operatorname{FV}(N)\cup\{u\}$ であるから第1の仮定が保たれ、

\operatorname{FV}(N_0)\setminus\operatorname{set}(u\cdot\Theta) \subseteq\operatorname{FV}(N)\setminus\operatorname{set}(\Theta)

であるから第2の仮定も保たれる。 $\uparrow_c^b(\mathsf lP)=\mathsf l(\uparrow_c^{b+1}P)$ と本体に対する帰納法の仮定から結論を得る。変数、適用、抽象の三つの構文形を尽くした。▨

補題 7.4. 次の二つが成り立つ。

項 $P$ と変数 $x,y$ が $y\notin\operatorname{Var}(P)\cup\{x\}$ を満たし、束縛文脈 $\Delta,\Xi$ が $x\notin\operatorname{set}(\Delta), \qquad y\notin\operatorname{set}(\Delta), \qquad \operatorname{FV}(P)\subseteq\operatorname{set}(\Delta)\cup\{x\}\cup\operatorname{set}(\Xi)$ を満たすならば、 $\operatorname{dB}_{\Delta\,(x)\,\Xi}(P) =\operatorname{dB}_{\Delta\,(y)\,\Xi}\bigl(\rho_{x\to y}(P)\bigr)$ である。
$M\equiv_\alpha M'$ かつ $\operatorname{FV}(M)\subseteq\operatorname{set}(\Xi)$ ならば $\operatorname{dB}_\Xi(M)=\operatorname{dB}_\Xi(M')$ である。したがって、翻訳はアルファ同値類上の写像として定まる。

証明.(1)を $P$ の構造に関する帰納法で示す。 $c=|\Delta|$ と書く。

$P=x$ の場合。 $\rho_{x\to y}(x)=y$ である。 $x\notin\operatorname{set}(\Delta)$ であるから左辺の指標は $c$ であり、 $y\notin\operatorname{set}(\Delta)$ であるから右辺の指標も $c$ である。

$P=z\ne x$ の場合。 $\rho_{x\to y}(z)=z$ であり、 $y\notin\operatorname{Var}(P)=\{z\}$ から $z\ne y$ である。 $z\in\operatorname{set}(\Delta)$ ならば両辺の指標は $\operatorname{idx}_\Delta(z)$ である。 $z\notin\operatorname{set}(\Delta)$ ならば、仮定により $z\in\operatorname{set}(\Xi)$ であり、 $z\ne x$ と $z\ne y$ から両辺の指標はともに $c+1+\operatorname{idx}_\Xi(z)$ である。

$P=P_1P_2$ の場合。 $\rho_{x\to y}$ は適用について準同型であり、 $\operatorname{FV}(P_i)\subseteq\operatorname{FV}(P)$ 、 $y\notin\operatorname{Var}(P_i)$ であるから、二つの帰納法の仮定を合わせる。

$P=\lambda x.P_0$ の場合。§E15.8 定義 2.1により $\rho_{x\to y}(\lambda x.P_0)=\lambda x.P_0$ である。示すべき等式は

\operatorname{dB}_{x\cdot\Delta\,(x)\,\Xi}(P_0) =\operatorname{dB}_{x\cdot\Delta\,(y)\,\Xi}(P_0)

である。 $z\in\operatorname{FV}(P_0)$ とする。 $z=x$ ならば両方の指標は $0$ である。 $z\ne x$ ならば $z\in\operatorname{FV}(P)$ であり、 $y\notin\operatorname{Var}(P)$ から $z\ne y$ である。 $z\in\operatorname{set}(\Delta)$ の場合は両方の指標が $1+\operatorname{idx}_\Delta(z)$ 、そうでない場合は仮定により $z\in\operatorname{set}(\Xi)$ であり両方の指標が $c+2+\operatorname{idx}_\Xi(z)$ である。補題 7.2の補題 7.2 (2)から等式を得る。

$P=\lambda u.P_0$ かつ $u\ne x$ の場合。 $\rho_{x\to y}(\lambda u.P_0)=\lambda u.\rho_{x\to y}(P_0)$ である。 $u\in\operatorname{BV}(P)\subseteq\operatorname{Var}(P)$ と $y\notin\operatorname{Var}(P)$ から $u\ne y$ である。したがって $\Delta$ を $u\cdot\Delta$ へ置き換えても第1と第2の仮定が保たれ、 $\operatorname{FV}(P_0)\subseteq\operatorname{FV}(P)\cup\{u\}$ から第3の仮定も保たれる。本体に対する帰納法の仮定を抽象の翻訳の式へ入れると結論を得る。変数、適用、および二種類の抽象を尽くした。

(2)を示す。最初に、アルファ同値な項の自由変数集合が等しいことを確かめる。 $\rho_{u\to y}$ の定義に関する構造帰納法により、 $y\notin\operatorname{Var}(P)$ のとき

\operatorname{FV}\bigl(\rho_{u\to y}(P)\bigr)= \begin{cases} \bigl(\operatorname{FV}(P)\setminus\{u\}\bigr)\cup\{y\}&(u\in\operatorname{FV}(P)),\\ \operatorname{FV}(P)&(u\notin\operatorname{FV}(P)) \end{cases}

である。したがって§E15.8 定義 2.2の改名生成規則の両辺の自由変数集合は、ともに $\operatorname{FV}(P)\setminus\{u\}$ である。項文脈の規則と同値関係の規則もこの性質を保つ。

$M\equiv_\alpha M'$ の導出に関する帰納法を用いる。反射性と対称性の段階では帰納法の仮定と等号の性質を用いる。推移性の段階では、中間の項の自由変数集合が $\operatorname{FV}(M)$ と等しいので、二つの帰納法の仮定を同じ $\Xi$ について適用することができる。

改名生成規則を項文脈の中で一回用いる段階を、改名位置から根までの一穴項文脈の構造に関する帰納法で示す。文脈が空の場合、比較する二項は $\lambda u.P$ と $\lambda y.\rho_{u\to y}(P)$ であり、 $y\notin\operatorname{Var}(P)\cup\{u\}$ である。 $\operatorname{FV}(\lambda u.P)\subseteq\operatorname{set}(\Xi)$ から $\operatorname{FV}(P)\subseteq\{u\}\cup\operatorname{set}(\Xi)$ を得る。(1)を $\Delta=\varepsilon$ として用いると

\operatorname{dB}_{(u)\Xi}(P) =\operatorname{dB}_{(y)\Xi}\bigl(\rho_{u\to y}(P)\bigr)

であり、抽象の翻訳の式から二項の翻訳が一致する。文脈が $\lambda v.C[\,]$ の場合には、束縛文脈を $v\cdot\Xi$ へ延ばして帰納法の仮定を用いる。文脈が $C[\,]Q$ または $QC[\,]$ の場合には、変化しない側の翻訳が等しく、変化する側へ帰納法の仮定を用いる。空文脈、抽象の本体、適用の作用素、適用の引数は一穴項文脈の全ての構成法であるから、場合分けは尽くされている。▨

命題 7.5. 束縛文脈 $\Xi$ 、変数 $x$ 、項 $M,N$ が

\operatorname{FV}(M)\subseteq\{x\}\cup\operatorname{set}(\Xi), \qquad \operatorname{FV}(N)\subseteq\operatorname{set}(\Xi)

を満たすならば、

\operatorname{dB}_\Xi\bigl(M[x:=N]\bigr) =\operatorname{SubTop}\bigl(\operatorname{dB}_\Xi(N), \operatorname{dB}_{x\cdot\Xi}(M)\bigr)

である。とくに、 $\lambda x.M$ と $V$ がともに閉項であり $\operatorname{dB}(\lambda x.M)=\mathsf lR$ ならば、

\operatorname{SubTop}\bigl(\operatorname{dB}(V),R\bigr) =\operatorname{dB}\bigl(M[x:=V]\bigr)

である。

証明.補題 7.4 (2)により、右辺は $M$ のアルファ同値類だけに依存する。左辺も、§E15.8 命題 2.5により $M[x:=N]$ のアルファ同値類が $M$ のアルファ同値類だけで定まるので、 $M$ の代表元によらない。したがって、 $M$ の代表元として、束縛変数が全て $\{x\}\cup\operatorname{FV}(N)$ の外にあるものを選んでよい。各束縛子の変数を、有限集合 $\operatorname{Var}(M)\cup\operatorname{Var}(N)\cup\{x\}$ の外の相異なる変数へ内側から順に改名すれば、そのような代表元が得られる。この代表元では、§E15.8 定義 2.4の再帰が改名を必要とせず、抽象については $(\lambda u.M_0)[x:=N]=\lambda u.\bigl(M_0[x:=N]\bigr)$ である。また、 $M$ の部分項の束縛変数も同じ条件を満たす。

次の一般化した主張を、 $M$ の構造に関する帰納法で示す。束縛文脈 $\Delta$ （長さ $c$ ）と $\Xi$ が

x\notin\operatorname{set}(\Delta), \qquad \operatorname{set}(\Delta)\cap\operatorname{FV}(N)=\varnothing,

\operatorname{FV}(M)\subseteq\operatorname{set}(\Delta)\cup\{x\}\cup\operatorname{set}(\Xi), \qquad \operatorname{FV}(N)\subseteq\operatorname{set}(\Xi)

を満たすならば、

\operatorname{dB}_{\Delta\Xi}\bigl(M[x:=N]\bigr) =\operatorname{sub}_c\bigl(\uparrow_c^0D, \operatorname{dB}_{\Delta\,(x)\,\Xi}(M)\bigr), \qquad D=\operatorname{dB}_\Xi(N)

である。 $\Delta=\varepsilon$ とすれば命題の第1の等式を得る。

$M=x$ の場合。左辺は $\operatorname{dB}_{\Delta\Xi}(N)$ である。 $x\notin\operatorname{set}(\Delta)$ であるから $\operatorname{idx}_{\Delta\,(x)\,\Xi}(x)=c$ であり、右辺は $\operatorname{sub}_c(\uparrow_c^0D,\mathsf v_c)=\uparrow_c^0D$ である。補題 7.3により両辺は一致する。

$M=z\ne x$ の場合。左辺は $\operatorname{dB}_{\Delta\Xi}(z)$ である。 $z\in\operatorname{set}(\Delta)$ ならば、二つの束縛文脈における指標はともに $\operatorname{idx}_\Delta(z)<c$ であり、 $\operatorname{sub}_c$ はこれを変えない。 $z\notin\operatorname{set}(\Delta)$ ならば $z\in\operatorname{set}(\Xi)$ であり、 $\operatorname{idx}_{\Delta\,(x)\,\Xi}(z)=c+1+\operatorname{idx}_\Xi(z)>c$ であるから、 $\operatorname{sub}_c$ は指標を一つ減らして $c+\operatorname{idx}_\Xi(z)$ とする。これは $\operatorname{idx}_{\Delta\Xi}(z)$ に等しい。

$M=M_1M_2$ の場合。代入、翻訳、 $\operatorname{sub}_c$ のいずれも適用について準同型であるから、二つの帰納法の仮定を合わせる。

$M=\lambda u.M_0$ の場合。代表元の選び方により $u\ne x$ かつ $u\notin\operatorname{FV}(N)$ であり、 $M[x:=N]=\lambda u.\bigl(M_0[x:=N]\bigr)$ である。左辺は $\mathsf l\,\operatorname{dB}_{u\cdot\Delta\Xi}\bigl(M_0[x:=N]\bigr)$ である。右辺は

\operatorname{sub}_c\Bigl(\uparrow_c^0D, \mathsf l\,\operatorname{dB}_{u\cdot\Delta\,(x)\,\Xi}(M_0)\Bigr) =\mathsf l\,\operatorname{sub}_{c+1}\Bigl(\uparrow_1^0\uparrow_c^0D, \operatorname{dB}_{u\cdot\Delta\,(x)\,\Xi}(M_0)\Bigr)

である。補題 6.2を $b=0$ として用いると $\uparrow_1^0(\uparrow_c^0D)=\uparrow_{c+1}^0D$ であるから、右辺は $\mathsf l\,\operatorname{sub}_{c+1}\bigl(\uparrow_{c+1}^0D,\operatorname{dB}_{u\cdot\Delta\,(x)\,\Xi}(M_0)\bigr)$ である。束縛文脈 $u\cdot\Delta$ は $x\notin\operatorname{set}(u\cdot\Delta)$ と $\operatorname{set}(u\cdot\Delta)\cap\operatorname{FV}(N)=\varnothing$ を満たし、 $\operatorname{FV}(M_0)\subseteq\operatorname{FV}(M)\cup\{u\}$ である。したがって、 $M_0$ と $u\cdot\Delta$ に対する帰納法の仮定が両辺を一致させる。

変数、適用、抽象の三つの構文形を尽くしたので、一般化した主張が成り立つ。第2の等式は、 $\lambda x.M$ と $V$ が閉項の場合に $\Xi=\varepsilon$ とし、翻訳の抽象に関する式から $R=\operatorname{dB}_{(x)}(M)$ であることを用いたものである。▨

8 ラムダ計算から Turing 機械へ

de Bruijn 項の値を $\mathsf lP$ とする。閉項上の一段評価を、次の部分関数として固定する。

定義 8.1. 閉 de Bruijn 項 $D$ に対する部分関数 $\operatorname{Step}_v(D)$ (one-step call-by-value evaluation function) を、値では未定義とし、値でない場合には次の規則で定める。

$D=\mathsf a(P,Q)$ かつ $P$ が値でない場合には、 $\operatorname{Step}_v(D) =\mathsf a(\operatorname{Step}_v(P),Q)$ とする。
$D=\mathsf a(\mathsf lR,Q)$ かつ $Q$ が値でない場合には、 $\operatorname{Step}_v(D) =\mathsf a(\mathsf lR,\operatorname{Step}_v(Q))$ とする。
$D=\mathsf a(\mathsf lR,Q)$ かつ $Q$ が値である場合には、 $\operatorname{Step}_v(D)=\operatorname{SubTop}(Q,R)$ とする。

各再帰呼出しは真部分項に対して行う。したがって、閉項 $D$ が値でなければ、三規則のうちちょうど一つが適用される。

前節の翻訳により、この部分関数は名前付き項の一段評価と対応する。

補題 8.2. $M$ を閉じた名前付き項とする。

$M$ が値であることと、 $\operatorname{dB}(M)$ が $\mathsf lP$ の形であることは同値である。
$M$ が値ならば $\operatorname{Step}_v(\operatorname{dB}(M))$ は定義されない。 $M$ が値でなければ、補題 1.2の一意な次項 $M'$ について $\operatorname{Step}_v\bigl(\operatorname{dB}(M)\bigr)=\operatorname{dB}(M')$ である。

証明.(1)を示す。閉項は変数ではない。抽象の翻訳は $\mathsf l$ で始まり、適用の翻訳は $\mathsf a$ で始まる。定義 1.1の値は抽象であるから、両者は対応する。 $\operatorname{Step}_v$ は値で定義されないので、(2)の前半も従う。

(2)の後半を $M$ の構造に関する帰納法で示す。値でない閉項 $M$ は閉じた適用 $PQ$ であり、 $P$ と $Q$ も閉項である。翻訳は適用について準同型であるから、 $\operatorname{dB}(M)=\mathsf a(\operatorname{dB}(P),\operatorname{dB}(Q))$ である。

$P$ が値でない場合。補題 1.2の証明にある評価文脈 $[\,]Q$ により $M'=P'Q$ であり、 $P'$ は $P$ の一意な次項である。(1)により $\operatorname{dB}(P)$ は値ではないので、定義 8.1 (1)が適用され、 $\operatorname{Step}_v(\operatorname{dB}(M))=\mathsf a\bigl(\operatorname{Step}_v(\operatorname{dB}(P)),\operatorname{dB}(Q)\bigr)$ である。 $P$ に対する帰納法の仮定から $\operatorname{Step}_v(\operatorname{dB}(P))=\operatorname{dB}(P')$ であり、右辺は $\operatorname{dB}(P'Q)$ に等しい。

$P$ が値で $Q$ が値でない場合。 $P=\lambda x.M_0$ であるから $\operatorname{dB}(P)=\mathsf lR$ の形であり、 $\operatorname{dB}(Q)$ は値ではない。評価文脈 $P[\,]$ により $M'=PQ'$ である。定義 8.1 (2)と $Q$ に対する帰納法の仮定から結論を得る。

$P$ と $Q$ がともに値の場合。 $P=\lambda x.M_0$ であり、根のβ基の縮約により $M'=M_0[x:=Q]$ である。 $\operatorname{dB}(P)=\mathsf lR$ とすると、定義 8.1 (3)により $\operatorname{Step}_v(\operatorname{dB}(M))=\operatorname{SubTop}\bigl(\operatorname{dB}(Q),R\bigr)$ である。 $\lambda x.M_0$ と $Q$ は閉項であるから、命題 7.5の命題 7.5の第2の等式により、これは $\operatorname{dB}(M_0[x:=Q])$ に等しい。三つの場合は補題 1.2の場合分けと一致し、互いに排他的である。▨

補題 8.3. 符号化された閉じた de Bruijn 項 $D$ を入力として、 $D$ が値かどうかを判定し、値でなければ弱い値呼び評価の一意な次項 $\operatorname{Step}_v(D)$ を出力する決定性多テープ Turing 機械を構成することができる。出力は再び閉じた整形式項である。

証明. 機械は入力を左から走査し、作業テープ上のスタックを用いて接頭辞符号を構文木へ復号する。同じ走査で $\operatorname{WF}_0$ を検査することができる。作用子側から構文木を再帰的に下り、値の場合、作用子を一段評価する場合、引数を一段評価する場合、根のβ基を縮約する場合を判定する。再帰的探索は毎回真部分木へ進むので有限回で終了する。根のβ基に達した場合には、別の作業テープ上で $\uparrow$ と $\operatorname{sub}$ の構造再帰を実行する。指標は単項表現の $1$ の個数として加算、比較、1の減算を有限走査で実行することができる。補題 6.3により代入は全域で整形式を保存する。

閉じた de Bruijn 項が値でなければ、定義 8.1の三規則のうちちょうど一つが適用され、その右辺は真部分項に対する再帰と $\operatorname{SubTop}$ だけを用いる。したがって、機械の出力は $\operatorname{Step}_v$ の値そのものである。この出力が名前付き項の弱い値呼び一段評価と一致することは、補題 8.2が与える。構文木を接頭辞符号へ再符号化すれば、所要の多テープ機械を得る。▨

数値出力を判定するため、正準数値の de Bruijn 項を記述する。

定義 8.4 (値呼び Church 数の de Bruijn 符号).

\begin{aligned} C_0&=\mathsf l(\mathsf l\mathsf v_0),\\ C_{n+1} &=\mathsf l\bigl(\mathsf l( \mathsf a(\mathsf v_1, \mathsf a(\mathsf a(C_n,\mathsf v_1),\mathsf v_0)) )\bigr). \end{aligned}

この族を値呼び Church 数の de Bruijn 符号 (de Bruijn encoding of a call-by-value Church numeral) という。

$C_n$ が $\mathbf c_n$ の翻訳であることを確かめる。

補題 8.5. 全ての $n\in\mathbb N$ について $\operatorname{dB}(\mathbf c_n)=C_n$ である。

証明. 最初に、 $\operatorname{WF}_c(P)$ ならば $\uparrow_r^cP=P$ であることを $P$ の構造に関する帰納法で確かめる。変数では $\operatorname{WF}_c$ から指標が $c$ 未満であり、シフトはこれを変えない。適用では二つの部分項へ帰納法の仮定を用いる。抽象では、 $\operatorname{WF}_{c+1}$ を満たす本体へ切断位置 $c+1$ の帰納法の仮定を用いる。

$n$ に関する帰納法で主張を示す。 $\mathbf c_0=\lambda f.\lambda x.x$ であり、束縛文脈 $(x,f)$ において $\operatorname{idx}(x)=0$ であるから

\operatorname{dB}(\mathbf c_0)=\mathsf l\bigl(\mathsf l\,\mathsf v_0\bigr)=C_0

である。 $\mathbf c_{n+1}=\lambda f.\lambda x.f(\mathbf c_n\,f\,x)$ であり、束縛文脈 $(x,f)$ において $\operatorname{idx}(f)=1$ 、 $\operatorname{idx}(x)=0$ であるから

\operatorname{dB}(\mathbf c_{n+1}) =\mathsf l\Bigl(\mathsf l\bigl( \mathsf a(\mathsf v_1, \mathsf a(\mathsf a(\operatorname{dB}_{(x,f)}(\mathbf c_n),\mathsf v_1),\mathsf v_0)) \bigr)\Bigr)

である。 $\mathbf c_n$ は閉項であるから、補題 7.3を $\Delta=(x,f)$ 、 $\Xi=\varepsilon$ として用いると $\operatorname{dB}_{(x,f)}(\mathbf c_n)=\uparrow_2^0\operatorname{dB}(\mathbf c_n)$ である。帰納法の仮定により $\operatorname{dB}(\mathbf c_n)=C_n$ であり、補題 7.2 (1)により $\operatorname{WF}_0(C_n)$ である。したがって $\uparrow_2^0C_n=C_n$ であり、上の右辺は定義 8.4の $C_{n+1}$ に一致する。▨

補題 8.6. 有限 de Bruijn 項 $D$ の符号を入力として停止する決定性多テープ Turing 機械が存在する。この機械は、ある $n\in\mathbb N$ について $D=C_n$ であるとき、かつそのときに限り受理状態で停止し、出力テープへ単項表現 $1^n$ を残す。 $D$ がどの $C_n$ とも一致しない場合には、拒否状態で停止する。

証明. 機械は接頭辞符号を一回走査して有限構文木を復号し、符号が不正ならば拒否する。復号された木に対して、まず $\mathsf l(\mathsf l\mathsf v_0)$ と一致するかを調べる。一致すれば空の単項列を出力して受理する。

$\mathsf l(\mathsf l\mathsf v_0)$ と一致しない木に対しては、

\mathsf l\bigl(\mathsf l( \mathsf a(\mathsf v_1, \mathsf a(\mathsf a(R,\mathsf v_1),\mathsf v_0)) )\bigr)

という値呼び Church 数の再帰形を調べる。値呼び Church 数の再帰形でなければ拒否する。値呼び Church 数の再帰形であれば、作業テープの単項カウンタへ $1$ を一つ加え、真部分項 $R$ に同じ検査を行う。

各再帰呼出しは真部分項へ進むので、有限構文木に対する検査は有限回で止まる。 $C_{n+1}$ の再帰定義に関する帰納法により、機械は $C_n$ を受理して単項列 $1^n$ を出力する。逆に、機械が受理するならば、基底形 $\mathsf l(\mathsf l\mathsf v_0)$ と、基底形に到達するまでに繰り返し確認した値呼び Church 数の再帰形から、同じ帰納法により入力はただ一つの $C_n$ である。▨

定理 8.7. 部分関数 $f\colon\mathbb N^k\rightharpoonup\mathbb N$ を強く表現する閉項 $F$ から、 $f$ を計算する Turing 機械 $M_F$ を構成することができる。ラムダ評価が $\mathbf c_n$ で停止する場合には $M_F$ は単項表現の $n$ を出力して停止し、ラムダ評価が無限ならば $M_F$ も停止しない。

証明.定義 7.1の翻訳を用いて $\operatorname{dB}(F)$ を作り、その二進符号を機械の有限制御へ固定する。入力された単項表現 $x_1,\ldots,x_k$ から定義 8.4の $C_{x_1},\ldots,C_{x_k}$ を作る。補題 8.5により $C_{x_i}=\operatorname{dB}(\mathbf c_{x_i})$ であり、翻訳は適用について準同型であるから、これらを $\mathsf a$ で左結合に組んだ項は $\operatorname{dB}(F\,\mathbf c_{x_1}\cdots\mathbf c_{x_k})$ である。この項は補題 7.2 (1)により閉じた整形式項である。機械は補題 8.3の一段機械を反復する。補題 8.2により、反復の各段は名前付き項の一段評価と対応し、第 $s$ 段の項は $F\,\mathbf c_{x_1}\cdots\mathbf c_{x_k}$ から $s$ 段評価した閉項の翻訳である。

現在項が値ならば、補題 8.6の正準数値判定を行う。 $C_n$ なら $n$ を単項表現で出力して停止し、正準数値でない値なら無限ループへ入る。入力符号の破損または整形式でない途中項に対しても、防御的に無限ループへ入るものとする。強く表現する項から開始した計算では、入力符号の破損も整形式でない途中項も生じない。

$f(\vec x)=n$ ならば、強い表現により有限回の一段評価後に $\mathbf c_n$ へ達し、対応する翻訳は $C_n$ である。一段機械と数値判定は各回有限時間で終了するため、模倣機械は単項表現の $n$ を出力して停止する。 $f(\vec x)\mathord\uparrow$ ならば、ラムダ評価には常に次の一段がある。模倣機械は各一段を有限時間で実行した後に次の反復へ進むので、有限段で停止せず、Turing 機械の計算も無限になる。

得られた多テープ機械へ§E15.7 補題 1.2を適用すると、停止時には出力テープ上の正準な単項表現だけを残し、発散時には発散を保つ一テープ機械へ変換することができる。▨

9 計算可能性の一致

定理 9.1. 自然数上の部分関数 $f$ について、次の二条件は同値である。

$f$ は§E15.7 定義 1.1の意味で部分 Turing 計算可能である。
$f$ は閉じた型なしラムダ項によって、弱い値呼び評価の下で強く表現される。

両方向の変換は、定義される入力では同じ自然数を返し、定義されない入力では無限計算を生じる。

証明.(1) $\Rightarrow$ (2)は定理 4.1である。(2) $\Rightarrow$ (1)は定理 8.7である。二つの定理はいずれも停止時の値と発散を個別に保存するため、部分関数の定義域と定義域上の値が一致する。▨

値呼びラムダ計算可能性と部分 Turing 計算可能性の同値性は、Church–Turing の提唱を一つの定理だけから導くものではない。形式化された二つの計算模型について、相互の模倣を数学的に証明した結果である。本記事の結論は、閉項、正準 Church 数、左から右への弱い値呼び評価という明示した条件に依存する。強い評価や名前呼び評価を扱う場合には、評価規則と発散保存の証明を別に与える必要がある。

10 演習

問題 10.1.

$\mathsf{If}\,\mathsf F\,(\lambda d.\Omega)\,(\lambda d.\mathbf c_2)$ の評価列を示し、 $\Omega$ が評価されない理由を評価文脈から説明せよ。
原始再帰の構成で、初期対が $\langle\mathbf c_0,\mathbf c_{z_0}\rangle_v$ まで評価されなければ反復へ進めない理由を示せ。また、第 $j$ 段の不変条件から第 $j+1$ 段の不変条件を導け。
非有界最小化について、最小の零が存在する場合、途中で未定義値に達する場合、全ての値が正である場合の三つに分け、構成した項の停止または発散を示せ。
$\operatorname{WF}_d(N)$ と $\operatorname{WF}_{d+1}(P)$ を仮定し、 $\operatorname{SubTop}(N,P)$ が $\operatorname{WF}_d$ を満たすことを、変数の場合を三つに分けて示せ。
一段模倣機械が各回有限時間で停止することと、無限評価を模倣する機械が停止しないことを区別して説明せよ。
束縛文脈 $\Xi=(y,x)$ に対して $\operatorname{dB}_\Xi(\lambda x.x\,y)$ を計算せよ。また、 $\operatorname{idx}_\Xi$ が最小の添字を取る規約を採らない場合に、どの主張が成り立たなくなるかを述べよ。
直接模倣の遷移項について、 $D=L$ かつ $h=0$ の場合に左側リストの二つの分枝のどちらが選ばれるかを述べ、得られる値が§E15.4 定義 1.2の $C'$ を表すことを確かめよ。

解答 (演習の要点).

真偽値の選択後には第3引数の抽象だけが残り、 $\mathsf I$ への適用によって $\mathbf c_2$ を返す。 $\Omega$ は選ばれた評価文脈に入らない抽象の本体にある。
Church 数の反復では、初期値が値でなければ外側の適用を縮約することができない。第 $j$ 段の対へ $\mathsf{Step}_{\vec x}$ を適用し、二つの射影、後続者、 $G$ を順に評価すると、第 $j+1$ 段の対を得る。
最小の零が存在すれば有限個の正の検査後に真の分枝が候補を返す。最初の未定義値では $\mathsf{IsZero}$ の引数評価が発散する。全ての値が正なら、固定点の有限展開と次候補の検査が無限に続く。
変数指標 $i$ が $0$ より小さい場合は存在せず、 $i=0$ なら $N$ を代入し、 $i>0$ なら $\mathsf v_{i-1}$ とする。変数指標が $i=0$ の場合の整形式性は $\operatorname{WF}_d(N)$ から、変数指標が $i>0$ の場合の整形式性は $i<d+1$ から従う。抽象の内部では同じ議論を切断位置を一つ増やして用いる。
一段処理は有限構文木の真部分木へ再帰するので毎回終了する。元の評価が無限なら、閉項の進行により各有限段階の後にも次項があり、模倣機械は有限回の反復では停止条件へ到達しない。
束縛文脈は $(x,y,x)$ へ延び、 $\operatorname{idx}(x)=0$ 、 $\operatorname{idx}(y)=1$ であるから $\operatorname{dB}_\Xi(\lambda x.x\,y)=\mathsf l\,\mathsf a(\mathsf v_0,\mathsf v_1)$ である。最小の添字を取らない規約では、内側の束縛子が同名の外側の束縛子を遮蔽することが指標に現れない。その場合、補題 7.2 (2)が成り立たず、これに依拠する補題 7.4のアルファ同値の不変性も失われる。
$h=0$ では左側リストが $[\,]_v$ であるから、補題 5.2 (3)により空リストの分枝が選ばれ、 $\mathsf{Conf}\,\overline{q'}\,\mathsf{Nil}\,\overline{a'}\,(\mathsf{Rg}\,w)$ へ進む。§E15.4 定義 1.2では $h'=0$ かつ $T'(0)=a'$ であり、 $T'$ は他の位置で $T$ と一致する。したがって左側は長さ $0$ 、現在記号は $\overline{T'(0)}=\overline{a'}$ 、右側は変わらず、末尾が空白であるという条件も $T$ から引き継がれる。

▨

§E15.9ラムダ計算と Turing 機械の同値性

1 弱い値呼び評価

2 値呼び Church 符号

3 部分ミュー再帰関数の表現

4 Turing 機械からラムダ計算へ

5 Turing 機械の配置の直接符号化

6 de Bruijn 符号と代入

7 名前付き項から de Bruijn 項への翻訳

8 ラムダ計算から Turing 機械へ

9 計算可能性の一致

10 演習

参考文献

前提記事