Стратегии редукции — λ-исчисление

Правило, по которому из всех редексов терма выбирается очередной, называется стратегией редукции. Разберёмся, где возникает выбор. Терм бывает трёх видов:

переменная $x$ — редуцировать нечего;
абстракция $\lambda x.M$ — выбора нет: редуцируем тело $M$ ;
аппликация $M\,N$ — редексы могут быть и в левой части, и в правой; выбор между ними и делает стратегия.

Раскроем аппликацию: её левая часть может снова быть аппликацией, левая часть той — тоже, и так далее. Спустившись по левым ветвям до первой не-аппликации — до головы терма, — получим один из двух видов:

\begin{aligned}&(\dots((x\,N_1)\,N_2)\dots N_k), \\&(\dots(((\lambda x.M)\,N_1)\,N_2)\dots N_k).\end{aligned}

В первом виде голова — переменная $x$ : слева стягивать нечего, редексы могут прятаться только в аргументах $N_i$ . Во втором голова — абстракция, и $(\lambda x.M)\,N_1$ — редекс; вот и развилка: стянуть его сразу или сначала вычислить аргумент. Этот выбор и различает две классические стратегии.

Нормальная стратегия стягивает самый левый внешний редекс — в нашей записи это $(\lambda x.M)\,N_1$ : аргументы подставляются в тело невычисленными. Аппликативная стратегия поступает наоборот: сперва доводит аргумент редекса до нормальной формы и лишь потом стягивает сам редекс.

Терм удобно изображать деревом. Например, для $((\lambda x.M)\,N_1)\,N_2$ оно устроено так (рис. 1.4): узлы $@$ — аппликации, узел $\lambda x$ — абстракция. Самый левый внешний редекс на дереве ищется спуском от корня по левым рёбрам: это первый $@$ , у которого левый ребёнок — абстракция.

Дерево терма ((λx.M) N₁) N₂: два узла-аппликации @ и узел-абстракция λx; нижний @ — самый левый внешний редекс — **Рис. 1.4.** Дерево терма $((\lambda x.M)\,N_1)\,N_2$ : узлы $@$ — аппликации, узел $\lambda x$ — абстракция; красный $@$ — самый левый внешний редекс $(\lambda x.M)\,N_1$ .

Этот же спуск позволяет ввести важное понятие — головную нормальную форму. Поясним его на двух примерах:

\begin{aligned}&\lambda x_1\dots x_n.\,y\,N_1\dots N_k, \quad n,k \ge 0,\\&\lambda x_1\dots x_n.\,(\lambda z.M)\,N_1\dots N_k, \quad n\ge 0,\ k>0.\end{aligned}

Первый терм — головная нормальная форма: спуск по левым ветвям упирается в переменную $y$ , она называется головной переменной. Голова такого терма уже не изменится, редексы могут прятаться лишь в аргументах $N_i$ . Второй терм головной нормальной формой не является: его голова — редекс $(\lambda z.M)\,N_1$ , он называется головным редексом.

Сформулируем обе стратегии точно — правилами операционной семантики. Мало нам понятий — надо ещё: понадобятся три синтаксические категории. Первая — не-абстракция $\mathit{NA}$ :

\mathit{NA} \mathrel{\text{::=}} x \mid M\,N.

Тут, кажется, всё понятно: это любой терм, только не абстракция. $M$ и $N$ — произвольные термы, так что не-абстракция вполне может быть редексом — например, $(\lambda y.y)\,z$ . Две другие категории описывают готовые результаты: нормальные формы $\mathit{NF}$ и их подкласс — нормальные формы-не-абстракции $\mathit{NANF}$ :

\begin{aligned}\mathit{NF} &\mathrel{\text{::=}} \lambda x.\mathit{NF} \mid \mathit{NANF},\\\mathit{NANF} &\mathrel{\text{::=}} x \mid \mathit{NANF}\ \mathit{NF}.\end{aligned}

Разделение необходимо: без него была бы возможна аппликация, у которой слева стоит абстракция, — а такой терм уже не нормальная форма, это редекс. Примеры $\mathit{NF}$ : $\lambda x.\,x$ , $\lambda f.\lambda x.\,f\,x$ . Примеры $\mathit{NANF}$ : $x$ , $f\,x$ , $x\,(\lambda y.y)\,z$ — причём каждый из них одновременно и $\mathit{NF}$ .

Теперь наконец-то стратегии. В основе каждой лежит своё правило стягивания редекса. Нормальная стратегия использует обычную $\beta$ -редукцию: редекс стягивается сразу, аргумент $N$ — произвольный терм, он подставляется в тело невычисленным:

\displaystyle (\lambda x.M)\,N

\displaystyle \to M[x\!:=\!N]

(1.33)

Аппликативная стратегия стягивает редекс иначе — лишь когда аргумент уже вычислен, то есть доведён до нормальной формы — слева от стрелки стоит $\mathit{NF}$ , и пока аргумент не таков, стягивание запрещено:

\displaystyle (\lambda x.M)\,\mathit{NF}

\displaystyle \to M[x\!:=\!\mathit{NF}]

(1.34)

Так как мы не можем стянуть редекс, пока аргумент не в нормальной форме, в аппликативной стратегии есть правило для аргумента:

\dfrac{N \to N'}{(\lambda x.M)\,N \to (\lambda x.M)\,N'}

(1.35)

Оставшиеся правила — общие для нормальной стратегии и аппликативной:

\dfrac{\mathit{NA} \to \mathit{NA}'}{\mathit{NA}\,N \to \mathit{NA}'\,N}, \quad \dfrac{N \to N'}{\mathit{NANF}\,N \to \mathit{NANF}\,N'}, \quad \dfrac{M \to M'}{\lambda x.M \to \lambda x.M'}

(1.36)

Первое правило редуцирует левую часть аппликации, пока та остаётся не-абстракцией; второе переходит к аргументу, лишь когда слева уже стоит $\mathit{NANF}$ ; третье заводит редукцию в тело абстракции. Категории $\mathit{NA}$ и $\mathit{NANF}$ в посылках как раз и гарантируют порядок «самый левый внешний»: пока слева есть что стягивать, вправо не смотрим.

Выбор самого левого внешнего редекса неслучаен: теорема о нормализации (Карри) гарантирует, что если у терма есть нормальная форма, то последовательное стягивание именно такого редекса её достигнет. За это нормальную стратегию называют полной.

Полнота не бесплатна: аргумент, подставленный в несколько мест, приходится пересчитывать. Для «большого» $N$ : $(\lambda x.\,F\,x\,(G\,x)\,x)\,N$ $\to_\beta F\,N\,(G\,N)\,N$ — здесь $N$ придётся редуцировать трижды — по разу на копию. Аппликативная стратегия вычислит $N$ ровно один раз, но платит за это полнотой. Пусть $\mathrm{K}$ $\equiv \lambda x y.x$ , $\mathrm{I}$ $\equiv \lambda x.x$ , а $\Omega$ $\equiv (\lambda x.x\,x)\,(\lambda x.x\,x)$ — терм без нормальной формы. Нормальная стратегия вычисляет $\mathrm{K}\,\mathrm{I}\,\Omega$ $\twoheadrightarrow_\beta \mathrm{I}$ , отбросив $\Omega$ не глядя; аппликативная же сперва берётся за аргумент $\Omega$ — и зацикливается.

В языках программирования обе стратегии живут под другими именами. Аппликативная — это вызов по значению (call-by-value) строгих языков вроде Си: сначала аргументы, потом применение. Нормальная — основа ленивых вроде Haskell: вызов по имени (call-by-name).