コンビネータ論理の問題。
Lambda-Calculus and Combinators: An Introduction
Hindley & Seldin より
以前のブログで一つの解答を示したが、実はもう一つ解答があるので、それを紹介する。
Exercise 2.34(a)
ペア生成コンビネータ$D$と次の条件を満たす二つの射影$D_1, D_2$を作成せよ。
$$D_1(Dxy)\ \triangleright_\omega\ x\quad(1)$$
$$D_2(Dxy)\ \triangleright_\omega\ y\quad(2)$$
もう一つの解答
$$D\equiv [x,y,z].z(Ky)x$$とする。$\overline{n}$をチャーチ数とすると、
$$D_1\equiv\lambda x.x\overline{0},\quad
D_2\equiv\lambda x.x\overline{1}$$とすると(1)と(2)が成り立つ。
実際にそうなるかを検証する。
Dについて
$D\equiv[x,y,z].z(Ky)x\equiv[x].([y].([z].z(Ky)x)))$なので
zでの抽象化
$[z].z(Ky)x\equiv S([z].z(Ky))([z].x)$
$\equiv S(S([z].z)([z].Ky))(Kx)$
$\equiv S(SI(K(Ky)))(Kx)$
従って
$$[z].z(Ky)x\equiv S(SI(K(Ky)))(Kx)$$
上式の検証：
$S(SI(K(Ky)))(Kx) z\equiv (SI(K(Ky)))z((Kx)z)$
$Iz((K(Ky))z) x\equiv z(Ky) x$ Q.E.D$\quad(3)$
更にyでの抽象化
$[y].([z].z(Ky)x)\equiv [y].S(SI(K(Ky)))(Kx)$
$\equiv S([y].S(SI(K(Ky))))([y].Kx)$
ここで、
$[y].S(SI(K(Ky)))
\equiv S([y].S)([y].SI(K(Ky)))$
$\equiv S(KS)(S([y].SI)([y].K(Ky)))$
$\equiv S(KS)(S(K(SI))(S([y].K)([y].Ky)))$
$\equiv S(KS)(S(K(SI))(S(KK)K))$
それを元の式に代入して
$$[y].([z].z(Ky)x)$$
$$\equiv S(S(KS)(S(K(SI))(S(KK)K)))(K(Kx))$$となる。
上式を検証：
$S (S(KS) (S(K(SI)) (S(KK)K))) (K(Kx)) y$
$\equiv S(KS) (S(K(SI))(S(KK)K)) y ((K(Kx)) y)$
$\equiv (KS) y (S (K(SI)) (S(KK)K) y) (Kx)$
$\equiv S ((K(SI)) y (S(KK)K y)) (Kx)$
$\equiv S (SI ((KK)y (Ky))) (Kx)$
$\equiv S (SI (K (Ky))) (Kx) $Q.E.D.$\quad(4)$
更にxでの抽象化
$[x].([y].([z].z(Ky)x)))$
$\equiv[x].S (S(KS)(S(K(SI))(S(KK)K))) (K(Kx))$
$\equiv S([x].S(S(KS)(S(K(SI))(S(KK)K)))) ([x].K(Kx))$
この時$[x].K(Kx)\equiv S(KK)Kなので$
$\equiv S (K(S(S(KS)(S(K(SI))(S(KK)K))))) (S(KK)K)$
従って、
$$D\equiv
[x].([y].([z].z(Ky)x)))$$
$$\equiv S (K(S(S(KS)(S(K(SI))(S(KK)K))))) (S(KK)K)$$
上式を検証：
$S (K(S(S(KS)(S(K(SI))(S(KK)K))))) (S(KK)K) x$
$\equiv (K(S(KS)(S(K(SI))(S(KK)K))))) x ((S(KK)K) x)$
$\equiv S(S(KS)(S(K(SI))(S(KK)K))) ((KK)x (Kx))$
$\equiv S(S(KS)(S(K(SI))(S(KK)K))) (K (Kx))\quad$Q.E.D.$\quad(5)$
Dxyについて
$Dxy$
$\equiv S (K(S(S(KS)(S(K(SI))(S(KK)K))))) (S(KK)K) x y$
$\equiv S(S(KS)(S(K(SI))(S(KK)K))) (K (Kx)) y\quad$ by$(5)$
$\equiv S (SI (K (Ky)))\quad$by$(4)$
D1とD2について
$$D_1\equiv\lambda x.x\overline{0},\quad
D_2\equiv\lambda x.x\overline{1}$$とはどんな式になるだろうか。
チャーチ数
チャーチ数についてはこちらを参照。
チャーチ数$\overline{0},\overline{1}$は以下の通りになる。
$\overline{0}\equiv\lambda ab.b\quad\equiv\lambda fx.x$とも書かれる。
$\overline{1}\equiv\lambda ab.ab\quad\equiv\lambda fx.f(x)$とも書かれる。
どちらも同じ意味である。ちなみに$\overline{2}$は、
$\overline{2}\equiv\lambda ab.aab\quad\equiv\lambda fx.f(f(x))$
$\overline{0},\overline{1}$のコンビネータ式は、
$\overline{0}\equiv\lambda ab.b\equiv[a,b].b\equiv[a].([b].b)\equiv[a].I\equiv KI$
$\overline{1}\equiv\lambda ab.ab\equiv[a,b].ab\equiv[a].([b].ab)\equiv[a].a\equiv I$
D1(Dxy),D2(Dxy)を求める
$D_1(Dxy)$は
$D_1(Dxy)\equiv(\lambda x.x\overline{0})(Dxy)
\equiv(Dxy)\overline{0}$
$\equiv S (SI(K(Ky))) (Kx) \overline{0}$
$\equiv SI(K(Ky))\overline{0} ((Kx) \overline{0})$
$\equiv I\overline{0} (K(Ky)\overline{0}) (x)\equiv \overline{0} (Ky) x$
$\equiv(\lambda ab.b)(Ky)x\equiv x$
よって$$D_1(Dxy)\ \triangleright_\omega\ x$$
一方、$D_2(Dxy)$は、
$D_2(Dxy)\equiv(\lambda x.x\overline{1})(Dxy)
\equiv(Dxy)\overline{1}$
$\equiv S (SI(K(Ky))) (Kx) \overline{1}$
$\equiv SI(K(Ky))\overline{0} ((Kx) \overline{1})$
$\equiv I\overline{1} (K(Ky)\overline{1}) (x)\equiv \overline{1} (Ky) x$
$\equiv(\lambda ab.ab)(Ky)x\equiv (Ky)x\equiv x$
よって$$D_2(Dxy)\ \triangleright_\omega\ y$$
よって条件を満たすことが分かった。
$n\geq1$の一般のチャーチ数$\overline{n}\equiv\lambda ab.a^n b$についても
$D_{n+1}(Dxy)\equiv(\lambda x.x\overline{n})(Dxy)
\equiv(Dxy)\overline{n}$
$\equiv S (SI(K(Ky))) (Kx) \overline{n}$
$\equiv\overline{n} (Ky) x$
$\equiv(\lambda ab.a^n b)(Ky)x\equiv (Ky)^n x$
$\equiv(Ky)((Ky)((Ky)(\cdots((Ky)((Ky)x))\cdots)))$
$\equiv(Ky)((Ky)((Ky)(\cdots(y)\cdots)))\equiv(Ky)y\equiv y$
つまり、
$D_0(Dxy)\ \triangleright_\omega\ x$ if $n=0$
$D_{n+1}(Dxy)\ \triangleright_\omega\ y$ if $n\geq 1$
もう一つ別の解が見つかった。チャーチ数というのは不思議なふるまいをするんだねえ。