β-редукция

Переливание из пустого в порожнее продолжается, и сейчас поговорим о β-редукции. Именно не о конверсии, так как экспансии тут быть не может: есть только редукция. Вообще вся операционная семантика λ-исчисления — одно правило переписывания, не более чем.

Вызов функции в любом языке — частный случай β-редукции.

(λx. M) N  \displaystyle (\lambda x.\,M)\,N \; →β  M[x:=N]\displaystyle \to_\beta\; M[x{:=}N]
(1.8)

Терм вида (λx. M) N(\lambda x.\,M)\,N называется редексом. Редукция может применяться к любому редексу в любом месте терма. Обозначение →β\to_\beta означает один шаг β-редукции, ↠β\twoheadrightarrow_\beta — ноль и более шагов, а =β=_\beta — эквивалентность, порождённая редукцией. Нормальная форма, или НФ, — это терм без редексов: вычислять больше нечего. Результатом работы программы как раз и должна быть нормальная форма.

Если запретить редукцию под знаком λ — не заглядывать в тело абстракции, — получается более слабое понятие: слабая нормальная форма. В ней стянуты все редексы, кроме спрятанных под λ. Скажем, λx. (λy. y) z\lambda x.\,(\lambda y.\,y)\,z уже в слабой нормальной форме, хотя обычной НФ λx. z\lambda x.\,z ещё не достиг. Именно до такой формы (точнее, слабой головной, WHNF) и вычисляют реальные языки: тело функции не трогают, пока её не позвали — подробнее в главе о стратегиях редукции.

Так в Haskell живут бесконечные структуры: их вычисляют до слабой головной формы, но не до конца.

nats = [1..]        -- бесконечный список 1 : 2 : 3 : …
-- уже в WHNF: виден внешний конструктор (:), хвост — невычисленный thunk;
-- полной НФ нет — чтобы её достичь, пришлось бы построить весь список
take 3 nats         -- [1,2,3]: берём только начало, и всё работает

Примеры β-редукций:

(λx. x) y\displaystyle (\lambda x.\,x)\,y →βy\displaystyle \to_\beta y
(λf. f (f z)) (λx. x)\displaystyle (\lambda f.\,f\,(f\,z))\,(\lambda x.\,x) →β(λx. x) ((λx. x) z)\displaystyle \to_\beta (\lambda x.\,x)\,((\lambda x.\,x)\,z) ↠βz\displaystyle \twoheadrightarrow_\beta z

Но, как всегда, есть нюансы, и главный нюанс заключается в том, что далеко не все термы редуцируются до нормальной формы. Выше на Haskell я уже дал пример бесконечного списка, но тут будет не о нём. Терм Ω\Omega редуцируется сам в себя — вычисление не завершается никогда:

Ω\displaystyle \Omega =(λx. x x) (λx. x x)\displaystyle = (\lambda x.\,x\,x)\,(\lambda x.\,x\,x) →βΩ\displaystyle \to_\beta \Omega →β⋯\displaystyle \to_\beta \cdots

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