Дельта-редукция (цитата)
Oct. 24th, 2010 11:11 amВыношу из комментариев цитату о дельта-редукции (Х. Барендрегт, «Лямбда-исчисление. Его синтаксис и семантика», перевод с английского Г. Е. Минца под редакцией А. С. Кузичева, 1985, глава 15 «Другие понятия редукции», § 3 «Дельта-редукция»).
Дельта-редукция — это не какое-то одно понятие редукции, а целая их совокупность. Все они определены на некотором расширении множества Λ [то есть множества λ-термов].
15.3.1. Определение. (i) Пусть δ — некоторая константа. Тогда Λδ обозначает множество λ-термов, построенных из переменных и константы δ с обычным использованием аппликации и абстракции [доступно краткое определение].
(ii) Аналогично определяется множество Λδ̅, где δ̅ — последовательность констант.
Дельта-редукция служит для того чтобы можно было сделать внутренними многие внешние функции ƒ на множестве Λ, постулировав δΜ̅ → ƒ(Μ̅) [Μ̅ — некоторая последовательность аргументов, специфичная для δ]. Это полезно для прикладного (особенно ориентированного на программирование) λ-исчисления.
Первый пример δ-редукции вводит тест на равенство двух н. ф. [нормальных форм].
15.3.2. Определение (δ-символ Черча). Пусть δC— некоторая константа. На множестве ΛδC введем следующее понятие редукции δC:
δCMN → T [T ≡ λxy.x, истина], если M, N ∈ βδC-NF⁰, M ≡ N [равны с точностью до альфа-конверсии],
δCMN → F [F ≡ λxy.y, ложь], если M, N ∈ βδC-NF⁰, M ≢ N,
где βδC-NF⁰ ⊆ ΛδC⁰ — множество замкнутых β-н.ф., не содержащих подтермов вида δCPQ.
15.3.1. Определение. (i) Пусть δ — некоторая константа. Тогда Λδ обозначает множество λ-термов, построенных из переменных и константы δ с обычным использованием аппликации и абстракции [доступно краткое определение].
(ii) Аналогично определяется множество Λδ̅, где δ̅ — последовательность констант.
Дельта-редукция служит для того чтобы можно было сделать внутренними многие внешние функции ƒ на множестве Λ, постулировав δΜ̅ → ƒ(Μ̅) [Μ̅ — некоторая последовательность аргументов, специфичная для δ]. Это полезно для прикладного (особенно ориентированного на программирование) λ-исчисления.
Первый пример δ-редукции вводит тест на равенство двух н. ф. [нормальных форм].
15.3.2. Определение (δ-символ Черча). Пусть δC— некоторая константа. На множестве ΛδC введем следующее понятие редукции δC:
δCMN → T [T ≡ λxy.x, истина], если M, N ∈ βδC-NF⁰, M ≡ N [равны с точностью до альфа-конверсии],
δCMN → F [F ≡ λxy.y, ложь], если M, N ∈ βδC-NF⁰, M ≢ N,
где βδC-NF⁰ ⊆ ΛδC⁰ — множество замкнутых β-н.ф., не содержащих подтермов вида δCPQ.
