Лямбда-исчисление

Чистое λ-исчисление, термы которого, называемые также объектами («обами»), или λ-термами, построены исключительно из переменных применением аппликации и абстракции. Изначально наличие каких-либо констант не предполагается.

В основу λ-исчисления положены две фундаментальные операции:

• Аппликация (лат. applicatio — прикладывание, присоединение) означает применение или вызов функции по отношению к заданному значению. Её обычно обозначают ${\displaystyle f\ a}$ , где ${\displaystyle f}$  — функция, а ${\displaystyle a}$  — аргумент. Это соответствует общепринятой в математике записи ${\displaystyle f(a)}$ , которая тоже иногда используется, однако для λ-исчисления важно то, что ${\displaystyle f}$  трактуется как алгоритм, вычисляющий результат по заданному входному значению. В этом смысле аппликация ${\displaystyle f}$  к ${\displaystyle a}$  может рассматриваться двояко: как результат применения ${\displaystyle f}$  к ${\displaystyle a}$ , или же как процесс вычисления ${\displaystyle f\ a}$ . Последняя интерпретация аппликации связана с понятием β-редукции.

• Абстракция или λ-абстракция (лат. abstractio — отвлечение, отделение) в свою очередь строит функции по заданным выражениям. Именно, если ${\displaystyle t\equiv t[x]}$  — выражение, свободно^[en] содержащее ${\displaystyle x}$ , тогда запись ${\displaystyle \ \lambda x.t[x]}$  означает: ${\displaystyle \lambda }$  функция от аргумента ${\displaystyle x}$ , которая имеет вид ${\displaystyle t[x]}$ , обозначает функцию ${\displaystyle x\mapsto t[x]}$ . Таким образом, с помощью абстракции можно конструировать новые функции. Требование, чтобы ${\displaystyle x}$  свободно входило в ${\displaystyle t}$ , не очень существенно — достаточно предположить, что ${\displaystyle \lambda x.t\equiv t}$ , если это не так.

Основная форма эквивалентности, определяемая в лямбда-термах, это альфа-эквивалентность. Например, ${\displaystyle \lambda x.x}$  и ${\displaystyle \lambda y.y}$ : альфа-эквивалентные лямбда-термы и оба представляют одну и ту же функцию (функцию тождества). Термы ${\displaystyle x}$  и ${\displaystyle y}$  не альфа-эквивалентны, так как они не находятся в лямбда-абстракции.

Поскольку выражение ${\displaystyle \lambda x.2\cdot x+1}$  обозначает функцию, ставящую в соответствие каждому ${\displaystyle x}$  значение ${\displaystyle 2\cdot x+1}$ , то для вычисления выражения

в которое входят и аппликация и абстракция, необходимо выполнить подстановку числа 3 в терм ${\displaystyle 2\cdot x+1}$  вместо переменной ${\displaystyle x}$ . В результате получается ${\displaystyle 2\cdot 3+1=7}$ . Это соображение в общем виде записывается как

и носит название β-редукция. Выражение вида ${\displaystyle (\lambda x.t)\ a}$ , то есть применение абстракции к некому терму, называется редексом (redex). Несмотря на то, что β-редукция по сути является единственной «существенной» аксиомой ${\displaystyle \lambda }$ -исчисления, она приводит к весьма содержательной и сложной теории. Вместе с ней ${\displaystyle \lambda }$ -исчисление обладает свойством полноты по Тьюрингу и, следовательно, представляет собой простейший язык программирования.

${\displaystyle \eta }$ -преобразование выражает ту идею, что две функции являются идентичными тогда и только тогда, когда, будучи применёнными к любому аргументу, дают одинаковые результаты. ${\displaystyle \eta }$ -преобразование переводит друг в друга формулы ${\displaystyle \lambda x.f\ x}$  и ${\displaystyle f}$  (только если ${\displaystyle x}$  не имеет свободных вхождений в ${\displaystyle f}$ : иначе, свободная переменная ${\displaystyle x}$  после преобразования станет связанной внешней абстракцией или наоборот).

Функция двух переменных ${\displaystyle x}$  и ${\displaystyle y}$  ${\displaystyle f(x,y)=x+y}$  может быть рассмотрена как функция одной переменной ${\displaystyle x}$ , возвращающая функцию одной переменной ${\displaystyle y}$ , то есть как выражение ${\displaystyle \ \lambda x.\lambda y.x+y}$ . Такой приём работает точно так же для функций любой арности. Это показывает, что функции многих переменных могут быть выражены в ${\displaystyle \lambda }$ -исчислении и являются «синтаксическим сахаром». Описанный процесс превращения функций многих переменных в функцию одной переменной называется карринг (также: каррирование), в честь американского математика Хаскелла Карри, хотя первым его предложил М. Э. Шейнфинкель (1924).

