programming-languages - calculo - lambda calculus tutorial
¿Qué se entiende por "sustituciones que evitan la captura"? (3)
Mientras leía el Cálculo de Lambda en Wiki, apareció el término Sustituciones que evitaban la captura . ¿Alguien puede explicar qué significa? No pude encontrar una definición desde cualquier lugar.
Gracias
PD
Lo que quiero saber es la razón por la que le digo a esa operación que evite las capturas y evite las sustituciones . Sería de gran ayuda si alguien puede hacer eso.
La sustitución de E ''por x en E (escrito [E'' / x] E)
- Paso 1. Renombra las variables enlazadas en E y E ''para que sean únicas
- Paso 2. Realiza la sustitución textual de E ''por x en E
Se llama sustitución evitando capturas .
Ejemplo: [y (λx. X) / x] λy. (λx. x) yx
Después de cambiar el nombre: [y (λv. V) / x] λz. (λu. u) zx
Después de la sustitución: λz. (λu. u) z (y (λv. v))
Se captura una variable si se coloca debajo de una lambda (u otras construcciones de enlace, si existen) que vincula 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.
Normalmente, los nombres de variables específicas que elegimos en el cálculo lambda carecen de significado: 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 (λa. (λb.ba)) - cambiar el nombre de x a a y y to b no cambia nada.
De esto, podría 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 así. Considere la lambda interna en la primera expresión de arriba:
(λy.yx)
En esta expresión, x es "libre", no está "vinculado" por una abstracción lambda. Si reemplazáramos y por x , la expresión sería:
(λx.xx)
Esto tiene un significado totalmente diferente. Ambas x ahora se refieren al argumento de la abstracción lambda. Esa última x (que originalmente era "libre") ha sido "capturada"; está "ligado" por la abstracción lambda.
Las sustituciones que evitan la captura accidental de variables libres se denominan, de forma poco imaginativa, "sustituciones que evitan la captura".
Ahora, si lo único que nos importaba en el cálculo lambda era sustituir una variable por otra, la vida sería bastante aburrida. Más realista, lo que queremos hacer es reemplazar una variable con un término lambda . Entonces podríamos reemplazar una variable con una abstracción lambda (λx.t) o una aplicación (xt). En cualquier caso, se aplican las mismas consideraciones: cuando hacemos la sustitución, queremos asegurarnos de no cambiar el significado de la expresión original al "capturar" accidentalmente una variable que originalmente era libre.