термами мы можем на следующем примере:
( λ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
говорит о том, что мы дали обозначение N терму M. Этой операции нет в лямбда-исчислении, но мы будем
пользоваться ею для удобства.
Логические значения
Суть логических значений заключается в операторе If, с помощью которого мы можем организовывать
ветвление алгоритма. Есть два терма T rue и F alse, которые для любых термов a и b, обладают свойствами:
If T rue a b
=
a
If F alse a b