( ?xz. x) y
После подстановки будет совсем другим. Но мы всего лишь изменили обозначение локальной перемен-
ной y на z. И смысл изменился, для того чтобы исключить такие случаи пользуются переименованием пе-
ременных или ?-преобразованием. Для корректной работы функций необходимо следить за тем, чтобы все
переменные, которые были свободными в аргументе, остались свободными и после подстановки.
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)
На каждом шаге редукции мы будем вновь и вновь возвращаться к исходному терму.
Стратегии редукции
В главе о ленивых вычислениях нам встретились две стратегии вычисления выражений. Это вычисление
по имени и вычисление по значению. Также там мы узнали о том, что ленивые вычисления это улучшенная
версия вычисления по имени, в которой аргументы функций вычисляются не более одного раза.
Эти стратегии вычисления пришли из лямбда-исчисления. Если нам нужно избавиться от всех редексов
в выражении, то с какого редекса лучше начать? В вычислении по значению ( аппликативная стратегия) мы
начинаем с самого левого редекса, который не содержит других редексов, то есть с самого маленького подвы-
ражения. А в вычислении по имени ( нормальная стратегия) мы начинаем с самого левого внешнего редекса.
Левый редекс означает, что в записи выражения он находится ближе всех к началу выражения.
Теорема (Карри) Если у терма есть нормальная форма, то последовательное сокращение самого левого
внешнего редекса приводит к ней.
Эта теорема говорит о том, что стратегия вычисления по имени может вычислить все термы, которые
имеют нормальную форму. В том, что вычисление по значению может не справиться с некоторыми такими
термами мы можем на следующем примере:
( ?xy. x) z (( ?x. xx)( ?x. xx))
Этот терм имеет нормальную форму z несмотря на то, что мы передаём вторым аргументом в констант-
ную функцию терм, у которого нет нормальной формы. Алгоритм вычисления по значению зависнет при
вычислении второго аргумента. В то время как алгоритм вычисления по имени начнёт с самого внешнего
терма и там определит, что второй аргумент не нужен.
Ещё один важный результат в лямбда-исчислении был сформулирован в следующей теореме:
Лямбда исчисление без типов | 219
Теорема (Чёрча-Россера) Если терм X редуцируется к термам Y 1 и Y 2, то существует терм L, к которому
редуцируются и терм Y 1 и терм Y 2.
Эта теорема говорит о том, что у терма может быть только одна нормальная форма. Поскольку если бы
их было две, то существовал третий терм, к которому можно было бы редуцировать эти нормальные формы.
Но по определению нормальной формы, мы не можем её редуцировать. Из этого следует, что нормальные
формы должны совпадать.
Теорема Чёрча-Россера указывает на способ сравнения термов. Для того чтобы понять равны термы или
нет, необходимо привести их к нормальной форме и сравнить. Если термы совпадают в нормальной форме,
значит они равны.
Рекурсия. Комбинатор неподвижной точки
В лямбда-исчислении все функции являются безымянными. Это означает, что мы не можем в теле функ-
ции вызвать саму функции, ведь мы не можем на неё сослаться, кажется, что у нас нет возможности строить
рекурсивные функции. Однако это не так. Нам на помощь придёт комбинатор неподвижной точки. По опре-
делению комбинатор неподвижной точки решает задачу: для терма F найти терм X такой, что
F X = X
Существует много комбинаторов неподвижной точки. Рассмотрим Y -комбинатор:
Y = ?f. ( ?x. f ( xx))( ?x. f ( xx))
Убедимся в том, что для любого терма F , выполнено тождество: F ( Y F ) = Y F :
Y F = ( ?x. F ( xx))( ?x. F ( xx)) = F ( ?x. F ( xx))( ?x. F ( xx)) = F ( Y F ) Так с помощью Y -комбинатора можно составлять рекурсивные функции.