コンビネータ論理を学んでいて、xyの順序をyxに変える操作はどうなるのか気になってやってみた。
$$[x,y].yx$$はどうなるか？
[x,y].yxについて
$[x,y].yx$
$\equiv[x].([y].yx)$
$\equiv[x].S([y].y)([y].x)$ 定義2.28(f)より$y$で抽象化
$\equiv[x].SI(Kx)$
$\equiv[x].(SI)(Kx)$
$\equiv S([x].SI)([x].Kx)$
$\equiv S(K(SI))K$
検証してみる：
$S(K(SI))Kxy$
$\equiv\{S\underbrace{(K(SI))}Kx\}y$
$\rightarrow (K(SI))x(Kx)y$
$\rightarrow SI(Kx)y$
$\rightarrow Iy((Kx)y)$
$\rightarrow yx$
検証できたので、$$[x,y].yx\equiv S(K(SI))K$$となった。
[x,y]=xyについて
では、順序変更しない式はどうなるのか、気になったのでやってみた。
$[x,y].xy$
$\equiv[x].([y].xy)\equiv[x].(x)\equiv I$
$Ixy\rightarrow(Ix)y\rightarrow xy$なので、
$$[x,y].xy\equiv I$$となる。
抽象化(abstraction)については前の記事を参照してね。