Meredithのコンビネータ$H$は、
$$H\equiv\lambda abcd.cd(a(\lambda x.d))$$
と定義される。このコンビネータのみで$K,S$を生成することができる。
The Lambda Calculus: Its Syntax and Semantics
H. P. Barendregt
8.5.16 (i)
それを示す手順は複雑なので、順次説明する。
事前定義 H2 ≡ HH, H3 ≡ H2 H
$$H_1\equiv H$$
$$H_{n+1}\equiv H_n H$$
と置く。
$H_2\equiv HH\equiv\lambda abcd.cd(a(\lambda x.d))H$
$\rightarrow\lambda bcd.cd(H(\lambda x.d))$
$\equiv\lambda bcd.cd((\lambda yzuv.uv(y(\lambda w.v)))(\lambda x.d))$
$\rightarrow\lambda bcd.cd(\lambda zuv.uv((\lambda x.d)(\lambda w.v)))$
$\rightarrow\lambda bcd.cd(\lambda zuv.uvd)$
$\equiv_\alpha\lambda ijk.jk(\lambda zuv.uvk)$ 変数の置き換え
$$H_2\equiv\lambda bcd.cd(\lambda zuv.uvd)$$
$H_3\equiv H_2 H
\equiv(\lambda bcd.cd(\lambda zuv.uvd))H$
$\rightarrow\lambda cd.cd(\lambda zuv.uvd)$
$$H_3\equiv\lambda cd.cd(\lambda zuv.uvd)$$
U ≡ H3 H2
$U\equiv H_3 H_2
\equiv(\lambda cd.cd(\lambda zuv.uvd))H_2$
$\rightarrow\lambda d.H_2d(\lambda zuv.uvd)$
$\equiv\lambda d.(\lambda ijk.jk(\lambda pmn.mnk))d(\lambda zuv.uvd)$
$\rightarrow\lambda d.\lambda k.(\lambda zuv.uvd)k(\lambda pmn.mnk)$
$\rightarrow\lambda dk.(\lambda zuv.uvd)k(\lambda pmn.mnk)$
$\rightarrow\lambda dk.\lambda v.(\lambda pmn.mnk)vd$
$\rightarrow\lambda dkv.\lambda n.dnk
\equiv\lambda dkvn.dnk$
$\equiv_\alpha\lambda abcd.adb$
H4 ≡ H3 H
$H_4\equiv H_3 H
\equiv(\lambda cd.cd(\lambda zuv.uvd))H$
$\equiv\lambda d.Hd(\lambda zuv.uvd)$
$\equiv_\alpha\lambda y.Hy(\lambda zuv.uvy)$
$\equiv\lambda y.(\lambda abcd.cd(a(\lambda x.d)))y(\lambda zuv.uvy)$
$\rightarrow\lambda y.\lambda cd.cd(y(\lambda x.d))$
$\equiv\lambda ycd.cd(y(\lambda x.d))$
$\equiv_\alpha\lambda abc.bc(a(\lambda d.c))$
$$H_4 \equiv\lambda abc.bc(a(\lambda d.c))$$
H4(H4 U H2)H4 ≡ Kの証明
$H_4\ U H_2$
$\equiv(\lambda abc.bc(a(\lambda d.c)))UH_2$
$\rightarrow \lambda c.H_2c(U(\lambda d.c))$
$\equiv_\alpha\lambda x.H_2x(U(\lambda y.x))$
$\rightarrow\lambda x.(\lambda bcd.cd(\lambda zuv.uvd))x(U(\lambda y.x))$
$\rightarrow\lambda x.\lambda d.U(\lambda y.x)d(\lambda zuv.uvd)$
$\rightarrow\lambda xw.U(\lambda y.x)w(\lambda zuv.uvw)$
$\equiv\lambda xw.(\lambda abcd.adb)(\lambda y.x)w(\lambda zuv.uvw)$
$\rightarrow\lambda xw.\lambda d.(\lambda y.x)dw
\rightarrow\lambda xwd.xw
\equiv_\alpha\lambda xyz.xy$
$$H_4\ U H_2
\equiv\lambda xyz.xy$$
$H_4(H_4\ UH_2)H_2$
$\equiv(\lambda abc.bc(a(\lambda d.c)))(\lambda xyz.xy)H_2$
$\rightarrow\lambda c.H_2c((\lambda xyz.xy)(\lambda d.c))$
$\rightarrow\lambda c.H_2c(\lambda yz.(\lambda d.c)y)$
$\rightarrow\lambda c.H_2c(\lambda yz.c)$
$\equiv_\alpha\lambda i.H_2i(\lambda jk.i)$
$\equiv\lambda i.(\lambda bcd.cd(\lambda zuv.uvd))i(\lambda jk.i)$
$\rightarrow\lambda i.\lambda d.(\lambda jk.i)d(\lambda zuv.uvd)$
$\rightarrow\lambda id.i\equiv K$
$$H_4(H_4\ UH_2)H_2\equiv K$$
X ≡ H4(K H4), Y≡XX
$X\equiv H_4(KH_4)$
$\equiv(\lambda abc.bc(a(\lambda d.c)))(KH_4)$
$\rightarrow\lambda bc.bc(KH_4(\lambda d.c))$
$\rightarrow\lambda bc.bcH_4$
$$X\equiv\lambda bc.bcH_4$$
$Y\equiv XX$
$\equiv(\lambda bc.bcH_4)X
\rightarrow\lambda c.XcH_4
\rightarrow\lambda x.XxH_4$
$\equiv\lambda x.(\lambda bc.bcH_4)xH_4$
$\equiv\lambda x.xH_4H_4$
$$Y\equiv\lambda x.xH_4H_4$$
Z ≡ H4(H4Y)(KH4)
$Z\equiv H_4(H_4 Y)(KH_4)$
$\equiv(\lambda abc.bc(a(\lambda d.c)))(H_4Y)(KH_4)$
$\equiv\lambda c.(KH_4)c(H_4Y(\lambda d.c))$
$\rightarrow\lambda c.H_4(H_4Y(\lambda d.c))
\equiv_\alpha\lambda x.H_4(H_4Y(\lambda y.x))$
ここで
$H_4Y(\lambda y.x)$
$\equiv(\lambda abc.bc(a(\lambda d.c)))Y(\lambda y.x)$
$\rightarrow\lambda c.(\lambda y.x)c(Y(\lambda d.c))$
$\rightarrow\lambda c.x(Y(\lambda d.c))$
$\rightarrow\lambda c.x((\lambda y.yH_4H_4)(\lambda d.c))$
$\rightarrow\lambda c.x((\lambda d.c)H_4H_4)$
$\rightarrow\lambda c.x(cH_4)$
$\equiv_\alpha\lambda z.x(zH_4)$
$Z\equiv\lambda x.H_4(H_4Y(\lambda y.x))$
$\equiv\lambda x.(\lambda abc.bc(a(\lambda d.c)))(\lambda z.x(zH_4))$
$\equiv\lambda x.(\lambda bc.bc((\lambda z.x(zH_4))(\lambda d.c)))$
$\equiv\lambda x.(\lambda bc.bc(x((\lambda d.c)H_4)))$
$\rightarrow\lambda x.\lambda bc.bc(xc)$
$\equiv\lambda xbc.bc(xc)$
$\equiv_\alpha\lambda xyz.yz(xz)$
$$Z\equiv\lambda xyz.yz(xz)$$
X(UZ) ≡ S
$X(UZ)$
$\equiv(\lambda bc.bcH_4)(UZ)
\rightarrow\lambda c.(UZ)cH_4
\equiv_\alpha\lambda x.(UZ)xH_4$
$\rightarrow\lambda x.((\lambda abcd.adb)Z)xH_4$
$\rightarrow\lambda x.\lambda d.Zdx
\equiv_\alpha\lambda ab.Zba$
$\equiv\lambda ab.(\lambda xyz.yz(xz))ba$
$\rightarrow\lambda ab.\lambda z.az(bz)$
$\equiv_\alpha\lambda xyz.xz(yz)
\equiv S$
$$X(UZ)\equiv S$$