Лямбда-исчисление (λ-исчисление) — формальная система, разработанная американским математиком Алонзо Чёрчем для формализации и анализа понятия вычислимости.
Чистое λ-исчисление, термы которого, называемые также объектами («обами»), или λ-термами, построены исключительно из переменных применением аппликации и абстракции. Изначально наличие каких-либо констант не предполагается.
В основу λ-исчисления положены две фундаментальные операции:
Основная форма эквивалентности, определяемая в лямбда-термах, это альфа-эквивалентность. Например, λ x . x {displaystyle lambda x.x} и λ y . y {displaystyle lambda y.y} : альфа-эквивалентные лямбда-термы и оба представляют одну и ту же функцию (функцию тождества). Термы x {displaystyle x} и y {displaystyle y} не альфа-эквивалентны, так как они не находятся в лямбда-абстракции.
Поскольку выражение λ x .2 ⋅ x + 1 {displaystyle lambda x.2cdot x+1} обозначает функцию, ставящую в соответствие каждому x {displaystyle x} значение 2 ⋅ x + 1 {displaystyle 2cdot x+1} , то для вычисления выражения
( λ x .2 ⋅ x + 1 ) 3 {displaystyle (lambda x.2cdot x+1) 3} ,в которое входят и аппликация и абстракция, необходимо выполнить подстановку числа 3 в терм 2 ⋅ x + 1 {displaystyle 2cdot x+1} вместо переменной x {displaystyle x} . В результате получается 2 ⋅ 3 + 1 = 7 {displaystyle 2cdot 3+1=7} . Это соображение в общем виде записывается как
( λ x . t ) a = t [ x := a ] , {displaystyle (lambda x.t) a=t[x:=a],}и носит название β-редукция. Выражение вида ( λ x . t ) a {displaystyle (lambda x.t) a} , то есть применение абстракции к некому терму, называется редексом (redex). Несмотря на то, что β-редукция по сути является единственной «существенной» аксиомой λ-исчисления, она приводит к весьма содержательной и сложной теории. Вместе с ней λ-исчисление обладает свойством полноты по Тьюрингу и, следовательно, представляет собой простейший язык программирования.
η {displaystyle eta } -преобразование выражает ту идею, что две функции являются идентичными тогда и только тогда, когда, будучи применёнными к любому аргументу, дают одинаковые результаты. η {displaystyle eta } -преобразование переводит друг в друга формулы λ x . f x {displaystyle lambda x.f x} и f {displaystyle f} (только если x {displaystyle x} не имеет свободных вхождений в f {displaystyle f} : иначе, свободная переменная x {displaystyle x} после преобразования станет связанной внешней абстракцией или наоборот).
Функция двух переменных x {displaystyle x} и y {displaystyle y} f ( x , y ) = x + y {displaystyle f(x,y)=x+y} может быть рассмотрена как функция одной переменной x {displaystyle x} , возвращающая функцию одной переменной y {displaystyle y} , то есть как выражение λ x . λ y . x + y {displaystyle lambda x.lambda y.x+y} . Такой приём работает точно так же для функций любой арности. Это показывает, что функции многих переменных могут быть выражены в λ-исчислении и являются «синтаксическим сахаром». Описанный процесс превращения функций многих переменных в функцию одной переменной называется карринг (также: каррирование), в честь американского математика Хаскелла Карри, хотя первым его предложил М. Э. Шейнфинкель (1924).
Тот факт, что термы λ-исчисления действуют как функции, применяемые к термам λ-исчисления (то есть, возможно, к самим себе), приводит к сложностям построения адекватной семантики λ-исчисления. Чтобы придать λ-исчислению какой-либо смысл, необходимо получить множество D {displaystyle D} , в которое вкладывалось бы его пространство функций D → D {displaystyle D o D} . В общем случае такого D {displaystyle D} не существует по соображениям ограничений на мощности этих двух множеств, D {displaystyle D} и функций из D {displaystyle D} в D {displaystyle D} : второе имеет большую мощность, чем первое.
Эту трудность в начале 1970-х годов преодолел Дана Скотт, построив понятие области D {displaystyle D} (изначально на полных решётках, в дальнейшем обобщив до полного частично упорядоченного множества со специальной топологией) и урезав D → D {displaystyle D o D} до непрерывных в этой топологии функций. На основе этих построений была создана денотационная семантика языков программирования, в частности, благодаря тому, что с помощью них можно придать точный смысл таким двум важным конструкциям языков программирования, как рекурсия и типы данных.
Рекурсия — это определение функции через себя; на первый взгляд, лямбда-исчисление не позволяет этого, но это впечатление обманчиво. Например, рассмотрим рекурсивную функцию, вычисляющую факториал:
f(n) = 1, if n = 0; else n × f(n - 1).В лямбда-исчислении функция не может непосредственно ссылаться на себя. Тем не менее, функции может быть передан параметр, связанный с ней. Как правило, этот аргумент стоит на первом месте. Связав его с функцией, мы получаем новую, уже рекурсивную функцию. Для этого аргумент, ссылающийся на себя (здесь обозначен как r {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))В лямбда-исчислении, Y g {displaystyle operatorname {Y g} } — неподвижная точка 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)Теперь, чтобы определить факториал, как рекурсивную функцию, мы можем просто написать g ( Y g ) n {displaystyle operatorname {g (Y g)} n} , где n {displaystyle n} — число, для которого вычисляется факториал. Пусть n = 4 {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Каждое определение рекурсивной функции может быть представлено как неподвижная точка соответствующей функции, следовательно, используя Y {displaystyle operatorname {Y} } , каждое рекурсивное определение может быть выражено как лямбда-выражение. В частности, мы можем определить вычитание, умножение, сравнение натуральных чисел рекурсивно.
В языках программирования под «λ-исчислением» зачастую понимается механизм «анонимных функций» — callback-функций, которые можно определить прямо в том месте, где они используются, и которые имеют доступ к локальным переменным текущей функции (замыкание).