Комбинатор Тьюринга

Комбинатор Карри решает задачу рекурсии, но не безупречно. Один из его изъянов мы уже отметили: рекурсию он лишь декларирует. Тождество YF\mathrm{Y}\,F=βF(YF){} =_\beta F\,(\mathrm{Y}\,F) держится на β-равенстве, а прямой редукции из YF\mathrm{Y}\,F в F(YF)F\,(\mathrm{Y}\,F) нет — чтобы замкнуть петлю, приходится шагать «назад» (конверсия). Попробуем это исправить: построить другой комбинатор неподвижной точки, который разворачивает рекурсию настоящей β-редукцией вперёд, а не провозглашает её равенством.

Добудем эту редукцию — ΘF\Theta\,FβF(ΘF){} \twoheadrightarrow_\beta F\,(\Theta\,F) — «протолкнув» саму функцию аргументом внутрь самоаппликации: возьмём GG=λxy.y(xxy){} = \lambda x\,y.\,y\,(x\,x\,y) и положим Θ\Theta=GG{} = G\,G. Тогда за два шага β-редукции:

ΘF\displaystyle \Theta\,F =(GG)F  \displaystyle {} = (G\,G)\,F \;β  (λy.y(GGy))F  \displaystyle {} \to_\beta\; (\lambda y.\,y\,(G\,G\,y))\,F \;β  F(GGF)\displaystyle {} \to_\beta\; F\,(G\,G\,F)=F(ΘF).\displaystyle {} = F\,(\Theta\,F).

Функция (в роли yy) здесь не теряется, а на каждом витке заново применяется к воссозданному ΘF\Theta\,F=GGF{} = G\,G\,F; поэтому равенство и превращается в честную редукцию. Разворачивая GG, получаем окончательный вид комбинатора Тьюринга:

Θ\displaystyle \Theta =(λxy.y(xxy))(λxy.y(xxy)),\displaystyle {} = (\lambda x\,y.\,y\,(x\,x\,y))\,(\lambda x\,y.\,y\,(x\,x\,y)),ΘF\displaystyle \Theta\,FβF(ΘF)\displaystyle {} \twoheadrightarrow_\beta F\,(\Theta\,F)
(1.26)

Посчитаем тот же факториал, что и в главе про комбинатор Карри (тот же шаблон FF, то же число 3\overline{3}), только теперь каждый виток рекурсии — настоящая β-редукция, а не β-равенство:

fac  3\displaystyle \mathbf{fac}\;\overline{3} =ΘF  3\displaystyle {} = \Theta\,F\;\overline{3}βF(ΘF)  3\displaystyle {} \twoheadrightarrow_\beta F\,(\Theta\,F)\;\overline{3}βmul  3  (ΘF  2)\displaystyle {} \twoheadrightarrow_\beta \mathbf{mul}\;\overline{3}\;(\Theta\,F\;\overline{2})βmul  3  (mul  2  (mul  1  (ΘF  0)))\displaystyle {} \twoheadrightarrow_\beta \mathbf{mul}\;\overline{3}\;(\mathbf{mul}\;\overline{2}\;(\mathbf{mul}\;\overline{1}\;(\Theta\,F\;\overline{0})))βmul  3  (mul  2  (mul  1  1))\displaystyle {} \twoheadrightarrow_\beta \mathbf{mul}\;\overline{3}\;(\mathbf{mul}\;\overline{2}\;(\mathbf{mul}\;\overline{1}\;\overline{1}))=6\displaystyle {} = \overline{6}

Оба дают 6\overline{6}; разница лишь в статусе шага развёртки — равенство у Карри против редукции у Тьюринга.

На практике комбинатор Тьюринга почти не встречается — его роль теоретическая: он показывает, что рекурсия достижима честной редукцией, без шага «назад», и в этом качестве он стандартный спутник Y в учебниках.

Но и Карри, и Тьюринг рассчитаны на нормальный порядок (call-by-name). При строгом, энергичном порядке (call-by-value) оба расходятся: аргумент FF — то есть сам YF\mathrm{Y}\,F или ΘF\Theta\,F — вычисляется заранее и разворачивается бесконечно, так и не дойдя до полезной работы. Эту проблему решает следующий комбинатор — Z.