Ля́мбда-исчисле́ние (λ-исчисление) это формальная система, разработанная американским математиком Алонзо Чёрчем для формализации и анализа понятия вычислимости.
Чистое λ-исчисление Чистое λ-исчисление, термы которого, называемые также объектами («обами»), или λ-термами, построены исключительно из переменных применением аппликации и абстракции. Изначально наличие каких-либо констант не предполагается.
Аппликация и абстракция В основу λ-исчисления положены две фундаментальные операции:
Аппликация ( — прикладывание, присоединение) означает применение функции к заданному значению аргумента (то есть вызов функции). Её обычно обозначают , где — функция, а — аргумент. Это соответствует общепринятой в математике записи , которая тоже иногда используется, однако для λ-исчисления важно то, что трактуется как алгоритм, вычисляющий результат по заданному входному значению. В этом смысле аппликация может рассматриваться двояко: как результат применения к , или же как процесс вычисления этого результата. Последняя интерпретация аппликации связана с понятием β-редукции. Абстракция или λ-абстракция ( — отвлечение, отделение), в свою очередь, строит функции по заданным выражениям. Именно, если — выражение, содержащее , тогда запись означает: λ функция от аргумента , которая имеет вид , и обозначает функцию . Здесь скобки не обязательны и использованы для ясности, так как точка является частью нотации и отделяет имя связанной переменной от тела функции. Таким образом, с помощью абстракции можно конструировать новые функции. Требование, чтобы свободно входило в , не обязательно — в этом случае обозначает функцию , то есть такую, которая игнорирует свой аргумент.
α-эквивалентность Основная форма эквивалентности, определяемая в лямбда-термах, это альфа-эквивалентность. Например, и — это альфа-эквивалентные лямбда-термы, которые оба представляют одну и ту же функцию — а именно, функцию тождества . Термы и не являются альфа-эквивалентными, так как являются свободными переменными.
Вообще говоря, -преобразование — это переименование связанных переменных, не меняющее «смысла» терма. Структурно, два λ-терма -эквивалентны если это один и тот же терм, либо если какие-либо их составляющие термы соответственно -эквивалентны.
Для абстракций, терм -эквивалентен , если это в котором все свободные появления заменены на , при условии, что 1.) не входит свободно в , и 2.) не входит свободно ни в одну абстракцию внутри (если такие есть).
Требование, чтобы не была свободной переменной в — существенно, так как иначе она окажется «захваченной» абстракцией после -преобразования, и из свободной переменной в превратится в связанную переменную в .
Второе требование необходимо, чтобы предотвратить случаи, подобные тому, когда, например, является частью . Тогда необходимо произвести -преобразование такой абстракции, например, в данном случае, в .
β-редукция Применение некой функции к некоему аргументу выражается в -исчислении как аппликация -терма, выражающего эту функцию, и -терма аргумента. Например, применение функции к числу 3 выражается аппликацией
в которой на первом месте находится соответствующая абстракция. Поскольку эта функция ставит в соответствие каждому значение , для вычисления результата необходимо заменить каждое свободное появление переменной в терме на терм 3.
В результате получается . Это соображение в общем виде записывается как
и носит название β-редукция. Выражение вида , то есть применение абстракции к некоему терму, называется редексом (redex). Несмотря на то, что β-редукция по сути является единственной «существенной» аксиомой λ-исчисления, она приводит к весьма содержательной и сложной теории. Вместе с ней λ-исчисление обладает свойством полноты по Тьюрингу и, следовательно, представляет собой простейший язык программирования.
η-преобразование -преобразование выражает ту идею, что две функции являются идентичными тогда и только тогда, когда, будучи применёнными к любому аргументу, дают одинаковые результаты.
-преобразование переводит друг в друга формулы и , но только если не появляется свободно в . Иначе, свободная переменная в после преобразования стала бы связанной внешней абстракцией , и наоборот; и тогда применение этих двух выражений сводилось бы -редукцией к разным результатам.
Перевод в называют -редукцией, а перевод в — -экспансией.
Каррирование (карринг) Функция двух переменных и может быть рассмотрена как функция одной переменной , возвращающая функцию одной переменной , то есть как выражение . Такой приём работает точно так же для функций любой арности. Это показывает, что функции многих переменных могут быть выражены в λ-исчислении и являются «синтаксическим сахаром». Описанный процесс превращения функций многих переменных в функцию одной переменной называется карринг (также: каррирование), в честь американского математика Хаскелла Карри, хотя первым его предложил Моисей Шейнфинкель (1924).
Соответственно, аппликация n-арных функций — это на самом деле аппликация вложенных унарных функций, одна за другой. Например, для бинарных функций:
(λxy. ...x...y... ) a b = (λx.λy. ...x...y... ) a b = (λx.(λy. ...x...y... )) a b = ((λx.(λy. ...x...y... )) a) b = (λy. ...a...y... ) b = ...a...b...
Семантика бестипового λ-исчисления Тот факт, что термы λ-исчисления действуют как функции, применяемые к термам λ-исчисления (то есть, возможно, к самим себе), приводит к сложностям построения адекватной семантики λ-исчисления. Чтобы придать λ-исчислению какой-либо смысл, необходимо получить множество , в которое вкладывалось бы его пространство функций . В общем случае такого не существует по соображениям ограничений на мощности этих двух множеств, и функций из в : второе имеет бо́льшую мощность, чем первое.
Эту трудность в начале 1970-х годов преодолел Дана Скотт, построив понятие области (изначально на полных решёткахScott D.S. The lattice of flow diagrams.-- Lecture Notes in Mathematics, 188, Symposium on Semantics of Algorithmic Languages.-- Berlin, Heidelberg, New York: Springer-Verlag, 1971, pp. 311—372., в дальнейшем обобщив до полного частично упорядоченного множества со специальной топологией) и урезав до непрерывных в этой топологии функцийScott D.S. Lattice-theoretic models for various type-free calculi. — In: Proc. 4th Int. Congress for Logic, Methodology, and the Philosophy of Science, Bucharest, 1972.. На основе этих построений была создана языков программирования, в частности, благодаря тому, что с помощью них можно придать точный смысл таким двум важным конструкциям языков программирования, как рекурсия и типы данных.
Связь с рекурсивными функциями
Рекурсия — это определение функции через саму себя; на первый взгляд, лямбда-исчисление не позволяет этого, но это впечатление обманчиво. Например, рассмотрим рекурсивную функцию , вычисляющую факториал:
Эта функция не может быть выражена λ-термом λn.{ 1, if n = 0; else n × (fact (n-1)) }, так как в нём переменная fact является свободной, т.е. нигде не определённой. Эквивалентное выражение (G fact), где
G := λr.λn.{ 1, if n = 0; else n × (r (n-1)) }
оставляет открытым вопрос, что такое fact. Чтобы найти ответ на этот вопрос, необходимо прежде всего понять что G выражает собой один шаг вычисления факториала в парадигме "открытой рекурсии", вызывая полученную функцию r для выполнения "остатка вычислений". Рекурсивная функция — это, по определению, такая, которая использует саму себя для проведения остатка вычислений. То есть, должно выполняться:
Fact = G Fact = G (G Fact) = G (G (G (...)))
Таким образом, Fact является "неподвижной точкой" функционала G: вся работа выполняется повторением "шага вычислений" G неограниченное количество раз, как это продиктовано значением аргумента n:
Fact n = G Fact n = G (G Fact) n = G (G (G (...))) n
Функция ссылается на саму себя посредством ссылки на своё имя, но в лямбда-исчислении у λ-термов имен нет. Разрешение ссылки по имени достигается в программировании посредством лексического связывания через глобальный контекст, но в лямбда исчислении он является неизменяемым. В отсутствие изменяемого глобального контекста, локальный контекст создаётся использованием дополнительных аргументов:
Здесь функция использует аргумент и как функцию для вызова, в качестве "следующего шага вычислений", и передаёт его как дальнейший аргумент для последующего использования самой же вызванной фунцкцией . Вызов функции-аргумента для выполнения остатка вычислений называется "открытой рекурсией", потому что гипотетически может быть чем угодно. Вызов функции с самой собой в качестве аргумента на самом верхнем уровне, , "замыкает кольцо" и позволяет функции ссылаться на саму себя внутри своего тела, таким образом создавая функцию полностью эквивалентную оригинальной рекусивной функции .
Действительно, рекурсивная функция вызывает саму себя, и само-применяемая функция вызывает саму себя путём само-применения, передавая себя в качестве следующего шага вычислений, так же повторяя это и дальше снова и снова, сколько необходимо. Так как функция описывает один шаг вычисления факториала, повторное использование её снова и снова, по мере необходимости, описывает весь процесс вычисления факториала целиком.
В таком виде это синтаксически не-рекурсивное определение напрямую выражается как λ-терм:
F := λh. λn. { 1, if n = 0; else n × ((h h) (n-1)) } = λh. (λr.λn.{ 1, if n = 0; else n × (r (n-1)) }) (h h) = λh. G (h h) Fact := F F
Итак F h = G (h h), и следовательно F F = G (F F). λ-терм (F F) является неподвижной точкой λ-терма G, т.е. представлением рекурсивной функции , и G ссылается на него через параметр r, выполняя тождество:
Fact := F F = G (F F) = G Fact = G (G (G (...))) = U F = U (λh. G (h h)) = (λg. U (λh. g (h h))) G =: Y G U := λh. h h
где — это комбинатор самоприменения (самоаппликации), . Так несколькими элементарными само-очевидными преобразованиями сам собой получается т.н. "комбинатор неподвижной точки" (см. ниже), ,
Y := λg. U (λh. g (h h)) Fact := Y G = G (Y G)
Комбинатор создает рекурсивную функцию из аргумента, являющегося закрытым (то есть в котором нет свободных переменных) λ-термом исходного выражения функции (то есть без удвоения параметра). То есть — это комбинатор неподвижной точки: он вычисляет неподвижную точку своего аргумента. Для закрытого λ-терма с соответствующей арностью, его неподвижная точка выражает рекурсивную функцию, так как , то есть аргумент который здесь создаётся для вызова внутри — это та же самая функция :
Y g = U λh. g (h h) = g (U λh. g (h h)) = g (Y g)
Действительно,
Fact = Y (λr. λn. {1, if n = 0; else n × (r (n-1))}) = Y G = G (Y G) = (λr. λn. {1, if n = 0; else n × (r (n-1))}) (Y G) = ( λn. {1, if n = 0; else n × ((Y G) (n-1))}) = ( λn. {1, if n = 0; else n × (Fact (n-1))}) = G Fact
Итак, — это закрытый функционал, то есть λ-терм, вызывающий свой аргумент в качестве функции; его неподвижная (зафиксированная, неизменяемая) точка — это функция (здесь, ), которая передаётся ему в качестве аргумента; а вызов той же самой функции и есть рекурсивный вызов.
Используя , выписывать F явным образом становится излишним. Все что нужно это "функционал одного шага" G, и его повторение неограниченное число раз достигается автоматически:
Fact n = Y G n = G (Y G) n = G (G (G (...))) n = { 1, if n = 0; else n × (Y G (n-1)) } = ...
Чтобы определить факториал как рекурсивную функцию, мы можем просто написать , где — число, для которого вычисляется факториал. Пусть , получаем (подразумевая каррирование, (a b c) = ((a b) c)):
Y G 4 Y (λrn.{1, if n = 0; else n×(r (n-1))}) 4 (λrn.{1, if n = 0; else n×(r (n-1))}) (Y G) 4 (λn.{1, if n = 0; else n×(Y G (n-1))}) 4 {1, if 4 = 0; else 4×(Y G (4-1))} 4×(Y G 3) 4×(G (Y G) 3) 4×((λrn.{1, if n = 0; else n×(r (n-1))}) (Y G) 3) 4×{1, if 3 = 0; else 3×(Y G (3-1))} 4×(3×(G (Y G) 2)) 4×(3×{1, if 2 = 0; else 2×(Y G (2-1))}) 4×(3×(2×(G (Y G) 1))) 4×(3×(2×{1, if 1 = 0; else 1×(Y G (1-1))}))