コンビネータ論理を学んでいる。参考にしているのは下記の書籍:
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)も適用できない場合。
[f,g,x].fgx
$[f,g,x]$について解いていこう。
上式は以下のようになるので
$[f,g,x].fgx\equiv [f].([g].([x].fgx))$
[x]について抽象化。
$[x].fgx\equiv[x].(fg)x
\equiv fg$
となる。
更に[g]で抽象化
$[g].([x].fgx)\equiv [g].fg\equiv f$
最後に[f]で抽象化
$[f].([g].([x].fgx))
\equiv[f].f
\equiv I$
最終的に
$([f,g,x].fgx)fgx\equiv Ifgx\equiv fgx$
$$[f,g,x].fgx\equiv I$$
何かあたりまえの結果。