Коллизия имен переменных

Чтобы ввести новые имена используется α - конверсия, она позволяет изменять имена свободной переменной x.

(х+(λx.-х3)2)не сможет дать какую-либо характеристику переменной.

Использование (α) - конверсии позволит изменить имя свободной переменной.

(х+(λx.-х3)2)(у+(λx.-х3)2) получим свободное вхождение у и связное вхождение х.

Изменение статуса переменной при подстановке называется коллизией переменных.

Коллизия переменных может служить источником ошибок в вычислениях.

Пример

Прямая редукция терма (λxy.x)y дает неверный результат

(λxy.x)y →^(β) λy.y,

а если предварительно переименовать связанную переменную y, получится верный результат:

(λxy.x)y →^(α) (λxz.x)y →^(β) λz.y ≠ λy.y.

Дата добавления: 2014-01-11