From ordinary variables x, y, z… to λβη

lambdabetaeta

x ∈ Λ;                                                                          Лямбда-выражения строятся из переменных
M, N ∈ Λ ⇒ λx.M ∈ Λ ∧ M N ∈ Λ;                                                  с помощью абстракций и аппликаций;
(M) = M, M N P = (M N) P.                                                       причем аппликация лево-ассоциативна.

x[x := P] = P;                                                                  Подстановка заменяет вхождения переменной на другое выражение,
y[x := P] = y;                                                                  но только если переменная совпадает,
(λx.M)[x := P] = λx.M;                                                          при этом связанные переменные не подлежат подстановке;
(λy.M)[x := P] = λy.M[x := P];                                                  операция подстановки через абстракции
(M N)[x := P] = M[x := P] N[x := P].                                            и аппликации проходит выражение рекуррентно.

FV(x) = {x};                                                                    Самостоятельная переменная считается свободной,
FV(λx.M) = FV(M) ∖ {x};                                                         если она не связана абстракцией, а через абстракции и
FV(M N) = FV(M) ∪ FV(N).                                                        аппликации множество свободных переменных строится индуктивно.

y ∉ FV(M) ⇒ λx.M = λy.M[x := y].                                                Вхождения связанной переменной можно заменить на другую переменную (альфа-конверсия).

β = {((λx.M) N, M[x := N]) | M, N ∈ Λ};                                         Бета-редукция применяет функцию к аргументу, подставляя его вместо связанной переменной;
η = {(λx.M x, M) | M ∈ Λ, x ∉ FV(M)};                                           эта-редукция, в свою очередь, сокращает лишнюю операцию;
βη = β ∪ η.                                                                     объединение этих двух редукций называют бета-эта-редукцией.

M ⊂ M ⊂ λx.M;                                                                   Выражение считается подвыражением самого себя; тело абстракции
M ⊂ M N ⊃ N;                                                                    и обе части аппликации также являются подвыражениями;
M ⊂ N ∧ N ⊂ P ⇒ M ⊂ P.                                                          данное отношение транзитивно.

Fˡ(x) = x;                                                                      Определение нормальной стратегии: переменная не может быть редексом;
∃Q ∈ Λ: (M, Q) ∈ βη ⇒ Fˡ(M) = Q;                                                если выражение является редексом, то за ним приоритет;
∄Q ∈ Λ: (λx.M, Q) ∈ βη ⇒ Fˡ(λx.M) = λx.Fˡ(M);                                   если абстракция не является эта-редексом, то следует рассмотреть ее тело;
∄Q ∈ Λ: (M N, Q) ∈ βη ∧ ∃P ⊂ M: ∃Q ∈ Λ: (P, Q) ∈ βη ⇒ Fˡ(M N) = Fˡ(M) N;        если аппликация не является бета-редексом, то приоритет за левой ее частью с подвыражением-редексом,
∄Q ∈ Λ: (M N, Q) ∈ βη ∧ ∄P ⊂ M: ∃Q ∈ Λ: (P, Q) ∈ βη ⇒ Fˡ(M N) = M Fˡ(N).        иначе остается лишь правая часть аппликации.