Z-комбинатор — λ-исчисление

Осталась проблема, которой одинаково подвержены и комбинатор Карри, и комбинатор Тьюринга: в энергичном порядке (call-by-value) оба зацикливаются. Рекурсивный аргумент — сам $\mathrm{Y}\,F$ или $\Theta\,F$ — среда раскручивает заранее, ещё до вызова функции, так и не дойдя до полезной работы. Исправить это можно, отложив рекурсивный вызов — превратив его в значение, которое раскроется лишь тогда, когда действительно понадобится.

Идея до боли простая: над самоаппликацией надо навесить обёртку-функцию. Технически это η-развёртка $x\,x \to \lambda v.\,x\,x\,v$ . Завёрнутый в $\lambda$ вызов — уже значение и разворачивается только при реальном обращении. Так из комбинатора Карри (1.24) получается Z-комбинатор — та же конструкция, только каждое $x\,x$ заменено на $\lambda v.\,x\,x\,v$ :

Z = \lambda f.\,(\lambda x.\,f\,(\lambda v.\,x\,x\,v))\,(\lambda x.\,f\,(\lambda v.\,x\,x\,v))

(1.27)

Проследим первый разворот. Обозначим $W = \lambda x.\,F\,(\lambda v.\,x\,x\,v)$ ; тогда за два шага β-редукции:

Z\,F \;\to_\beta\; W\,W \;\to_\beta\; F\,(\lambda v.\,W\,W\,v) \;=\; F\,(\lambda v.\,Z\,F\,v).

Последнее равенство сворачивает $W\,W$ обратно в $Z\,F$ . Главное — рекурсивный вызов вышел наружу завёрнутым в $\lambda v$ : под $\lambda$ он остаётся значением и разворачивается лишь при реальном применении к аргументу (тогда как $\mathrm{Y}\,F$ и $\Theta\,F$ в энергичном порядке разворачиваются сразу).

Тот же факториал, что и в разделах про Карри и Тьюринга (тот же шаблон $F$ , то же число $\overline{3}$ ), считается настоящими β-редукциями, а завёрнутый вызов раскрывается ровно при переходе к следующему числу:

\begin{aligned}\mathbf{fac}\;\overline{3} = Z\,F\;\overline{3} &\twoheadrightarrow_\beta F\,(\lambda v.\,Z\,F\,v)\;\overline{3} \twoheadrightarrow_\beta \mathbf{mul}\;\overline{3}\;((\lambda v.\,Z\,F\,v)\;\overline{2}) \twoheadrightarrow_\beta \mathbf{mul}\;\overline{3}\;(Z\,F\;\overline{2}) \\ &\twoheadrightarrow_\beta \mathbf{mul}\;\overline{3}\;(\mathbf{mul}\;\overline{2}\;(\mathbf{mul}\;\overline{1}\;(Z\,F\;\overline{0}))) \\ &\twoheadrightarrow_\beta \mathbf{mul}\;\overline{3}\;(\mathbf{mul}\;\overline{2}\;(\mathbf{mul}\;\overline{1}\;\overline{1})) = \overline{6}\end{aligned}

Поэтому под энергичным порядком (call-by-value) он не разворачивается заранее и не зацикливается — рекурсивный вызов срабатывает точно в нужный момент.

Ни Y, ни Θ, ни Z не типизируются в простом типизированном λ-исчислении: самоаппликация $x\,x$ потребовала бы рекурсивного типа.

В Haskell такой рекурсивный тип и заводят — оборачивая самоаппликацию в newtype; на нём хорошо видно, что Z не опирается на лень. Обычный $\mathtt{fix}$ держится на ленивом узле $\mathtt{let\;x = f\;x}$ , а Z строит рекурсию самоприменением и прячет рекурсивный вызов под $\lambda v$ — под значение. Заставим вычисление быть строгим (аргумент форсится перед применением функции, как при call-by-value): наивный Y зацикливается, а Z спокойно считает факториал:

newtype Rec a = Rec { unRec :: Rec a -> a }

-- $! форсит аргумент до применения f — это и есть энергичный порядок (call-by-value)

-- наивный Y: рекурсивный вызов (unRec x x) не значение, форсится заранее => зацикливается
yStrict :: (a -> a) -> a
yStrict f = w (Rec w) where w x = f $! unRec x x

-- Z: вызов завёрнут в (\v -> ...), это уже значение — $! его не разворачивает
zStrict :: ((b -> c) -> b -> c) -> b -> c
zStrict f = w (Rec w) where w x = f $! \v -> unRec x x v

fac :: (Int -> Int) -> Int -> Int
fac rec n = if n == 0 then 1 else n * rec (n - 1)

-- yStrict fac 5  =>  зацикливается
-- zStrict fac 5  =>  120   -- Z досчитал без всякой ленивости