前回のブログではチューリングの$\boldsymbol{Y}$コンビネータが不動点であることを示した。
他にも$\boldsymbol{Y}$コンビネータがあるので証明していく。
演習3.5(a)
$${\bf Y}_{Curry-Ros}\equiv\lambda x.VVただしV\equiv\lambda y.x(yy)$$
証明
${\bf Y}_{Curry-Ros}x\equiv(\lambda x.VV)x\ \triangleright(\lambda y.x(yy))(\lambda y.x(yy))\equiv VV$
さらに適用していくと、
$\equiv(\lambda y.x(yy))V\triangleright\ x(VV)\equiv x({\bf Y}_{Curry-Ros}x)$
従って
${\bf Y}x\equiv x({\bf Y}x) $が成り立つので、${\bf Y}_{Curry-Ros}$はコンビネータである。
別のYコンビネータ
Rosenbloom(1950)のThe Element of Mathmatical Logicのp.130-131, 3(e), 5(f)から
$$\Theta\equiv\lambda x||W|Bx|W|Bx$$
ここで"$|$"は適用$|ab\equiv (a)b$を表しているので、
$$\Theta\equiv\lambda x.(W(Bx))(W(Bx))$$
証明
$\Theta a\equiv(\lambda x.(W(Bx))(W(Bx)))a\
\triangleright\ (W(Ba))(W(Ba))$
$\Theta a\equiv\ (W(Ba))(W(Ba))$となる。
更に適用していくと、
$\triangleright\ (Ba)(W(Ba))(W(Ba))\
\triangleright\ a((W(Ba))(W(Ba)))
\equiv a(\Theta a)$
$\Theta a\equiv a(\Theta a)$が成り立つので、$\Theta$は${\bf Y}$コンビネータである。