Ответ 1
Обычно имена переменных, которые мы выбрали в исчислении лямбда, бессмысленны - функция 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). В любом случае применяются те же соображения - когда мы выполняем подстановку, мы хотим убедиться, что мы не изменяем значение исходного выражения, случайно "фиксируя" переменную, которая изначально была бесплатной.