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

UptoLike

ВУЗ: 

ТГУ | Томск

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

Рубрика: 

все функции анонимны, и мы не можем использовать их имена, чтобы организовать ре-
курсивный вызов. Как это не удивительно, но рекурсия в λ–исчислении возможна! Но
этот факт, как и существование функции предшествования, был открыт только после зна-
чительных усилий.
Ключевой идеей послужило использование так называемого комбинатора непод-
вижной точки. Замкнутый λ–терм Y называется комбинатором неподвижной точки, если
для любого терма f выполнено соотношение f (Y f) = Y f. Другими словами, комбинатор
неподвижной точки, примененный для любой функции f, возвращает неподвижную точку
этой функции. Первый такой комбинатор был найден Карри и обычно обозначается Y.
Этот комбинатор напоминает парадокс Рассела и поэтому называется «парадоксальным
комбинатором». Если мы определим
R = λx. not (x x),
то обнаружим, что
R R = not (R R)
Таким образом, терм R R служит неподвижной точкой для оператора отрицания. Для того,
чтобы получить общий комбинатор неподвижной точки, мы должны заменить отрицание
на произвольный терм f. Поэтому мы определяем:
Y ≡ λ f. (λx .f (x x)) (λx .f (x x))
Проверим, что Y удовлетворяет требуемым условиям. С одной стороны,
Y E ≡ (λ f. (λx .f (x x)) (λx .f (x x))) E
→
β
(λx . E (x x)) (λx . E (x x))
→
β
E ((λx . E (x x)) (λx . E (x x)))
С другой стороны,
E (Y E) ≡ E ((λ f. (λx .f (x x)) (λx .f (x x))) E)
→
β
E ((λx . E (x x)) (λx . E (x x)))
Так как оба терма Y E и E (Y E) редуцируются к терму E ((λx . E (x x)) (λx . E (x x))), то
E (Y E) = Y E. Таким образом, мы получили, что каждое λ–выражение E имеет неподвиж-
ную точку Y E.
Рассмотрим теперь представление рекурсивных функций в λ–исчислении. В каче-
стве примера, попробуем определить λ–выражение summa, такое что
summa <m> = add <m> (add <m–1> ( … (add <1> <0>) … ))
Нетрудно увидеть, что summa должно удовлетворять уравнению:
summa <m> = If (iszero <m>) <0> (add <m> (summa (pre <m>)))
Пусть это имеет место, тогда, например,
summa <2> = If (iszero <2>) <0> (add <2> (summa (pre <2>)))
= (add <2> (summa (pre <2>)))
64

Страницы