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$
ここで
$$\begin{array}{rl}
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))\quad\text{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\\
\end{array}$$
XXX≡Kを求める
$$\begin{array}{rl}
XXX&\equiv&(XX)X\\
&\equiv&(KK)X\\
&\rightarrow&K\\
\\
XXX&\equiv&K
\end{array}$$
XK≡S
$$\begin{array}{rl}
XK&\equiv&(\lambda x.x(xS(KK))K)K\\
&\rightarrow&K(KS(KK))K\\
&\rightarrow&K(S)K\\
&\rightarrow&S\\
\\
XK&\equiv&S
\end{array}$$