ВУЗ:
Составители:
не имеет место, поскольку переменная x свободна в add x.
Более общим понятием, по сравнению с конверсией, является понятие обобщенной
конверсии (по причинам, которые станут понятным позже, она также называется одноша-
говой редукцией). Терм M обобщенно α–конвертируется (β–конвертируется, η–
конвертируется) к терму N, если последний получается из M в результате конверсии како-
го-то подтерма в M, являющегося α–редексом (β–редексом, η–редексом, соответственно).
Обобщенная конверсии обозначается также как и просто конверсия: M →
α
N (аналогично
и для других видов обобщенной конверсии).
В следующих примерах конвертируемые редексы подчеркнуты.
((λx. (λy. (add x y))) <3>)
<4> →
β
(λy. add <3> y) <4>
(λy. add <3>y) <4>
→
β
add <3> <4>
Отметим, что в первой конверсии сам терм ((λx. (λy. (add x y))) <3>)<4> не является ре-
дексом. Мы будем иногда писать последовательность конверсий, подобных двум преды-
дущим как:
((λx. (λy. (add x y))) <3>)
<4> →
β
(λy. add <3> y) <4> →
β
add <3> <4>
В следующих двух примерах исходное исходное выражение одно и то же, но по-
следовательности конвертируемых редексов различны (используемые редексы подчерк-
нуты):
1) (λf. λx. f <3> x) (λy. λx.add x y)
<0>
→
β
(λx.(λy. λx . add x y) <3> x) <0>
→
η
(λz.(λy. λx . add x y) <3> z) <0> – выбрали один из двух возможных редексов
→
β
(λy.λz. add z y) <3> <0>
→
β
(λz. add z <3>) <0>
→
β
add <0> <3>
2) (λf. λx .f <3> x) (λy. λx. add x y)
<0>
→
β
(λx. (λy. λx. add x y) <3> x) <0> – выбрали один из двух возможных редексов
→
η
(λx.(λx. add x <3>)x ) <0>
→
β
(λz.(λx. add x <3>)z ) <0> – снова делаем произвольный выбор
→
β
(λz. add z <3>)<0>
→
β
add <0> <3>
Заметим, что в данном случае независимо от выбора редексов мы пришли к одина-
ковому результату.
9.1.4 Нормальные формы
Если λ–выражение E получается из λ–выражения E' с помощью последовательно-
сти обобщенных конверсий, то естественно считать, что E' получается в результате «вы-
числения» E, которое более точно выражается через понятие редукции.
Определение отношения редукции
Пусть E и E' есть λ–выражения. Говорят, что терм E редуцируется к терму E' (и обознача-
ют как E → E'), если E ≡ E' или существуют выражения E
1
, E
2
, …, E
n
такие что:
1. E ≡ E
1
2. E
n
≡ E'
3. Для каждого i выполнено одно из трех отношений E
i
→
α
E
i
+1
, E
i
→
β
E
i
+1
или E
i
→
η
E
i
+1
.
55
Страницы
- « первая
- ‹ предыдущая
- …
- 53
- 54
- 55
- 56
- 57
- …
- следующая ›
- последняя »
