計算理論・ラムダ計算の問題

以下、項 $g$ と項 $t$ に対して $g^{j}t=g(g(\cdots (gt)\cdots ))$（$g$ が $j$ 個、$g^{0}t=t$）と書く。

補題 1. 任意の項 $g$ と $m\ge 0$ に対し $c_{m}g{\to }_{\beta }\lambda z.g^{m}z$（$z$ は $g$ に自由に現れない変数）。

実際、$c_{m}g=(\lambda f.\lambda z.f^{m}z)g$ を $1$ 回 $\beta$ 簡約すると、$f$ に $g$ が代入されて $\lambda z.g^{m}z$ になる。

補題 2. $x$ を変数、$b,n\ge 0$ とし、$h=\lambda y.x^{b}y$ とおく。このとき $c_{n}h{\to }_{\beta }^{\ast }\lambda y.x^{nb}y$ である。

補題 1 より $c_{n}h{\to }_{\beta }\lambda z.h^{n}z$ である。どの項 $t$ についても $ht=(\lambda y.x^{b}y)t{\to }_{\beta }{x}^{b}t$ が成り立つ。$h^{n}z=h(h(\cdots (hz)\cdots ))$ の一番内側から順に簡約すると
$$hz{\to }_{\beta }{x}^{b}z,h(x^{b}z){\to }_{\beta }{x}^b(x^{b}z)=x^{2b}z,\dots$$
となり、$n$ 回の簡約で $x^{nb}z$ に達する（$n=0$ のときは最初から $z=x^{0}z$）。よって $c_{n}h{\to }_{\beta }^{\ast }\lambda z.x^{nb}z$ で、これは $\lambda y.x^{nb}y$ と $\alpha$ 同値である。

補題 3. $x$ を変数、$n\ge 0$ とする。$j\ge 1$ に対して $c_n^{j}x{\to }_{\beta }^{\ast }\lambda y.x^{n^j}y$ である（$c_n^{j}x=c_n(c_n(\cdots (c_{n}x)\cdots ))$、$c_n$ が $j$ 個）。

$j$ についての帰納法で示す。
- $j=1$: 補題 1 より $c_{n}x{\to }_{\beta }\lambda y.x^{n}y$。
- $j\to j+1$: $c_n^{j+1}x=c_n(c_n^{j}x)$ であり、帰納法の仮定より内側の $c_n^{j}x$ は $h=\lambda y.x^{n^j}y$ に簡約される。補題 2（$b=n^j$）より $c_{n}h{\to }_{\beta }^{\ast }\lambda y.x^{n\cdot n^j}y=\lambda y.x^{n^{j+1}}y$。

補題 4. $m\ge 1$, $n\ge 0$ に対し、$c_m{c}_n{\to }_{\beta }^{\ast }{c}_{n^m}$ である。

補題 1 より $c_m{c}_n{\to }_{\beta }\lambda x.c_n^{m}x$（$x$ は $c_n$ に自由に現れない）。抽象の本体に補題 3（$j=m\ge 1$）を使うと
$$\lambda x.c_n^{m}x{\to }_{\beta }^{\ast }\lambda x.\lambda y.x^{n^m}y,$$
これは $c_{n^m}=\lambda f.\lambda x.f^{n^m}x$ と $\alpha$ 同値である。

（$m\ge 1$ の仮定は必要である。$m=0$ では $c_0{c}_n{\to }_{\beta }\lambda x.x$ となり、$\eta$ 簡約を使わない限り $c_1$ にはならない。本問で使うのは $m=3,2,8$ だけである。）

本問の計算.

補題 4 より
$$c_3{c}_2{\to }_{\beta }^{\ast }{c}_{2^3}=c_8,c_2{c}_3{\to }_{\beta }^{\ast }{c}_{3^2}=c_9.$$
$M$ の左右の部分項をそれぞれ簡約すれば $M{\to }_{\beta }^{\ast }{c}_8{c}_9$ であり、再び補題 4（$m=8$, $n=9$）より
$$c_8{c}_9{\to }_{\beta }^{\ast }{c}_{9^8}.$$
$c_{9^8}=\lambda f.\lambda x.f^{9^8}x$ は $\beta$ 基（$(\lambda u.P)Q$ の形の部分項）をもたないので正規形である。チャーチ・ロッサーの定理より正規形は（$\alpha$ 同値を除いて）一意なので、$M$ の正規形は $c_{9^8}$ であり、
$$k=9^8=(9^4{)}^2=6561^2=43046721.$$

一般に $c_m{c}_n=(\lambda f.\lambda x.f^{m}x)c_n{\to }_{\beta }\lambda x.c_n^{m}x$ であり、$c_{n}g{\to }_{\beta }\lambda x.g^{n}x$ より $c_n^m$（$c_n$ を $m$ 回合成したもの）は $\lambda x.$ の中で $n$ 回適用を $m$ 回重ねたもの、すなわち $c_{n^m}$ に簡約される。実際、$c_n$ は関数 $g$ を $g^n$ に写すので、$c_n$ を $m$ 回合成した作用は $f\mapsto f^{n^m}$ となる。よって $c_m{c}_n{=}_{\beta }{c}_{n^m}$。\n\n$c_3{c}_2=c_{2^3}=c_8$、$c_2{c}_3=c_{3^2}=c_9$。\n\n$M=c_8{c}_9=c_{9^8}$。$9^8=3^{16}=43046721$。\n\n検算: $c_2{c}_2=c_{2^2}=c_4$ は $\lambda x.c_2(c_{2}x)$、すなわち $f\mapsto (f^2{)}^2=f^4$ で一致。よって $k=9^8=43046721$。