ВУЗ:
Составители:
= (add <2> (summa <1>))
= (add <2> (If (iszero <1>) <0> (add <1> (summa (pre <1>)))))
= (add <2> (add <1> (summa (pre <1>))))
= (add <2> (add <1> (summa <0>)))
= (add <2> (add <1> (If (iszero <0>) <0> (add <0> (summa (pre <0>))))))
= (add <2> (add <1> <0>))
= (add <2> <1>)
= <3>
Приведенное выше уравнение для summa предполагает, что терм summa может
быть определен как
summa = λ m. If (iszero m) <0> (add m (summa (pre m)))
Но такое определение невозможно в λ–исчислении, поскольку определяемый терм не мо-
жет присутствовать в правой части определения. И здесь на помощь приходит комбинатор
неподвижной точки. Определим вспомогательный терм
summaf = λ f m. If (iszero m) <0> (add m (f (pre m)))
и затем определим summa = Y summaf. Получаем искомое уравнение:
summa <m> = (Y summaf )<m>
= summaf (Y summaf ) <m>
= (по определению summa) summaf summa <m>
= (λ f m. If (iszero m) <0> (add m (f (pre m)))) summa <m>
= If (iszero <m>) <0> (add <m> (summa (pre <m>)))
Уравнение вида f x
1
… x
n
= E называется рекурсивным, если f имеет свободное
вхождение в E. Комбинатор Y обеспечивает общий путь решения такого уравнения. Начи-
наем с уравнения в форме f x
1
… x
n
= ~ f ~, где ~ f ~ есть некоторое λ–выражение, содер-
жащее f. Затем определяем f как
f = Y (λ f x
1
… x
n
. ~ f ~)
Проверим, что f удовлетворяет необходимому уравнению:
f x
1
… x
n
= (Y (λ f x
1
… x
n
. ~ f ~)) x
1
… x
n
= (по свойству Y) (λ f x
1
… x
n
. ~ f ~) (Y (λ f x
1
… x
n
. ~ f ~)) x
1
… x
n
= (по определению f) (λ f x
1
… x
n
. ~ f ~) f x
1
… x
n
= ~ f ~
Хотя с математической точки зрения использование комбинатора Карри совершен-
но безукоризненно, но с точки зрения программирования вычислительный переход от вы-
ражения E (Y E) к выражению Y E и обратно нельзя осуществить только с помощью β–
конверсии. По этой причине более удобен комбинатор неподвижной точки, предложен-
ный Тьюрингом:
T ≡ (λx y. y(x x y)) (λx y. y(x x y))
65
Страницы
- « первая
- ‹ предыдущая
- …
- 63
- 64
- 65
- 66
- 67
- …
- следующая ›
- последняя »
