ВУЗ:
Составители:
нечное значение выражения из его первоначального вида. Правила конверсии, описанные
ниже, являются достаточно общими, так, что, например, когда они применяются к λ–
терму, представляющему арифметическое выражение, то они моделируют вычисление
этого выражения.
Правила конверсии
• α–конверсия. Любая абстракция вида λV. E может быть конвертирована к терму λV'.
[V'/V]E. Мы переименовываем связные переменные так, чтобы избежать коллизии пе-
ременных.
• β–конверсия. Любая аппликация вида (λV. E
1
) E
2
конвертируется к терму [E
2
/V]E
1
.
• η–конверсия. Любая абстракция вида λV. (E V
), в которой V не имеет свободных
вхождений в терме E может быть конвертировано к E.
Если какой-то λ–терм E
1
α–конвертируется к терму E
2
, то это обозначается как
E
1
→
α
E
2
. Аналогично определяются обозначения
→
β
и →
η
. Наиболее важным видом
конверсии является β–конверсия; она единственная может использоваться для моделиро-
вания произвольного вычислительного механизма. α–конверсия применяется для техни-
ческих преобразований связных переменных и η–конверсия выражает тот факт, что две
функции, дающие один и тот же результат для любых аргументов, естественно считаются
равными.
Обсудим более подробно правила конверсии. Ламбда–выражение, к которому мо-
жет быть применено правило α–конверсии, называется α–редексом. «Редекс» есть абре-
виатура для «редуцируемое выражение». Правило α–конверсии говорит, что любая свя-
занная переменная может быть корректно переименована. Например, λx.x →
α
λy.y.
Ламбда–выражение, к которому может быть применено правило β–конверсии, на-
зывается β–редексом. Правило β–конверсии подобно вычислению вызова функции в язы-
ке программирования: тело E
1
функции λV. E
1
вычисляется в окружении (в контексте), в
котором «формальный параметр» V заменяется на «фактический параметр» E
2
.
Примеры:
(λx. f x) E →
β
f E
(λx. (λy. (add x y))) <3> →
β
λy. add <3> y
(λy. add <3> y) <4> →
β
add <3> <4>
Ламбда–выражение, к которому может быть применено правило η–конверсии, на-
зывается η–редексом. Правило η–конверсии выражает следующее свойство (называемое
экстенсиональностью): две функции являются равными, если они дают одинаковый ре-
зультат когда применяются к одинаковым аргументам. Действительно, λV. (E V) обозна-
чает функцию, которая возвращает [E'/V] (E V) когда применяется к аргументу E'. Если V
не является свободной в E, то [E'/V] (E V) = (E E'). Так как термы λV. (E V) и E оба воз-
вращают один и тот же результат (E E'), когда применяются к одинаковым аргументам, то,
следовательно, они обозначают одну и ту же функцию.
Примеры:
λx. add x →
η
add
λy. add x y →
η
add x
Но следующая конверсия
λx. add x x→
η
add x
54
Страницы
- « первая
- ‹ предыдущая
- …
- 52
- 53
- 54
- 55
- 56
- …
- следующая ›
- последняя »
