BarendregtのコンビネータX≡λx.x(xS(KK))KからK,Sを導く

Barendregtのコンビネータは、
$$X\equiv\lambda x.x(xS(KK))K$$

と定義される。このコンビネータのみで$K,S$を導くことができる。

The Lambda Calculus: Its Syntax and Semantics
H. P. Barendregt
8.5.16 (ii)

XX≡KKを求める

$XX\equiv(\lambda x.x(xS(KK))K)X\equiv X(XS(KK))K$

ここで
$XS(KK)\equiv(\lambda x.x(xS(KK))K)S(KK)$
$\rightarrow S(SS(KK))K (KK)$
$\rightarrow (SS(KK))(KK) (K(KK))$
$\rightarrow S(KK) ((KK)(KK)) (K(KK))$
$\rightarrow S(KK) K (K(KK))$ by $(KK)(KK)\rightarrow K$
$\rightarrow (KK)(K(KK)) (K(K(KK)))$
$\rightarrow K (K(K(KK)))$

$XX\equiv X(XS(KK))K
\equiv X(K(K(K(KK))))K$
$\equiv(\lambda x.x(xS(KK))K)(K(K(K(KK))))K$
$\rightarrow(K(K(K(KK))))(K(K(K(KK)))S(KK))KK$
$\rightarrow K(K(KK))KK
\rightarrow (K(KK))K
\rightarrow KK$

$$XX\equiv KK$$

XXX≡Kを求める

$XXX\equiv(XX)X
\equiv(KK)X
\rightarrow K$

$$XXX\equiv K$$

XK≡S

$XK\equiv(\lambda x.x(xS(KK))K)K$
$\rightarrow K(KS(KK))K
\rightarrow K(S)K
\rightarrow S$

$$XK\equiv S$$