Podczas czytania rachunku Lambda na Wiki, natknąłem się na termin Zastąpienie uniknięcia przechwytywania. Czy ktoś może mi wyjaśnić, co to znaczy, ponieważ nie mogłem znaleźć definicji z dowolnego miejsca.Co to jest "substytucje unikające przechwytywania"?
Dzięki
PS
Co chcę wiedzieć jest powodem mówi, że operacja capture-unikanie podstawienia. Byłoby bardzo pomocne, jeśli ktoś może zrobić
Normalnie konkretne nazwy zmiennych, które wybraliśmy w rachunku lambda są bez znaczenia - funkcja x to samo jako funkcja a lub b lub c. Innymi słowy:
(. Λx (λy.yx)) jest równoważne - zmiana nazwy x do a i y do b robi nie nic zmieniać (λa (λb.ba).).
Z tego można wywnioskować, że dowolne zastąpienie jest dozwolone - tj. Dowolna zmienna w dowolnym terminie lambda może być zastąpiona przez dowolną inną. Tak nie jest. Rozważmy wewnętrzną lambda pierwszego wyrażenia powyżej:
(λy.yx)
W tym wyrażeniu x jest „wolne” - to jest „związany” przez pobór lambda. Gdybyśmy mieli zastąpić y z x wyrażenie staną:
(λx.xx)
ten ma zupełnie inne znaczenie. Zarówno x s teraz odnoszą się do argumentu do abstrakcji lambda. Ten ostatni x (który pierwotnie był "bezpłatny") został "schwytany"; jest "związany" przez abstrakcję lambda.
Zastępstwa, które pozwalają uniknąć przypadkowego uchwycenia wolnych zmiennych, nazywane są niewyobrażalnie "podstawami unikania przechwytywania".
Jeśli wszystko, na czym nam zależało w rachunku lambda, zastępuje jedną zmienną inną, życie byłoby dość nudne. Bardziej realistycznie, chcemy zastąpić zmienną terminem lambda. Możemy więc zamienić zmienną na abstrakcję lambda (λx.t) lub aplikację (x t). W obu przypadkach obowiązują te same rozważania - gdy dokonamy substytucji, chcemy upewnić się, że nie zmienimy znaczenia pierwotnego wyrażenia poprzez przypadkowe "przechwycenie" zmiennej, która pierwotnie była wolna.
Zamiana E 'dla X E (napisany [E'/x] e)
Przykład: [y (λx. X)/x] λy. (λx. x) y x
Po zmianie nazwy: [y (λv. v)/x] λz. (λu. u) z x
Po zamianie: λz. (λu. u) z (y (λv. v))
Co naprawdę chcę wiedzieć, dlaczego jest nazywany substytucją unikającą wychwytywania. Mam na myśli koncepcyjnie. – Pradeep
@ Jaguar, czy x jest powiązany (λx. (Γy.yx))? Ponieważ zewnętrzne wyrażenie ma x jako argument. Lub jest powiązany w stosunku do (λx. (Γy.yx)) i wolnego w stosunku do (γy.yx)? –
Zmienna jest przechwycona, jeśli jest umieszczona pod lambdą (lub innymi konstrukcjami wiążącymi, jeśli istnieją), która wiąże zmienną. Nazywa się to podstawieniem unikania przechwytywania, ponieważ proces unika przypadkowego umożliwienia przechwycenia w pierwotnym wyrażeniu wolnych zmiennych w podstawieniu.
Dziękuję bardzo! Znaczenie słowa "chwytanie" nie zostało wyjaśnione w materiałach, które czytałem, co pozostawiło mnie w sprzeczności z intencją. – Paul
@Ord, czy x jest powiązany (λx. (Γy.yx))? Ponieważ zewnętrzne wyrażenie ma x jako argument. Lub jest powiązany w stosunku do (λx. (Γy.yx)) i wolnego w stosunku do (γy.yx)? –
x byłby związany w wyrażeniu (λx. (Γy.yx)) i wolny w wyrażeniu (γy.yx). – Ord