Подстановка

Определение.

Для термов М и N и переменной х результат подстановки [N/x]M -“ N на место х в М” определяется по индукции по построению терма М.

[N/x] x = N

[N/x] a = a

[N/x](M₁M₂) = ([N/x] M₁)([N/x] M₂)

[N/x](λх.M) = λх.M (т.к. х - связана)

[N/x](λу.M) = (λу.[N/x]М), если у ≠ х, уN (или хМ), иначе

=^(α)(λz.[N/x][z/y]M),

если у ≠ х, уN и xM, где z- новая переменная, не входящая ни в N, ни в М.

Это запрещает значению [N/x](λх.M) зависеть от связанной переменной у.

Пример. [3/y](y) →3

[3/y](x) →x

[3/y](y+x) →3+x

[3/y](λу.y)7+x+y) → ((λу.y)7+x+3)

┌───║───_↓

λу.((λу.y)7+x+y)3)

↑

┌─_↓

(λу.y+34) (λx.x) →((((λx.x)+)3)4) →((+3)4)

^↑──────└───┘ ^↑──┘

┌───_↓ ┌───_↓

Пример. (λx. λу. λz+ x(-yz))123→(λxyz.+x(-yz))123→((λyz.+1(-yz))2)3→

↑_________│ ↑_______│

| ↓

→(λz.+1(-2z))3→+1(-23)

↑

Вначале вычисляется выражение в скобках.

Дата добавления: 2014-01-11; Просмотров: 379; Нарушение авторских прав?; Мы поможем в написании вашей работы!