Стратегии редукции

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

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

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

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

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

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

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

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

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

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

Разделение необходимо: без него была бы возможна аппликация, у которой слева стоит абстракция, — а такой терм уже не нормальная форма, это редекс. Примеры $\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$ — произвольный терм, он подставляется в тело невычисленным:

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

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

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

Первое правило редуцирует левую часть аппликации, пока та остаётся не-абстракцией; второе переходит к аргументу, лишь когда слева уже стоит $\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).