Учебник по Haskell

менной с именем 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 -комбинатора можно составлять рекурсивные функции.

Кодирование структур данных

Вы наверное заметили, что пока мы составляли лишь обобщённые функции. Эти функции комбинируют

другие функции, они не выполняют никаких действий над элементами. Что если нам захочется вычислять

логические значения или воспользоваться числами?

Оказывается, что логические значения, числа, пары, списки и другие конструкции могут быть закодиро-

ваны с помощью термов лямбда-исчисления. Тезис Чёрча утверждает, что с помощью лямбда-терма можно

представить любую вычислимую числовую функцию. В 1936 году Чёрч с помощью лямбда-исчисления дока-

зал существование неразрешимых проблем в теории чисел. Из этого следовала неразрешимость арифметики

и неразрешимость исчисления логики предикатов первого порядка. Система аксиом называется разрешимой

в том случае, если существует такой алгоритм, который позволяет по виду формулы определить следует ли

она из заданных аксиом или нет.

Посмотрим как с помощью термов кодируются структуры данных. Далее для сокращения записи мы бу-

дем считать, что в лямбда исчислении можно определять синонимы с помощью знака равно. Запись N = M