Ля́мбда-исчисле́ние ($\lambda$-исчисление), формальная система, используемая для определения и анализа понятия вычислимости, интенсионального (алгоритмического) определения функций, а также в качестве основы языка высказываний в формальной логике. Основная задача $\lambda$-исчисления – определение формальной системы правил построения вычислимых функций и оперирования ими. Функции в $\lambda$-исчислении задаются интенсионально, т. е. непосредственно, без отсылки к другим математическим объектам, таким как множества или отображения. Они строго описываются конечным и однозначно понимаемым набором правил преобразования аргумента в результат или, иначе говоря, алгоритмом вычисления. В логиках, основанных на $\lambda$-исчислении, функция выступает в качестве начального понятия, через которое с помощью дополнительных правил вывода или аксиом определяются все остальные математические сущности (в том числе множества и отображения).

Лямбда-исчисление даёт простое абстрактное синтаксическое определение функции как терма из класса, называемого также классом или множеством $\lambda$-термов, индуктивно определяемого в алфавите из счётного числа переменных и двух бинарных операций (абстракции и аппликации) с помощью набора из трёх правил построения:

1) любая переменная из выбранного алфавита является $\lambda$-термом (для условного обозначения переменных используют строчные буквы латинского алфавита);

2) для любой переменной из выбранного алфавита и любого $\lambda$-терма применение операции абстракции к их упорядоченной паре порождает $\lambda$-терм; операция абстракции обозначается символом $\lambda,$ который ставится перед абстрагируемой переменной и используется аналогично кванторам в математической логике (например, $\lambda x.\,x$);

3) применение операции аппликации к упорядоченной паре произвольных $\lambda$-термов также порождает $\lambda$‑терм; операция аппликации обозначается с помощью небольшого отступа, разделяющего её аргументы, имеет приоритет больший, чем у абстракции, и считается левоассоциативной, например $f\,x\,y = (f\,x)\,y.$

Пример $\lambda$-терма: $\left(\lambda yx.\,f\,y\,(\lambda y.\,f\,y)\right)\,(f\,x).$

Большинство вопросов, исследуемых с помощью $\lambda$-исчисления, сводятся к исследованию отношения $\alpha \beta \eta$‑редукции $(\rhd_{αβη}{}^*)$ на множестве $\lambda$-термов. Оно определяется как рефлексивное транзитивное конгруэнтное замыкание объединения трёх отношений, соответствующих трём базовым операциям $\lambda$‑исчисления:

• $\alpha$-конверсия (или $\alpha$-эквивалентность) задаётся отношением вида $\lambda x.\,X \cong_ \alpha \lambda y.\,X[x \mapsto y]$ при условии $y \not\in FV(X),$ где $FV(T)$ обозначает множество свободных (неабстрагированных) переменных (от англ. free variables) терма $T,$ а $T[x \mapsto U]$ – подстановку терма $U$ вместо свободных вхождений переменной $x$ в терме $T;$

• $\beta$-редукция задаётся отношением вида $( \lambda x.\,X)\, Y \rhd_ \beta X[x ↦ Y]$ при условии
  $BV(X) \cap FV(Y) = \emptyset ,$ где $BV(T)$ обозначает множество связанных (абстрагированных где-либо) переменных (от англ. bound variables) терма $T;$

• $\eta$-редукция задаётся отношением вида $\lambda x.\,X\, x\rhd_η X$ при условии $x \not\in FV(X).$

