Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
From ordinary variables x, y, z… to λβη
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). иначе остается лишь правая часть аппликации.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment