ременных или α-преобразованием. Для корректной работы функций необходимо следить за тем, чтобы все
переменные, которые были свободными в аргументе, остались свободными и после подстановки.
218 | Глава 14: Лямбда-исчисление
β-редукция
Процесс подстановки аргументов в функции называется β-редукцией. В редексе ( λx. M) N вместо свобод-
ных вхождений x в M мы подставляем N. Посмотрим на правила подстановки:
x[ x = N ]
⇒ N
y[ x = N ]
⇒ y
( P Q)[ x = N ]
⇒ ( P [ x = N] Q[ x = N])
( λy. P )[ x = N ] ⇒ ( λy. P [ x = N ]) ,
y /
∈ F V ( N)
( λx. P )[ x = N ] ⇒ ( λx. P )
Первые два правила определяют подстановку вместо переменных. Если переменная совпадает с той, на
место которой мы подставляем терм N, то мы возвращаем терм N, иначе мы возвращаем переменную:
x[ x = N ] ⇒ N
y[ x = N ] ⇒ y
Подстановка применения термов равна применению термов, в которых произведена подстановка:
( P Q)[ x = N ] ⇒ ( P [ x = N ] Q[ x = N ])
При подстановке в лямбда-функции необходимо учитывать связность переменных. Если переменная ар-
гумента отличается от той переменной на место которой происходит подстановка, то мы заменяем в теле
функции все вхождения этой переменной на N:
( λy. P )[ x = N ] ⇒ ( λy. P [ x = N ]) ,
y /
∈ F V ( N)
Условие y / ∈ F V ( N) означает, что необходимо следить за тем, чтобы в N не оказалось свободной пере-
менной с именем y, иначе после подстановки она окажется связанной. Если такая переменная в N всё-таки
окажется мы проведём α-преобразование в терме $ λy. M и заменим y на какую-нибудь другую переменную.
В последнем правиле мы ничего не меняем, поскольку переменная x оказывается связанной. А мы про-
водим подстановку только вместо свободных переменных:
( λx. P )[ x = N ] ⇒ ( λx. P )
Отметим, что не любой терм можно вычислить, например у такого терма нет нормальной формы:
( λx. xx)( λx. xx)
На каждом шаге редукции мы будем вновь и вновь возвращаться к исходному терму.
Стратегии редукции
В главе о ленивых вычислениях нам встретились две стратегии вычисления выражений. Это вычисление
по имени и вычисление по значению. Также там мы узнали о том, что ленивые вычисления это улучшенная
версия вычисления по имени, в которой аргументы функций вычисляются не более одного раза.
Эти стратегии вычисления пришли из лямбда-исчисления. Если нам нужно избавиться от всех редексов
в выражении, то с какого редекса лучше начать? В вычислении по значению ( аппликативная стратегия) мы
начинаем с самого левого редекса, который не содержит других редексов, то есть с самого маленького подвы-
ражения. А в вычислении по имени ( нормальная стратегия) мы начинаем с самого левого внешнего редекса.
Левый редекс означает, что в записи выражения он находится ближе всех к началу выражения.
Теорема (Карри) Если у терма есть нормальная форма, то последовательное сокращение самого левого
внешнего редекса приводит к ней.
Эта теорема говорит о том, что стратегия вычисления по имени может вычислить все термы, которые