ペアリングとは

コンピュータではリストやタプル構造が使われる。ペアとは、2変数のタプルのことで、変数の順序は固定されている。ラムダ計算の世界では、驚くべきことにこれらのデータ構造は関数で表される。変数$M,N$とのペア$\langle M,N\rangle$は
$$\langle M,N\rangle\equiv\lambda z.zMN$$と表現される。ここで、
$${\bf left}\equiv\lambda p.p(\lambda xy.x)$$

$${\bf right}\equiv\lambda p.p(\lambda xy.y)$$

と定義すると、
$${\bf left}\langle M,N\rangle\rightarrow M$$

$${\bf right}\langle M,N\rangle\rightarrow N$$

実際、
${\bf left}\langle M,N\rangle$
$\equiv(\lambda p.p(\lambda xy.x))(\lambda z.zMN)$
$\rightarrow(\lambda z.zMN)(\lambda xy.x)
\rightarrow(\lambda xy.x)MN\rightarrow M$
${\bf right}$の場合も同様。

タプル

$n$項のタプル$\langle M_1,\dots,M_n\rangle$も一般化して、
$$\langle M_1,\dots,M_n\rangle\equiv\lambda z.zM_1,\dots,M_n$$と定義できる。$i$番目のprojectionとして、
$$\pi_i^n\equiv\lambda p.p(\lambda x_1\dots x_n.x_i)$$と定義すれば、全ての$1\leq i\leq n$について$$\pi_i^n\langle M_1,\dots,M_n\rangle\ \rightarrow_\beta\ M_i$$

参考：
Lecture Notes on the Lambda Calculus (PDF)
Peter Selinger (2008)

Exercise 2.34(a)

ペアリングコンビネータ$D$と次の条件を満たす二つの射影$D_1, D_2$を作成せよ。
$$D_1(Dxy)\ \triangleright_\omega\ x$$

$$D_2(Dxy)\ \triangleright_\omega\ y$$

回答

$D\equiv [x,y,z].zxy$及び、$D_i\equiv [u].u([x_1,x_2].x_i)$とすると成り立つ。$D_i$は$i$番目のペアの要素を取り出すコンビネータである。
実際にそうなるかを検証する。

Dについて

$D\equiv[x,y,z].zxy\equiv[x].([y].([z].zxy)))$なので

$z$での抽象化
$[z].zxy\equiv S([z].zx)([z].y)$
$\equiv S(S([z].z)([z].x))(Ky)$
$\equiv S(SI(Kx))(Ky)\equiv[z].zxy$

上式の検証：
$S(SI(Kx))(Ky) z\equiv (SI(Kx))z((Ky)z)$
$Iz((Kx)z)y\equiv z(x)y\equiv zxy$ Q.E.D$...(1)$

更に$y$での抽象化
$[y].([z].zxy)\equiv [y].S(SI(Kx))(Ky)$
$\equiv S([y].S(SI(Kx)))([y].Ky)$
$\equiv S(K(S(SI(Kx)))K$

上式を検証：
$S(K(S(SI(Kx)))Ky$
$\equiv K(S(SI(Kx)))y(Ky)$
$\equiv S(SI(Kx))(Ky)$ Q.E.D...(2)

更に$x$での抽象化
$[x].([y].([z].zxy)))$
$\equiv[x].S(K(S(SI(Kx)))K$
$\equiv S([x].S(K(S(SI(Kx)))))([x].]K)$
$\equiv S(S([x].S)([x].K(S(SI(Kx))))) (KK)$
$\equiv S(S(KS)(S([x].K)([x].S(SI(Kx))))) (KK)$
$\equiv S(S(KS)(S(KK)(S([x].S)([x].SI(Kx))))) (KK)$
$\equiv S(S(KS)(S(KK)(S(KS)(S([x].SI)([x].Kx))))) (KK)$
$\equiv S(S(KS)(S(KK)(S(KS)(S(K(SI))K)))) (KK)$
従って、
$$D\equiv
[x].([y].([z].zxy)))$$

$$\equiv S(S(KS)(S(KK)(S(KS)(S(K(SI))K)))) (KK)$$

上式を検証：
$S(S(KS)(S(KK)(S(KS)(S(K(SI))K)))) (KK) x$
$\equiv S(KS)(S(KK)(S(KS)(S(K(SI))K))))x ((KK)x)$
$\equiv (KS)x (S(KK)(S(KS)(S(K(SI))K))x) K$
$\equiv S ((KK)x (S(KS)(S(K(SI))K)x)) K$
$\equiv S (K ((KS)x (S(K(SI))Kx))) K$
$\equiv S (K (S ((K(SI))x (Kx)))) K$
$\equiv S (K (S (SI (Kx)))) K$ Q.E.D....(3)

Dxyについて

$Dxy\equiv S(S(KS)(S(KK)(S(KS)(S(K(SI))K)))) (KK) xy$
$\equiv S (K (S (SI(Kx)))) Ky$ by (3)
$\equiv S(SI(Kx))(Ky)$ by (2)

Diについて

$D_i\equiv [u].u([x_1,x_2].x_i)$とすると
$D_1\equiv [u].u([x_1,x_2].x_1)$
$D_2\equiv [u].u([x_1,x_2].x_2)$
なので、
$D_1\equiv [u].u([x_1].([x_2].x_1))
\equiv [u].u([x_1].Kx_1)\equiv[u].u(K)$
$\equiv S([u].u)([u].K)\equiv SI(KK)$
よって$$D_1\equiv SI(KK)$$

$D_1(Dxy)\equiv SI(KK)(S(SI(Kx))(Ky))$
$\equiv I(S(SI(Kx))(Ky)) ((KK)(S(SI(Kx))(Ky)))$
$\equiv \{S(SI(Kx))(Ky)\} K$
$\equiv SI(Kx)K ((Ky)K)$
$\equiv IK ((Kx)K) y$
$\equiv K x y\equiv x$
よって$$D_1(Dxy)\ \triangleright_\omega\ x$$

一方、$D_2$は、
$D_2\equiv [u].u([x_1].([x_2].x_2))
\equiv [u].u([x_1].KI)\equiv[u].u(KI)$
$\equiv S([u].u)([u].KI)\equiv SI(K(KI))$
よって$$D_2\equiv SI(K(KI))$$

$D_2(Dxy)\equiv SI(K(KI))(S(SI(Kx))(Ky))$
$\equiv I(S(SI(Kx))(Ky)) ((K(KI))(S(SI(Kx))(Ky)))$
$\equiv (S(SI(Kx))(Ky)) (KI)$
$\equiv (SI(Kx))(KI)) ((Ky)(KI))$
$\equiv SI(Kx)(KI) y$
$\equiv I(KI) ((Kx)(KI)) y$
$\equiv (KI) (x) y\equiv I y\equiv y$
よって$$D_2(Dxy)\ \triangleright_\omega\ y$$

よって条件を満たすことが分かった。他の組み合わせでもうまくいく場合があるので、後程掲載する。