Al leer el cálculo de Lambda en Wiki, se encontró con el término sustituciones que evitan la captura. ¿Puede alguien explicar por qué significa que no pude encontrar una definición desde ningún lugar?¿Qué se entiende por "sustituciones que evitan la captura"?
Gracias
PS
Lo que yo quiero saber es la razón por decir que la operación sustituciones de captura-evitando. Sería de gran ayuda si alguien puede hacer eso
Normalmente, los nombres de las variables específicas que elegimos en el cálculo lambda no tienen sentido - una función de x es lo mismo que una función de a o b o c. En otras palabras:
(. Λx (λy.yx)) es equivalente a - el cambio de nombre a xa y y a b hace no cambio nada (λa (λb.ba).).
De esto, puede concluir que se permite cualquier sustitución, es decir, cualquier variable en cualquier término lambda puede ser reemplazada por cualquier otra. Esto no es asi Considere la lambda interior en la primera expresión anterior:
(λy.yx)
En esta expresión, x es "libre" - no es "obligado" por una abstracción lambda. Si tuviéramos que reemplazar y con x, la expresión se convertiría en:
(λx.xx)
Esto tiene un significado completamente diferente. Ambos x ahora se refieren al argumento de la abstracción lambda. Ese último x (que originalmente era "gratis") ha sido "capturado"; está "atado" por la abstracción lambda.
Las sustituciones que evitan la captura accidental de variables libres se denominan, sin imaginación, "sustituciones que evitan la captura".
Ahora, si todo lo que nos preocupa en el cálculo lambda es sustituir una variable por otra, la vida sería bastante aburrida. De manera más realista, lo que queremos hacer es reemplazar una variable con un término lambda. Así que podríamos reemplazar una variable con una abstracción lambda (λx.t) o una aplicación (x t). En cualquier caso, se aplican las mismas consideraciones: cuando hacemos la sustitución, queremos asegurarnos de que no cambiemos el significado de la expresión original al accidentalmente "capturar" una variable que originalmente era libre.
La sustitución de E 'para x en E (escrito [E'/x] E)
Ejemplo: [(. Λx x) y/x] λy. (λx. x) y x
Después de cambiar el nombre: [y (λv. v)/x] λz. (λu. u) z x
Después de la sustitución: λz. (λu. u) z (y (λv. v))
Lo que realmente quiero saber es por qué se llama sustitución que evita la captura. Me refiero conceptualmente. – Pradeep
@Jaguar, ¿está ligado x en (λx. (Λy.yx))? Porque la expresión externa tiene x como argumento. O está vinculado en relación con (λx. (Λy.yx)) y libre en relación con (λy.yx)? –
Una variable es capturada si está colocada debajo de una lambda (u otras construcciones de enlace si existen) que une la variable. Se llama sustitución que evita la captura porque el proceso evita accidentalmente permitir que las variables libres en la sustitución se capturen dentro de la expresión original.
¡Muchas gracias! La relevancia de la palabra "captura" no se explicaba en los materiales que estaba leyendo, lo que me dejaba sin saber cuál era la intención. – Paul
@Ord, ¿está ligado x en (λx. (Λy.yx))? Porque la expresión externa tiene x como argumento. O está vinculado en relación con (λx. (Λy.yx)) y libre en relación con (λy.yx)? –
x estaría vinculado en la expresión (λx. (Λy.yx)) y libre en la expresión (λy.yx). – Ord