コンビネータ論理を学んでいて、練習問題で結構難しかったので、メモ。
参考にしているのは下記の書籍：

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)も適用できない場合。

練習問題 2.26*

$[x,y,z].y(xz)$
上式は以下のようになるので
$\equiv [x].([y].([z].y(xz)))$

一番内側の式は[z]について抽象化。

$[z].y(xz)\equiv S([z].y)([z].xz)$
$\equiv S(Ky)(S([z].x)([z].z)$
$\equiv S(Ky)(S(Kx)I)$
となる。

検証のために$z$を適用してみると
$S(Ky)(S(Kx)I)z$
$\equiv(Ky)z(S(Kx)Iz)$
$\equiv y((Kx)z(Iz))$ by $(Ky)z\equiv z$ and $S(Kx)Iz\equiv (Kx)z(Iz)$
$\equiv y(xz)$ by $(x)z\equiv x$ and $Iz\equiv z$

$S(Ky)(S(Kx)I)z\rightarrow y(xz)$が示された。

更に[y]で抽象化

$[y].([z].y(xz))$
$\equiv [y].(S(Ky)(S(Kx)I))$
$\equiv S\underbrace{([y].S(Ky))}\underbrace{([y].S(Kx)I)}$
二項目は
$[y].S(Ky)$
$\equiv S([y].S)([y].Ky)$ by (f)
$\equiv S(KS)K$
三項目は
$[y].S(Kx)I$
$\equiv K(S(Kx)I)$
合わせて、
$[y].(S(Ky)(S(Kx)I))\equiv S(S(KS)K)(K(S(Kx)I))$
元の式になっているので、検証できた。

検証のためにyを右から適用してみる。
$S(S(KS)K)(K(S(Kx)I))$
$\equiv S(KS)K)y[K(S(Kx)I)y]$
$\equiv (KS)y(Ky)[S(Kx)I]$
$\equiv S(Ky)[S(Kx)I]$

最後に[x]で抽象化

$[x].S(S(KS)K)(K(S(Kx)I))y$
$\equiv S\underbrace{([x].S(S(KS)K))}\underbrace{([x].K(S(Kx)I))}$ by (f)
二項目は、
$[x].S(S(KS)K)$
$\equiv K(S(S(KS)K))$
三項目は、
$[x].K(S(Kx)I)$
$\equiv S([x].K)([x].S(Kx)I)$
$\equiv S(KK)(S\underbrace{([x].K)}\underbrace{([x].S(Kx)I)})$
ここで
$(S([x].K)\equiv KK$
$([x].S(Kx)I)$
$\equiv S([x].S(Kx))([x].I)$
$\equiv S(S([x].S)([x].Kx))(KI)$
$\equiv S(S(KS)K)(KI)$
従って三項目
$[x].K(S(Kx)I)$
$\equiv S(KK)(S(KK)(S(S(KS)K)(KI)))$

全体の式
$[x].S(S(KS)K)(K(S(Kx)I))$
$\equiv S(K(S(S(KS)K)))(S(KK)(S(KK)(S(S(KS)K)(KI))))$

検証のためにxを右から適用すると
$S\underbrace{(K(S(S(KS)K)))}
\underbrace{(S(KK)(S(KK)(S(S(KS)K)(KI))))}x$
$(K(S(S(KS)K)))x[(S(KK)(S(KK)(S(S(KS)K)(KI)))x]$
最終的に
$\equiv S(S(KS)K)(K(S(Kx)I))$となるので、検証できた。

変数の順序が入れ替わっているだけなのに、こんな複雑な式になるのは不思議だ。