The Lambda Calculus (2023)
Лямбда-исчисление — это минималистичный формализм для представления функций и их применения, основанный на двух ключевых операциях: абстракции (создание функции через λx.M) и аппликации (применение функции к аргументу, записывается как MN). Его синтаксис крайне лаконичен, но он позволяет выражать любые вычисления через правила подстановки.
Центральное правило — β-редукция: (λx.M)N сводится к M[x:=N], то есть замене всех вхождений x в M на N. Это отражает идею вычисления через подстановку аргумента. Например, (λx.x²−2x+5)2 даёт 2²−2·2+5=5. Важно, что функции здесь трактуются не как множества пар, а как правила преобразования, что делает теорию неэкстенсиональной.
Лямбда-исчисление легло в основу теории вычислений, логики и программирования, демонстрируя, как простые синтаксические правила могут порождать богатую семантику. Оно показывает, что даже в такой скудной нотации можно выразить всю вычислимую математику.