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

UptoLike

ВУЗ: 

ТГУ | Томск

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

Рубрика: 

Последний пример предыдущего пункта говорит, что
(λf. λx .f <3> x) (λy. λx. add x y) <0> → add <0> <3>
Три правила конверсии сохраняют значения λ–выражений, т. е. если терм E реду-
цируется к терму E', то выражения E и E' обозначают одну и ту же функцию. Мы опреде-
лим понятие равенства λ–выражений.
Пусть E и E' есть λ–выражения. Говорят, что терм E равен терму E' (обозначают
как E = E'), если E → E' или E'→ E. Мы требуем также, чтобы введенное отношение ра-
венства для λ–выражений обладало свойством транзитивности. В частности, если E
1
→ E'
и E
2
→ E', то считается также E
1
= E
2
.
Говорят, что λ–выражение находится в нормальной форме, если к нему нельзя
применить никакое правило конверсии. Другими словами, λ–выражение – в нормальной
форме, если оно не содержит редексов. Нормальная форма, таким образом, соответствует
понятию конца вычислений в традиционном программировании. Отсюда немедленно вы-
текает наивная схема вычислений:
while существует хотя бы один редекс
do преобразовывать один из редексов
end
(выражение теперь в нормальной форме).
Различные варианты конверсии в процессе редукции могут приводить к принципи-
ально различным последствиям.
Пример:
(λx.λy.y) ((λz. z z) (λz.z z)
)
→ (λx.λy.y) ((λz.z z) (λz.z z)
)
→ (λx.λy.y) ((λz.z z) (λz.z z)
)
→ ...
(бесконечный процесс редукции)
(λx.λy.y) ((λz. z z) (λz.z z))
→ λy.y
(редукция закончилась)
Порядок редукций (стратегия выбора редексов)
Самым левым редексом называется редекс, первый символ которого текстуально
расположен в λ–выражении левее всех остальных редексов. (Аналогично определяется
самый правый редекс.)
Самым внешним редексом называется редекс, который не содержится внутри ника-
кого другого редекса.
Самым внутренним редексом называется редекс, не содержащий других редексов.
В контексте функциональных языков и λ–исчисления существуют два важных по-
рядка редукций [8].
Аппликативный порядок редукций (АПР), который предписывает вначале преобра-
зовывать самый левый из самых внутренних редексов.
Нормальный порядок редукций (НПР), который предписывает вначале преобразо-
вывать самый левый из самых внешних редексов.
В терме (λx.λy.y) ((λz.zz) (λz.z z)
) подчеркнут самый левый из самых внутренних
редексов – если его последовательно конвертировать, то редукция никогда не закончится.
56

Страницы