コンビネータ論理を学んでいて、$B=[f,g,x].f(g(x))$がどうなるか、しりたかったので、やってみた。
参考にしているのは下記の書籍：
Lambda-Calculus and Combinators:An Introduction PDF
定義 2.18（抽象化）
(a)$\ [x].M\equiv KM$ if $x\in FV(M)$
(b)$\ [x].x\equiv I$
(c)$\ [x].Ux\equiv U$ if $ x\notin FV(U)$
(f)$\ [x].UV\equiv S([x].U)([x].V)$もし(a)も(c)も適用できない場合。
問題
$B=[f,g,x].f(g(x)$について計算してみる。
$[f,g,x].f(g(x)\equiv[f].([g].([x].f(g(x))))$なので、
一番内側の式をxについて抽象化。
$[x].f(g(x)\equiv S([x].f)([x].g(x))$
$\equiv S(Kf)(g)
\equiv
S(Kf)g$
となる。
検証のために$x$を適用してみると
$S(Kf)g x$
$\equiv(Kf)x(gx)$
$\equiv f(gx)\equiv f(g(x))$
$$[x].f(g(x)\rightarrow S(Kf)g$$が示された。
更に[g]で抽象化
$[g].S(Kf)g$
$\equiv S([g].S(Kf))([g].g)$
$\equiv S(K(S(Kf)))I$
検証のために$g$を右から適用してみる。
$S(K(S(Kf)))I g$
$\equiv (K(S(Kf)))g (Ig)$
$\equiv S(Kf) g$
$$S(Kf)g\rightarrow S(K(S(Kf)))I$$が示された。
最後に[f]で抽象化
$[f].S(K(S(Kf)))I$
$S([f].S(K(S(Kf)))) ([f].I)$
$S\{S([f].S)([f].K(S(Kf)))\} (KI)$
$S\{S(KS)(S([f].K)([f].S(Kf)))\} (KI)$
$S\{S(KS)(S(KK)(S([f].S)([f].Kf)))\} (KI)$
$S\{S(KS)(S(KK)(S(KS)K))\} (KI)$
検証のために$f$を右から適用すると
$S(S(KS)(S(KK)(S(KS)K))) (KI) f$
$\rightarrow S(KS)(S(KK)(S(KS)K))f (KIf)$
$\rightarrow (KS)f (S(KK)(S(KS)K)f) I$
$\rightarrow S ((KK)f (S(KS)Kf)) I$
$\rightarrow S (K ((KS)f(Kf))) I$
$\rightarrow S (K (S (Kf))) I$
$$[f].S(K(S(Kf)))I\rightarrow S(S(KS)(S(KK)(S(KS)K))) (KI)$$
最終的に
$$[f,g,x].f(g(x))\rightarrow S(S(KS)(S(KK)(S(KS)K))) (KI)$$