コンビネータ論理：抽象化1 Exercise 2.26

この記事の練習問題。
https://qiita.com/Trubetzkoy/items/c55fc03a235e72022643

Exercise 2.26

$[x,y,z].xzy$
$\equiv [x].([y].([z].(xz)y)))$

(i) zで抽象化

$[z].(xz)y$
$\equiv S([z].xz)([z].y)$
$\equiv S(x)(Ky)\equiv Sx(Ky)$
検証する。
$Sx(Ky)z\rightarrow xz((Ky)z)\rightarrow xz(y)\rightarrow xzy$

(ii) yで抽象化

$[y].Sx(Ky)$
$\equiv [y].(Sx)(Ky)$
$\equiv S([y].Sx)([y].Ky)$
$\equiv S(K(Sx))K$
検証する。
$S(K(Sx))Ky$
$\rightarrow S(K(Sx))y(Ky)$
$\rightarrow (K(Sx))y(Ky)$
$\rightarrow Sx(Ky)$ Q.E.D.

(iii)xで抽象化

$[x].S(K(Sx))K$
$\equiv[x].(S(K(Sx)))K$
$\equiv S([x].S(K(Sx)))([x].K)$
$\equiv S(S([x].S)([x].K(Sx)))(KK)$
$\equiv S(S(KS)(S([x].K)([x].Sx)))(KK)$
$\equiv S(S(KS)(S(KK)S))(KK)$
となる。

右から$x$を適用して検証する。
$S(S(KS)(S(KK)S))(KK)x$
$\equiv S\underbrace{(S(KS)(S(KK)S))}\underbrace{(KK)}x$
$\rightarrow S(KS)(S(KK)S)x\{(KK)x\}$
$\rightarrow S\underbrace{(KS)}\underbrace{(S(KK)S)}x\{(KK)x\}$
$\rightarrow(KS)x\{(S(KK)S)x\}\{(KK)x\}$
$\rightarrow S\{(KK)x(Sx)\}\{K\}$
$\rightarrow S\{K(Sx)\}K$
$\rightarrow S(K(Sx))K$ Q.E.D.

つまり
$[x,y,z].xzy$
$\equiv [x].([y].([z].(xz)y)))$
$\equiv S(S(KS)(S(KK)S))(KK)$
となる。式は$S$と$K$のみで表現される。

第1変数$x$はそのままで、第2、第3変数の$y,z$が$zy$と順序が交替するからなのか？コンビネータにはどんな操作が隠れているのだろうか？
たまたま$I$コンビネータが出てこないだけだろうか？$I=SKK$なので$I$が現れるかどうかは重要ではないが。