Во время чтения Lambda Calculus в Wiki натолкнулся на термин Захват, исключающий замены. Может кто-нибудь объяснить, что это значит, поскольку я не мог найти определение из любой точки.
Спасибо
PS
То, что я хочу знать, является причиной того, что операция Capture-избегая замещений. Было бы очень полезно, если кто-нибудь сможет это сделать
Обычно имена переменных, которые мы выбрали в исчислении лямбда, бессмысленны - функция x - это то же самое, что и функция a или b или c. Другими словами:
(λx. (λy.yx)) эквивалентно (λa. (λb.ba)) - переименование x в a и y в b ничего не меняет.
Из этого вы можете заключить, что любая замена допускается - то есть любая переменная в любом лямбда-термина может быть заменена любым другим. Это не так. Рассмотрим внутреннюю лямбда в первом выражении выше:
(λy.yx)
В этом выражении x является "свободным" - он не "связан" абстракцией лямбды. Если бы мы заменили y на x, выражение получилось бы следующим:
(λx.xx)
Это имеет совершенно другое значение. Оба x теперь относятся к аргументу абстракции лямбда. Этот последний x (который первоначально был "свободным" ) был "захвачен"; он "связан" абстракцией лямбды.
Замены, которые избегают случайного захвата свободных переменных, называются, невообразимо, "захватами, избегающими замещений".
Теперь, если бы все, о чем мы заботились в лямбда-исчислении, заменяли одну переменную на другую, жизнь была бы довольно скучной. Более реалистично, что мы хотим сделать, это заменить переменную лямбда-термином. Поэтому мы могли бы заменить переменную абстракцией лямбда (λx.t) или приложением (x t). В любом случае применяются те же соображения - когда мы выполняем подстановку, мы хотим убедиться, что мы не изменяем значение исходного выражения, случайно "фиксируя" переменную, которая изначально была бесплатной.
Переменная захватывается, если она помещается под лямбдой (или другими конструкциями связывания, если они существуют), которая связывает переменную. Он называл захват-избегание замещения, потому что этот процесс позволяет избежать случайного включения свободных переменных в замещение внутри исходного выражения.
Подстановка E для x в E (записано [E/x] E)
Пример: [y (λx. x)/x] λy. (λx. x) y x
После переименования: [y (λv. v)/x] λz. (λu. u) z x
После подстановки: λz. (λu. u) z (y (λv. v))