ВУЗ:
Составители:
В терме (λx.λy.y) ((λz .z z) (λz .zz))
подчеркнут самый левый из самых внешних ре-
дексов – редукция в этом случае заканчивается за один шаг.
Функция λx.λy.y – это классический пример функции, которая отбрасывает свой
аргумент. НПР в таких случаях эффективно откладывает вычисление любых редексов
внутри выражения аргумента до тех пор, пока это возможно, в расчете на то, что такое
вычисление может оказаться ненужным.
В функциональных языках стратегии НПР соответствуют так называемые ленивые
вычисления. «Не делай ничего, пока это не потребуется» – механизм вызова по необходи-
мости (все аргументы передаются функции в не вычисленном виде и вычисляются только
тогда, когда в них возникает необходимость внутри тела функции). Haskell – один из язы-
ков с ленивыми вычислениями.
Стратегия АПР приводит к энергичным вычислениям. «Делай все, что можешь»;
другими словами, не надо заботиться о том, пригодится ли, в конечном счете, полученный
результат. Таким образом, реализуется механизм вызова по значению (значение аргумен-
та передается в тело функции). В языке Лисп реализуются, как правило, энергичные вы-
числения.
Теорема 14 (Теорема Чёрча-Россера о свойстве ромба) [1, с.78]. Если E → E
1
и E →
E
2
, то существует терм E' такой, что E
1
→ E' и E
2
→ E'.
Следствие 1. Если E
1
= E
2
, то существует терм E' такой, что E
1
→ E' и E
2
→ E'.
Следствие 2. Если выражение E может быть приведено двумя различными спосо-
бами к двум нормальным формам, то эти нормальные формы совпадают или могут быть
получены одна из другой с помощью замены связанных переменных.
Теорема 15 (Теорема стандартизации) [1, с. 298–303]. Если выражение E имеет
нормальную форму, то НПР гарантирует достижение этой нормальной формы (с точно-
стью до замены связанных переменных).
9.1.5 Комбинаторы
Теория комбинаторов была развита российским математиком Шейфинкелем [15]
перед тем как ламбда–обозначения были введены Чёрчем. Вскоре Карри переоткрыл эту
теорию независимо от Шейфинкеля и Чёрча. Теорию комбинаторов так же как и λ–
исчисление можно использовать для представления функций. Комбинаторы также обес-
печивают хороший промежуточный код для обычных компьютеров: несколько лучших
компиляторов для ленивых функциональных языков базируются на комбинаторах [8].
Существует два эквивалентных способа формализации теории комбинаторов:
1) внутри λ–исчисления;
2) как полностью независимую теорию.
Следуя первому подходу, определим комбинатор просто как λ–терм, не имеющих
свободных переменных. Такой терм также называется замкнутым – он имеет фиксирован-
ное значение независимо от значения любой переменной. Оказывается любое λ–
выражение равно некоторому выражению, построенному с помощью аппликации из пе-
ременных и двух комбинаторов K и S. Операция β–конверсии может быть смоделирована
с помощью простейших операций для K и S.
Определения комбинаторов K и S
K ≡ λx y. x
S ≡ λf g x . (f x) (g x)
Из этих определения, используя β–конверсию получаем, что для любых термов E
1
,
E
2
и E
3
выполнено
57
Страницы
- « первая
- ‹ предыдущая
- …
- 55
- 56
- 57
- 58
- 59
- …
- следующая ›
- последняя »
