При чтении лямбда-исчисления в Wiki натолкнулся на термин Захватывающие замещения. Может кто-нибудь объяснить, что это значит, поскольку я не мог найти определение из любой точки.Что имеется в виду под «Захват, избегающий замещений»?
Благодаря
PS
То, что я хочу знать, является причиной говорить, что операция Capture избегающих замены. Было бы большим подспорьем, если кто-то может сделать это
Как правило, конкретные имена переменных, которые мы выбрали в лямбда-исчислении бессмысленны - функция x это то же самое, как функция a или b или c. Другими словами:
(. Хх (λy.yx)) эквивалентно - переименование x в a и y к b делает не ничего менять (ХА (λb.ba).).
Из этого можно сделать вывод, что любая замена допускается - то есть любая переменная в любом лямбда-термина может быть заменена любым другим. Это не так. Рассмотрим внутреннюю лямбда в первом выражении выше:
(λy.yx)
В этом выражении, x «свободен» - это не «связан» с помощью лямбда-абстракции. Если бы мы должны были заменить y с x, выражение стало бы:
(λx.xx)
Это имеет совсем другое значение. Оба значения x теперь относятся к аргументу абстракции лямбда. Тот последний x (который изначально был «бесплатным») был «захвачен»; он «связан» абстракцией лямбды.
Замены, которые избегают случайного захвата свободных переменных, называются, невообразимо, «замещениями, исключающими захват».
Теперь, если все, о чем мы заботились в исчислении лямбда, заменяли одну переменную на другую, жизнь была бы довольно скучной. Более реалистично, что мы хотим сделать, это заменить переменную лямбда-термина. Поэтому мы могли бы заменить переменную лямбда-абстракцией (λx.t) или приложение (x t). В любом случае применяются те же самые соображения - когда мы выполняем подстановку, мы хотим убедиться, что мы не изменяем значение исходного выражения, случайно «фиксируя» переменную, которая изначально была свободной.
Замещение Е «для х в Е (написано [E»/х] Е)
Пример: [y (λx. X)/x] λy. (λx. x) y x
После переименования: [y (λv. v)/x] λz. (λu. u) z x
После подстановки: λz. (λu. u) z (yu (u, v))
Что я действительно хочу знать, так это то, что это называется захватом, избегающим замещения. Я имею в виду концептуально. – Pradeep
@Jaguar, является ли x связанным в (λx. (Λy.yx))? Поскольку внешнее выражение имеет x в качестве аргумента. Или он связан по отношению к (λx. (Λy.yx)) и свободен по отношению к (λy.yx)? –
Переменная зарегистрирована, если она помещена под лямбдой (или другими конструкциями связывания, если они существуют), которая связывает переменную. Это называется замещение захвата, потому что этот процесс позволяет избежать случайного включения свободных переменных в подстановку внутри исходного выражения.
Большое вам спасибо! Актуальность слова «захват» не была объяснена в материалах, которые я читал, что оставило меня в недоумении за то, что было намерено. – Paul
@Ord, является ли x связанным в (λx. (Λy.yx))? Поскольку внешнее выражение имеет x в качестве аргумента. Или он связан по отношению к (λx. (Λy.yx)) и свободен по отношению к (λy.yx)? –
x будет связан в выражении (λx. (Λy.yx)) и свободен в выражении (λy.yx). – Ord