数学の大学教授から薦められて、論文を読んでいる。
the Lambda Calculus is Algebra
Peter Selinger (2002)
だが、記号の意味や定義の意味が分からないことだらけで、ずーーとたどっていくとある一つのコンビネータで基本コンビネータ$S,K$を表せるという定義にたどり着いた。それは、$$X\equiv\ \langle K,S,K\rangle$$
$X$の組み合わせのみで
$$XXX\rightarrow K$$
$$X(XX)\rightarrow S$$
となり、$X$のみで$S,K$を表せることを示す。
ここで、$K,S$の定義は以下の通り：
$$K\equiv\lambda xy.x$$
$$S\equiv\lambda xyz.xz(yz)$$
以前書いたブログでもイオタ・コンビネータがK,Sを表せることを示した。ちなみに、イオタ・コンビネータは以下の定義：
$$\iota\equiv\ \lambda f.fSK$$
<,...,>とは何？
まずはこの括弧$\langle,\dots,\rangle$について説明する。
これはタプルを表し、一般に
$$\langle M_1,\cdots M_n\rangle\equiv\lambda xM_1,\cdots,M_n$$となる。二項の場合はペア$$[M,N]\equiv\lambda x.x MN$$となる。
つまり$X$は、$$X\equiv\langle K,S,K\rangle\equiv\lambda f.fKSK$$となる。
(i) XXX=K
まずは$XX$を計算する。
$XX\equiv(\lambda f.fKSK)X
\rightarrow XKSK
\equiv(\lambda f.fKSK)KSK$
$\rightarrow (KKSK)SK\rightarrow(KK)SK
\rightarrow KK$
$XXX\equiv(XX)X\equiv(KK)X\rightarrow K$
$$XXX\rightarrow K$$
(ii) X(XX)=S
$X(XX)\equiv X(KK)
\equiv(\lambda f.fKSK)(KK)
\rightarrow(KK)KSK$
$\rightarrow KSK
\rightarrow S$
$$X(XX)\rightarrow S$$
おまけ X(X(XX))?
ちなみに$X(X(XX))$はどうなるか、計算してみた。
$X(X(XX))\equiv X(S)\equiv(\lambda f.fKSK)S
\rightarrow SKSK$
$\rightarrow KK(SK)
\rightarrow K$
$$X(X(XX))\rightarrow K$$