Например, $$\begin{array}{c} \left(\lambda yx.\,f\,y\, (\lambda y.\,f\, y)\right) \underline{(\lambda y.\,f\,x\,y)}\,{\rhd_η}^*\left(\lambda y \underline x.\,f\,y\,(\lambda y.\,f\,y)\right) \underline{(f\,x)}\,{\cong_\alpha}^*\\ \\ {\cong_\alpha}^*\left(\lambda y \underline z.\,f\,y\,(\lambda y.\,f\,y)\right) \underline{(f\,x)}\,{\rhd_β}^* \lambda z.\,f\,(f\,x)\,(\lambda y.\,f\,y), \end{array}$$и поэтому $\left(\lambda yx.\,f\ y\,(\lambda y.\,f\,y)\right) ( \lambda y.\,f\,x\,y)\,{\rhd_{αβη}}^* \lambda z.\,f\,(f\,x)\,(\lambda y.\,f\,y).$ Здесь символом $R^*$ обозначается рефлексивное транзитивное конгруэнтное замыкание отношения $R.$

Симметричное замыкание отношения $\rhd_{αβη}{}^*$ ($\cong _{αβη}$) является отношением эквивалентности ($\alpha \beta \eta$‑эквивалентности). Терм, связанный отношением $\rhd_{αβη}{}^*$ только с $\alpha$-эквивалентными себе термами, называется $\beta \eta$-нормальной формой. Объектом исследования $\lambda$-исчисления являются классы $\alpha \beta \eta$‑эквивалентных $\lambda$-термов, представляющие функции или выражения. Понятие вычисления задаётся отношением $\alpha \beta \eta$-редукции. Понятие результата вычисления – $\beta \eta$‑нормальной формой. В качестве тотальных либо частичных функций выступают $\lambda$-термы, имеющие $\beta \eta$-нормальную форму для любого либо не для любого возможного аргумента. Вычислимыми считаются функции, представимые в виде каких-либо $\lambda$‑термов, а логическое равенство рассматривается как отношение $\alpha \beta \eta$‑эквивалентности (возможно, расширяемое в дальнейшем с помощью правил вывода или аксиом).

Корректность определения вычислимых функций как классов $\alpha \beta \eta$-эквивалентных $\lambda$-термов может быть показана с помощью теоремы Россера – Чёрча, из которой следует существование различных классов $\alpha \beta \eta$-эквивалентности по крайней мере для всех $\beta \eta$-нормальных форм, не совпадающих с точностью до $\alpha$‑конверсии. Выразительность формализма $\lambda$-исчисления демонстрируется двумя теоремами об эквивалентности класса функций, представимых с помощью $\lambda$-термов, классу рекурсивных функций из теории вычислимости и классу функций, вычислимых на абстрактной машине Тьюринга. Соответственно, так же, как и с помощью машин Тьюринга, с помощью $\lambda$-исчисления можно показать существование невычислимых функций. Таковыми являются, в частности, функции проверки существования $\beta \eta$‑нормальной формы терма и предикат $\alpha \beta \eta$-эквивалентности.

Однако изначальной целью введения формализма $\lambda$-исчисления А. Чёрчем было исследование логических оснований математики. С этой целью $\lambda$‑исчисление предлагалось использовать в качестве основы языка формальной логики для записи математических функций, выражений и высказываний. В силу ограниченной выразительности самого формализма (представляет только вычислимые функции), для его использования в качестве основы языка математических высказываний необходимо по крайней мере его расширение с помощью некоторых символов, определяемых экстенсионально, т. е. с помощью правил вывода логики либо аксиом, выражающих семантику обозначений через постулируемые соотношения между ними. Однако при непосредственном применении расширенного таким способом $\lambda$‑исчисления для формализации математических доказательств возникает проблема, связанная с неконсистентностью (противоречивостью) получаемой логической системы. Соответствующий парадокс называется парадоксом Рассела и связан с высказыванием вида $R = (\lambda x.\,¬x\,x)\, (λx.\,¬ x\,x),$ которое является $\beta$-эквивалентным своему отрицанию и поэтому не может иметь значения истинности. Вместо рассмотренного изначального формализма $\lambda$‑исчисления, называемого также нетипизированным, в качестве основы языка высказываний формальной логики используются различные версии типизированного $\lambda$-исчисления, в которых вводится дополнительный синтаксический механизм ограничения возможного вида $\lambda$-термов. Самым простым из таких формализмов является просто типизированное $\lambda$‑исчисление, которое обеспечивает непредставимость $\lambda$-термов, не имеющих $\beta \eta$‑нормальной формы $($в частности, высказывания $R).$ Самой известной формальной логикой на основе просто типизированного $\lambda$‑исчисления является простая теория типов, называемая также логикой высшего порядка. Консистентность этой логики эквивалентна консистентности ограниченной теории множеств Цермело – Френкеля, что даёт высокую степень уверенности в её непротиворечивости. На использовании этой логики, в частности, основаны инcтрументы интерактивного доказательства теорем HOL4, HOL-Light, Isabelle, IMPS, ProofPower, PVS и TPS.

