Problema con un lema básico en cálculo Lambda

Question

Tengo algunos problemas graves con el Cálculo Lambda. En una introducción por Barendregt y Barendsen en la página 11 es el siguiente lema, cuya prueba, no estoy de obtener.

$\mathbf{\lambda} \vdash ( \lambda x_1 \dots x_n . M) X_1\dots X_n = M [ x_1 := X_1] \dots [x_n := X_n]$.

Aunque me parece que el resultado intuitivo, de la prueba, que debería ser obvio por inducción y $\beta$-reducción, no está claro. En particular, yo realmente no obtener por qué el orden se conserva en la manipulación, es decir, de la PREPA se obtienen los RHS que $x_1 := X_1$, $x_2 := X_2$, etc (y creo que aquí el orden tiene que ser importante). Tengo la sensación de que este es el síntoma de un profundo malentendido de cómo lambda cálculo de las obras en general.

Cualquier retroalimentación es muy apreciada.
Gracias por su tiempo.

Answer 1

Hay un implícito pero la hipótesis fundamental en el lema citado: las variables $x_1, \dots, x_n$ no son libres en $X_1, \dots, X_n$. Esta es la razón por la que el orden de las sustituciones en la $M[x_1:=X_1]\dots[x_n :=X_n]$ realmente no importa.

Esta hipótesis está implícito en la definición de $\beta$-conversión, porque siempre ha de asumir la variable convenio 2.6 (p. 10):

Si $M_1, \dots, M_n$ se producen en un determinado contexto matemático (por ejemplo, definición, prueba), luego, en estas condiciones todas las variables vinculadas son elegidos para ser diferentes de las variables libres.

Tenga en cuenta que esta variable convención es también crucial en la definición de la sustitución de las abstracciones (p. 10). En efecto, la fijación $$(\lambda y.M)[x := N] \equiv \lambda y. M[x := N]$$ es correcta sólo en el caso de $y$ no es una variable libre en $N$; esta condición puede ser siempre cumplidas por el cambio de nombre de las variables vinculadas ($\lambda$-términos se consideran a a $\alpha$-conversión, es decir, hasta el cambio de nombre de las variables vinculadas). Si la variable de la convención no se cumplieron, que tendría por ejemplo $$(\lambda y. x)[x := y] \equiv \lambda y.y\,,$$ lo cual es claramente incorrecto, en lugar de la correcta $$(\lambda y. x)[x := y] \equiv \lambda z.y\,.$$

Answer 2

Tenga en cuenta que $(\lambda x_1 x_2. M)X_1 X_2$ es en realidad lo siguiente: $$(\lambda x_1 . (\lambda x_2 . M)) X_1 X_2$ $ teniendo en cuenta el segundo $\lambda$ plazo como ser opaco - decir es $Q$ - $(\lambda x_1 . Q) X_1 X_2$, % a $Q[x_1 := X_1] X_2$por $\beta$-reducción.

Ahora sustituye % espalda $Q = \lambda x_2 . M$, así que tenemos % $ $$((\lambda x_2 . M)[x_1 := X_1]) X_2$

Ya que no aparece en la frase '$x_1$' $\lambda x_2$, podemos mover la sustitución dentro del plazo de % de $\lambda$: $$(\lambda x_2 . M[x_1 := X_1]) X_2$ $

Y ahora estamos en condiciones de utilizar la inducción: hemos demostrado que $$(\lambda x_1 x_2 M)X_1 X_2 = (\lambda x_2 . M[x_1 := X_2])X_2$ $ y nosotros sólo podemos seguir adelante de la misma manera.