Изменения
Нет описания правки
===Приоритет операций===
* Применение левоассоциативно: <tex>x\ y\ z\ w \equiv ((x\ y)\ z)\ w</tex>
* Аппликация Абстракция забирает себе всё, до чего дотянется: <tex>\lambda x\ .\ \lambda y\ .\ \lambda z\ .\ z\ y\ x \equiv \lambda x\ .\ (\lambda y\ .\ (\lambda z\ .\ ((z\ y)\ x)))</tex>
* Скобки играют привычную роль группировки действий
===α-конверсия===
{{Определение
|definition=''<tex>\alpha</tex>-конверсияконверсией'' {{---}} переименование связанной переменной. Выражениеназывается наименьшее соотношение эквивалентности на \Lambda такое что::<tex>P=_\lambda x\ .\ falpha P</tex> для любого <tex>P</tex> можно заменить на :<tex>\lambda x.P=_\alpha \lambda y\ .\ fP[x := y]</tex>, если <tex>y\not\in FV(P)</tex> не входит свободно в <tex>f</tex>,где и замкнуто относительно следующих правил::<tex>f[P=_\alpha P' \Rightarrow \forall x\in V:\lambda x.P=y]</tex> означает замену всех свободных вхождений <tex>_\alpha \lambda x.P'\\P=_\alpha P' \Rightarrow \forall Z \in \Lambda : P Z =_\alpha P'Z\\P=_\alpha P' \Rightarrow \forall Z \in \Lambda : Z P =_\alpha Z P'\\P=_\alpha P' \Rightarrow P'=_\alpha P\\P=_\alpha P' \ \& \ P'=_\alpha P'' \Rightarrow P=_\alpha P''\\</tex> в <tex>f</tex> на <tex>y</tex>.
}}
Стандартные функции булевой логики:
<tex>\operatorname{and} = \lambda n\ .\ \lambda m\ .\ \operatorname{if} \ n\ m\ \operatorname{false}</tex>
<tex>\operatorname{or} = \lambda n\ .\ \lambda m\ .\ \operatorname{if} \ n\ \operatorname{true} \ m</tex>
<tex>\operatorname{not} = \lambda b\ .\ \operatorname{if} \ b\ \operatorname{false} \ \operatorname{true}</tex>
Ещё одной важной функцией является функция проверки, является ли число нулём:
