Лямбда-исчисление
Формальная модель вычислений. Алонзо Чёрч, 1930-е. Три базовых правила: переменные, абстракция (λx.тело), применение (f x). Тьюринг-полно — вычисляет всё, что может компьютер.
Основа функционального программирования. Каррирование (функции одного аргумента, возвращающие другие функции) названо в честь Хаскелла Карри. Y-комбинатор позволяет рекурсию без именованных функций. Типизированные лямбда-исчисления (простое типизированное → System F → исчисление конструкций) привели к Haskell, ML, Coq, Agda, Lean. Функциональное программирование — прямое наследство. Тезис Чёрча — Тьюринга утверждает, что лямбда-исчисление и машины Тьюринга выражают один и тот же класс вычислимого.