Лямбда-исчисление

---

Ля́мбда-исчисле́ние (λ-исчисление) — формальная система, разработанная американским математиком Алонзо Чёрчем для формализации и анализа понятия вычислимости.

Чистое λ-исчисление, термы которого, называемые также объектами («обами»), или λ-термами, построены исключительно из переменных применением аппликации и абстракции. Изначально наличие каких-либо констант не предполагается.

Основная форма эквивалентности, определяемая в лямбда-термах, это альфа-эквивалентность. Например, ${\displaystyle \lambda x.x}$ и ${\displaystyle \lambda y.y}$ - это альфа-эквивалентные лямбда-термы, которые оба представляют одну и ту же функцию — а именно, функцию тождества ${\displaystyle x\mapsto x}$. Термы ${\displaystyle x}$ и ${\displaystyle y}$ не являются альфа-эквивалентными, так как являются свободными переменными.

Вообще говоря, ${\displaystyle \alpha }$-преобразование - это переименование связанных переменных, не меняющее «смысла» терма. Структурно, два λ-терма ${\displaystyle \alpha }$-эквивалентны если это один и тот же терм, либо если какие-либо их составляющие термы соответстветственно ${\displaystyle \alpha }$-эквивалентны.

Для абстракций, терм ${\displaystyle \lambda y.t[y]}$ ${\displaystyle \alpha }$-эквивалентен ${\displaystyle \lambda x.t[x]}$, если ${\displaystyle t[y]}$ это ${\displaystyle t[x]}$ в котором все свободные появления ${\displaystyle x}$ заменены на ${\displaystyle y}$, при условии, что 1.) ${\displaystyle y}$ не входит свободно в ${\displaystyle t[x]}$, и 2.) ${\displaystyle x}$ не входит свободно ни в одну абстракцию ${\displaystyle \lambda y}$ внутри ${\displaystyle t[x]}$ (если такие есть).

---