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

UptoLike

ВУЗ: 

ТГУ | Томск

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

Рубрика: 

(( … (E
1
E
2
)… )E
n
). Например, E
1
E
2
E
3
обозначает ((E
1
E
2
) E
3
).
• λV. E
1
E
2
… E
n
обозначает (λV. (E
1
E
2
… E
n
)). Область действия λV распростра-
няется направо так далеко как это возможно.
• Операция абстракции является право–ассоциативной, т. е. λV
1
. λV
2
. … λV
n
. E
обозначает (λV
1
. (λV
2
. (… (λV
n
. E) … ))). Запись λV
1
. λV
2
. … λV
n
. E иногда еще
более сокращают λV
1
V
2
… V
n
. E. Так, например, λx y z. E обозначает
(λx.(λy.(λz.E))).
9.1.3 Вычисление ламбда–выражений
Переменная, расположенная не на месте связанной переменной, может быть свя-
занной или свободной, что определяется с помощью следующих правил:
1. Переменная x оказывается свободной в выражении x.
2. Все x, имеющиеся в λx.M, являются связанными. Если кроме x в λx.M есть переменная
y, то последняя будет свободной или связанной в зависимости от того, свободно она
или связанна в M.
3. Переменная встречающаяся в термах M или N выражения (MN) будет связанной или
свободной в общем терме в зависимости от того, свободна она или связанна в M или N.
Свободные (связанные) переменные – это переменные, которые, по крайней мере,
один раз появляются в терме в свободном (связанном) виде.
Нам понадобится следующее определение подстановки терма в другой терм вме-
сто свободного вхождения переменной. Для любых λ–термов M, N и переменной x через
[N/x]M обозначим результат подстановки N вместо каждого свободного вхождения x в M и
замены всех λy в M таким образом, чтобы свободные переменные из N не стали связан-
ными в [N/x]M. Мы употребляем запись M ≡ N для обозначения того, что термы M и N
совпадают.
Подстановка
a) [N/x]x ≡ N;
b) [N/x]y ≡ y, если переменная y не совпадает с x;
c) [N/x] (PQ) ≡ ([N/x]P [N/x]Q);
d) [N/x] (λx.P) ≡ λx.P;
e) [N/x] (λy.P) ≡ λy.[N/x]P, если y не имеет свободных вхождений в N и x имеет свободное
вхождение в P;
f) [N/x](λy.P) ≡ λz.[N/x]([z/y]P), если y имеет свободное вхождение в N и x имеет свобод-
ное вхождение в P и z – любая переменная, не имеющая свободных вхождений в N.
Следующие примеры пояснят суть определения. Пусть M≡λy.yx.
Если N ≡ vx, то [(vx)/x](λy.yx) ≡ λy. [(vx)/x](yx) согласно (e)
≡ λy. y(vx) согласно (a).
Если N ≡ yx, то [(yx)/x](λy.yx) ≡ λz. [(yx)/x](zx) согласно (f)
≡ λz.z(yx) согласно (a).
Введенное понятие подстановки требует должной мотивации. Для этого необходи-
мо снова вспомнить о коллизии переменных при неаккуратной подстановке (см. 2.3.4).
Если бы пункт (f) в определении подстановки был опущен, то мы столкнулись бы
со следующим нежелательным явлением. Хотя λv.x и λy.x обозначают одну и ту же функ-
цию (константу, чье значение всегда есть x), после подстановки v вместо x они стали бы
обозначать разные функции: [v/x](λy.x) ≡ λy.v, [v/x](λv.x) ≡ λv.v.
Мы рассмотрели, как λ–нотация может быть использована для представления
функциональных выражений и сейчас готовы к тому, чтобы определить правила конвер-
сии λ–исчисления, которые описывают, как вычислять выражение, т. е. как получать ко-
53

Страницы