Так как $\lambda$-исчисление является одним из способов формализации понятия алгоритма (в силу полноты по Тьюрингу), оно может использоваться для формального исполнимого представления алгоритмов, т. е. для программирования. Многие языки программирования поддерживают основные возможности, предоставляемые формализмом $\lambda$-исчисления, а именно:

• возможность использования функций (по крайней мере ранее определённых) во всех контекстах, где могут быть использованы другие виды значений (например, целые числа), в частности в параметрах других функций, в качестве возвращаемого значения, а также внутри структур данных в памяти программы;

• возможность записывать функции с помощью нотации для абстракции переменной, используемой в $\lambda$-исчислении (такие функции в языках программирования часто также называют анонимными); поддержка такой нотации позволяет задавать определение функции непосредственно в месте её использования в качестве значения;

• поддержка нотации для левоассоциативной операции аппликации (применения функции), которая также называется поддержкой карринга или каррирования (по имени математика Х. Карри) и позволяет определять и использовать функции от нескольких аргументов как частный случай функций от одного аргумента, а также задавать новые анонимные функции без использования $\lambda$-абстракции (с помощью применения к части аргументов).

Языки программирования, поддерживающие эти возможности (не обязательно все), обычно называются функциональными или языками функционального программирования (например, Lisp, Closure, Erlang, OСaml, Haskell, F# и др.). Часть из них (например, Haskell, PureScript) также гарантирует возможность корректной (сохраняющей семантику) подстановки определения любой функции или выражения программы в любом месте их использования (упоминания). Такие языки функционального программирования называются чистыми, в них выполнение фрагмента программы можно рассматривать как $\alpha \beta \eta$-редукцию $λ$-терма. Функциональные языки также можно различать по принятому в них порядку выполнения (редукции) операций применения функций (аппликации) (бывают, в частности, строгие и аппликативные языки), а также по использованию механизма типизации термов. В частности, аппликативные языки (вычисляющие функции до их аргументов) позволяют вычислять нормальную форму любых термов (её имеющих), а строгие языки позволяют придавать семантику программам, использующим одновременно $\lambda$-исчисление и императивные конструкции (такие, например, как изменение значения переменной или ввод-вывод), но не наоборот; языки, использующие типизированное $\lambda$-исчисление, нуждаются в специальных синтаксических конструкциях для представления рекурсии (т. к. большинство рекурсивных комбинаторов не имеют нормальной формы и поэтому не могут быть типизированы), однако в них возможное представление значения выражения возможно определить на этапе компиляции, а встраивание (подстановка) функций и выражений в месте их использования гарантированно завершается за конечное время, что увеличивает возможности для оптимизации. Лямбда‑исчисление может также использоваться и для исследования семантики достаточно произвольных программ с помощью использования механизмов монад или алгебраических эффектов, позволяющих эффективно (с помощью локальных преобразований конструкций языка) представлять программы на различных языках программирования в виде $λ$‑термов. Для придания строгой логической семантики нетипизированным $λ$-термам (в том числе рекурсивным комбинаторам, которые не могут быть использованы в формальных логиках напрямую из-за возникающих логических противоречий) также существуют логические модели $\lambda$-исчисления, такие как денотационная семантика на основе теории домéнов Д. Скотта.