Лямбда-исчисление (также пишется как λ - исчисление ) — это формальная система в математической логике для выражения вычислений на основе абстракции функций и применения с использованием связывания переменных и подстановки . Это универсальная модель вычислений , которую можно использовать для моделирования любой машины Тьюринга . Он был введен математиком Алонзо Черчем в 1930-х годах в рамках его исследования основ математики .
Лямбда-исчисление состоит из построения лямбда-членов и выполнения над ними операций редукции. В простейшей форме лямбда-исчисления термы строятся с использованием только следующих правил:
производя такие выражения, как: (λ x .λ y .(λ z .(λ x .zx ) (λ y .zy ) ) ( xy )) . Скобки можно опустить, если выражение однозначно. Для некоторых приложений могут быть включены термины для логических и математических констант и операций.
Если используется индексация Де Брейна , то α-преобразование больше не требуется, так как не будет конфликтов имен. Если повторное применение шагов редукции в конце концов прекратится, то по теореме Черча-Россера оно даст β-нормальную форму .
Имена переменных не нужны, если используется универсальная лямбда-функция, такая как Iota и Jot , которая может создавать любое поведение функции, вызывая ее в различных комбинациях.
Лямбда-исчисление является полным по Тьюрингу , то есть представляет собой универсальную модель вычислений , которую можно использовать для моделирования любой машины Тьюринга . [1] Его тезка, греческая буква лямбда (λ), используется в лямбда-выражениях и лямбда-терминах для обозначения привязки переменной в функции .