Durante la lettura del Lambda Calculus in Wiki, si è imbattuto nel termine Sostituzioni da evitare acquisizioni. Qualcuno può spiegare cosa significa perché non sono riuscito a trovare una definizione da nessuna parte.Cosa si intende per "sostituzioni per evitare le catture"?
Grazie
PS
Quello che voglio sapere è la ragione per raccontare che il funzionamento cattura-evitando sostituzioni. Sarebbe di grande aiuto se qualcuno può farlo
Normalmente, i nomi delle variabili specifiche che abbiamo scelto nel lambda calcolo sono prive di significato - in funzione della x è la stessa cosa in funzione di a o b o c. In altre parole:
(. Λx (λy.yx)) è equivalente a - rinominare x-a e y-b fa non cambiato qualcosa (λa (λb.ba).).
Da ciò si può concludere che è consentita qualsiasi sostituzione, ad esempio qualsiasi variabile in qualsiasi termine lambda può essere sostituita da qualsiasi altra. Non è così. Si consideri il lambda interno nella prima espressione sopra:
(λy.yx)
In questa espressione, x è "libero" - non è "legato" da un astrazione lambda. Se dovessimo sostituire y con x, l'espressione sarebbe diventato:
(λx.xx)
Questo ha un significato del tutto diverso. Entrambe le versioni x si riferiscono ora all'argomento dell'astrazione lambda. L'ultimo x (che in origine era "gratuito") è stato "catturato"; è "vincolato" dall'astrazione lambda.
Sostituzioni che evitano accidentalmente cattura variabili libere sono chiamati, unimaginatively, "sostituzioni di cattura-evitando."
Ora, se tutto ciò che importava in lambda calcolo stava sostituendo una variabile per un altro, la vita sarebbe piuttosto noioso. Più realisticamente, ciò che vogliamo fare è sostituire una variabile con un termine lambda . Così potremmo sostituire una variabile con un'astrazione lambda (λx.t) o un applicazione (x t). In entrambi i casi, valgono le stesse considerazioni: quando facciamo la sostituzione, vogliamo assicurarci di non modificare il significato dell'espressione originale accidentalmente "catturando" una variabile che era originariamente libera.
La sostituzione di E 'per x in E (scritto [E'/x] E)
Esempio: [(. Λx x) y/x] λy. (λx. x) y x
Dopo la ridenominazione: [y (λv. v)/x] λz. (λu. u) z x
Dopo la sostituzione: λz. (λu. u) z (y (λv. v))
Quello che voglio davvero sapere è il motivo per cui si chiama sostituzione evitabile. Intendo concettualmente – Pradeep
@Jaguar, x è vincolato in (λx. (Λy.yx))? Perché l'espressione esterna ha x come argomento. O è legato in relazione a (λx (λy.yx)) e libero in relazione a (λy.yx)? –
Una variabile è catturata se è posizionata sotto una lambda (o altri costrutti vincolanti se esistenti) che lega la variabile. Si chiama sostituzione evitando l'acquisizione perché il processo evita accidentalmente consentendo di catturare variabili libere nella sostituzione all'interno dell'espressione originale.
Grazie mille! La rilevanza della parola "cattura" non è stata spiegata nei materiali che stavo leggendo, il che mi ha lasciato in perdita per quale fosse l'intenzione. – Paul
@Ord, x è associato a (λx. (Λy.yx))? Perché l'espressione esterna ha x come argomento. O è legato in relazione a (λx (λy.yx)) e libero in relazione a (λy.yx)? –
x sarebbe legato nell'espressione (λx. (Λy.yx)) e libero nell'espressione (λy.yx). – Ord