Тот факт, что термы ${\displaystyle \lambda }$ -исчисления действуют как функции, применяемые к термам ${\displaystyle \lambda }$ -исчисления (то есть, возможно, к самим себе), приводит к сложностям построения адекватной семантики ${\displaystyle \lambda }$ -исчисления. Чтобы придать ${\displaystyle \lambda }$ -исчислению какой-либо смысл, необходимо получить множество ${\displaystyle D}$ , в которое вкладывалось бы его пространство функций ${\displaystyle D\to D}$ . В общем случае такого ${\displaystyle D}$  не существует по соображениям ограничений на мощности этих двух множеств, ${\displaystyle D}$  и функций из ${\displaystyle D}$  в ${\displaystyle D}$ : второе имеет бо́льшую мощность, чем первое.

Эту трудность в начале 1970-х годов преодолел Дана Скотт, построив понятие области ${\displaystyle D}$  (изначально на полных решётках^[1], в дальнейшем обобщив до полного частично упорядоченного множества со специальной топологией) и урезав ${\displaystyle D\to D}$  до непрерывных в этой топологии функций^[2]. На основе этих построений была создана денотационная семантика^[en] языков программирования, в частности, благодаря тому, что с помощью них можно придать точный смысл таким двум важным конструкциям языков программирования, как рекурсия и типы данных.

Рекурсия — это определение функции через себя; на первый взгляд, лямбда-исчисление не позволяет этого, но это впечатление обманчиво. Например, рассмотрим рекурсивную функцию, вычисляющую факториал:

f(n) = 1, if n = 0; else n × f(n - 1).

В лямбда-исчислении функция не может непосредственно ссылаться на себя. Тем не менее, функции может быть передан параметр, связанный с ней. Как правило, этот аргумент стоит на первом месте. Связав его с функцией, мы получаем новую, уже рекурсивную функцию. Для этого аргумент, ссылающийся на себя (здесь обозначен как ${\displaystyle r}$ ), обязательно должен быть передан в тело функции.

g := λr. λn.(1, if n = 0; else n × (r r (n-1)))

f := g g

Это решает специфичную проблему вычисления факториала, но решение в общем виде также возможно. Получив лямбда-терм, представляющий тело рекурсивной функции или цикл, передав себя в качестве первого аргумента, комбинатор неподвижной точки возвратит необходимую рекурсивную функцию или цикл. Функции не нуждаются в явной передаче себя каждый раз.

Существует несколько определений комбинаторов неподвижной точки. Самый простой из них:

Y = λg.(λx.g (x x)) (λx.g (x x))В лямбда-исчислении, ${\displaystyle \operatorname {Y\ g} }$  — неподвижная точка ${\displaystyle \operatorname {g} }$ ; продемонстрируем это:

Y g

(λh.(λx.h (x x)) (λx.h (x x))) g

(λx.g (x x)) (λx.g (x x))

g ((λx.g (x x)) (λx.g (x x)))

g (Y g).Теперь, чтобы определить факториал, как рекурсивную функцию, мы можем просто написать ${\displaystyle \operatorname {g\ (Y\ g)} n}$ , где ${\displaystyle n}$  — число, для которого вычисляется факториал. Пусть ${\displaystyle n=4}$ , получаем:

g (Y g) 4
   (λfn.(1, if n = 0; and n·(f(n-1)), if n>0)) (Y g) 4
   (λn.(1, if n = 0; and n·((Y g) (n-1)), if n>0)) 4
   1, if 4 = 0; and 4·(g(Y g) (4-1)), if 4>0
   4·(g(Y g) 3)
   4·(λn.(1, if n = 0; and n·((Y g) (n-1)), if n>0) 3)
   4·(1, if 3 = 0; and 3·(g(Y g) (3-1)), if 3>0)
   4·(3·(g(Y g) 2))
   4·(3·(λn.(1, if n = 0; and n·((Y g) (n-1)), if n>0) 2))
   4·(3·(1, if 2 = 0; and 2·(g(Y g) (2-1)), if 2>0))
   4·(3·(2·(g(Y g) 1)))
   4·(3·(2·(λn.(1, if n = 0; and n·((Y g) (n-1)), if n>0) 1)))
   4·(3·(2·(1, if 1 = 0; and 1·((Y g) (1-1)), if 1>0)))
   4·(3·(2·(1·((Y g) 0))))
   4·(3·(2·(1·((λn.(1, if n = 0; and n·((Y g) (n-1)), if n>0) 0))))
   4·(3·(2·(1·(1, if 0 = 0; and 0·((Y g) (0-1)), if 0>0))))
   4·(3·(2·(1·(1))))
   24

Каждое определение рекурсивной функции может быть представлено как неподвижная точка соответствующей функции, следовательно, используя ${\displaystyle \operatorname {Y} }$ , каждое рекурсивное определение может быть выражено как лямбда-выражение. В частности, мы можем определить вычитание, умножение, сравнение натуральных чисел рекурсивно.

В языках программирования под «${\displaystyle \lambda }$ -исчислением» зачастую понимается механизм «анонимных функций» — callback-функций, которые можно определить прямо в том месте, где они используются, и которые имеют доступ к локальным переменным текущей функции (замыкание).

• Аппликативные вычислительные системы
• Типизированное λ-исчисление
• Комбинаторная логика
• Функциональное программирование
• Анонимная функция

• Барендрегт X. Ламбда-исчисление. Его синтаксис и семантика: Пер. с англ. — М.: Мир, 1985. — 606 с.