Математическое введение в декларативное программирование. Зюзысов В.М. - 58 стр.

UptoLike

ВУЗ: 

ТГУ | Томск

Составители: 

Рубрика: 

K E
1
E
2
= E
1
S E
1
E
2
E
3
= (E
1
E
3
) (E
2
E
3
)
Любой замкнутый λ–терм можно выразить с помощью аппликации (комбинации) двух
комбинаторов K и S, называемых примитивными комбинаторами. Определим комбинатор
I ≡ S K K, тогда I x ≡ (S K K) x ≡ S K K x → (K x) (K x) ≡ K x (K x) → x. В силу η–
конверсии, I = λx. x.
Теорема 16 (Теорема о функциональной полноте комбинаторов). Любое λ–
выражение равно λ–выражению построенному из примитивных комбинаторов K и S и пе-
ременных с помощью только операции аппликации без использовании операции λ–
абстракции.
Доказательство этой теоремы см. в [1, стр. 158-171] и, в более элементарном изложении, в
[10, cтр. 91–97].
Например, λx. f x = S (K f) (S K K). Действительно, (S (K f) (S K K)) y ≡ (S (K f) I) y ≡
S (K f) I y → ((K f) y) (I y) ≡ (K f y) (I y) → f (I y) → f y. Таким образом, искомое равенство
получается в силу η–конверсии. Как произвольное λ–выражение можно транслировать в
комбинаторную форму см. [8, стр. 294–296].
9.2 Ламбда–исчисление как язык программирования
В описанном виде λ–исчисление является примитивным языком. Однако его мож-
но использовать для представления объектов и структур современного языка программи-
рования. Идея состоит в представление этих объектов и структур в виде λ–выражений та-
ким образом, чтобы они обладали требуемыми свойствами. Например, для представления
логических значений истинности true и false и логической связки «отрицание» (not) λ–
выражения true, false и not должны удовлетворять свойствам:
not true = false
not false = true
Для того, чтобы представить конъюнкцию (and) соответствующее λ–выражение and
должно обладать свойствами:
and true true = true
and true false = false
and false true = false
and false false = false
Подобно этому мы должны ожидать определенные свойства от λ–выражения or, пред-
ставляющего операцию дизъюнкции or для логических значений. Выбор λ–выражений
для представления программных объектов, на первый взгляд, может выглядеть немотиви-
рованным, однако, все предлагаемые определения согласованы так, что они могут рабо-
тать в унисон.
9.2.1 Истинностные значения и условное выражение
Определим λ–выражения true, false, not и условное выражение If так, чтобы вы-
полнялись следующие свойства:
not true = false
not false = true
If true E
1
E
2
= E
1
58

Страницы