Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- 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). иначе остается лишь правая часть аппликации.
Add Comment
Please, Sign In to add comment