Cálculo de Lambda: diferencia entre contextos y contextos de evaluación

En primer lugar, me gustaría decir que mi texto a continuación puede contener errores, así que siéntase libre de señalar cualquier error en mi formulación de la pregunta.

Considere un cálculo lambda sin tipo con booleanos y sentencias if cuyos términos están dados por esta sintaxis:

 t ::= v | t t | if t t t | x
 v ::= \x.t | #t | #f

Los contextos C en este caso se darían de acuerdo con esta sintaxis:

C ::= [-] | \x. C | C t | t C | if C t t | if t C t | if t t C 

Además, uno podría definir los contextos de evaluación E de acuerdo con esta otra sintaxis:

E ::= [-] | \x. E | v E | E t | if E t t 

Dividí mi pregunta en tres subpuntos que me gustaría abordar.

1. ¿Cuándo se usan las dos nociones? Sé, por ejemplo, que los contextos de evaluación se utilizan para definir la semántica del cálculo, pero el uso de contextos todavía me elude. También me gustaría una confirmación de mi conocimiento aquí.
2. ¿Cuándo se prefiere uno al otro y por qué?
3. ¿Podría señalar artículos relevantes que podrían ayudarme a resolver este asunto?

El contexto se usa para muchos propósitos, pero generalmente para definir congruencias en los programas. Los contextos de evaluación son un subconjunto de contextos. Suelen utilizarse para definir relaciones de reducción. Déjame darte un ejemplo de cada uno.

Una forma formal de definir la igualdad de programas es decir que dos programas y son contextualmente iguales y pueden reemplazarse entre sí en cada contexto sin un cambio de comportamiento. Podemos definir esto de la siguiente manera: y son contextualmente iguales para todos los contextos de cierre para y : si y solo si . Decimos que se está cerrando un contexto para si ni ni tienen variables libres. La expresiónN M N C [ ⋅ ] M N C [ M ] ⇓ t C [ N ] ⇓ t M , N C [ M ] C [ N ] M ⇓ t M $M$$N$$M$$N$$C[\cdot]$$M$$N$$C[M] \Downarrow t$$C[N] \Downarrow t$$M, N$$C[M]$$C[N]$$M \Downarrow t$significa que el programa reduce en un número finito de pasos al valor . (Como comentario aparte, tenga en cuenta que la definición de equivalencia contextual está más involucrada para las nociones ricas de computación, por ejemplo, procesos concurrentes).$M$$t$

En contraste, los contextos de evaluación son contextos que no bloquean la evaluación. Más precisamente, un contexto de evaluación es un término con un agujero en el punto donde debe tener lugar el siguiente paso de reducción atómica (o puede tener lugar para el cálculo no determinista). Por lo tanto, la siguiente regla debe ser válida para los contextos de evaluación: Como ejemplo de uso de contextos de evaluación, considere las reglas de reducción para call-by-value -cálculo, donde no reducimos bajo . Entonces, incluso cuando , no tenemos una reducción λλM→Nλx. M→λx. N

$$\frac{M \rightarrow N}{E[M] \rightarrow E[N]}$$ $\lambda$$\lambda$$M \rightarrow N$$\lambda x.M \rightarrow \lambda x.N$. Esto se puede expresar fácilmente con la regla contextual general anterior, junto con una gramática para contextos de evaluación que omite -expressions. Los contextos de evaluación se utilizaron por primera vez en el Informe revisado sobre las teorías sintácticas del control secuencial y el estado por Felleisen y Hieb.$\lambda$

Un contexto es una noción sintáctica. Un contexto es un término con un agujero en él. (Ocasionalmente hay contextos de múltiples agujeros, la definición se dará claramente en ese caso.) La sintaxis de los contextos se define tomando la sintaxis de los términos y permitiendo que un subterráneo sea un agujero lugar de un término. En BNF (uso el cálculo lambda como ejemplo, sin booleanos y sentencias if que no aportan nada al ejemplo): $[]$

$$C ::= [] \mid x \mid t \, C \mid C \, t \mid \lambda x.C$$

Junto con la definición de un contexto viene la definición de poner un término en un contexto. Si es un contexto y es un término, entonces es el término obtenido al poner en el árbol de sintaxis donde el agujero está en . Esto es básicamente una sustitución en la que se garantiza que la variable ocurra exactamente una vez (pero tenga en cuenta que la "variable" que se sustituye es una variable en el nivel meta, , no una variable en el cálculo lambda u otro lenguaje de los términos ).$C[]$$t$$C[t]$$t$$[]$$C[t]$$[]$$t$

Los contextos se utilizan para formular varias definiciones en semántica. Un ejemplo común es que la mayoría de las nociones de evaluación implican la definición de contextos en los que se puede realizar la evaluación. Por ejemplo, considere el cálculo lambda. La noción fundamental de evaluación viene dada por la regla de reducción beta: donde es la sustitución aplicada a .

$$(\lambda x. M) \, N \to_\beta M \{x\leftarrow N\}$$ $M \{x\leftarrow N\}$$x \mapsto N$$M$

Esta no es la definición completa de reducción beta: dado un término , puede reducir beta si hay subterms y y una variable tal que ; pero más generalmente puede beta-reducir si hay un subtérmino de tal manera que . Otra forma de expresar esto es que puede reducir beta si hay un contexto y algunos términos y y una variable tal que$t$$M$$N$$x$$t = (\lambda x. M) \, N$$t$$t'$$t' = (\lambda x. M) \, N$$t$$C$$M$$N$$x$$t = C[(\lambda x. M) \, N]$. Cuando existe tal reducción, el lado derecho es . Para usar una notación formal, la reducción beta se define mediante las siguientes reglas de deducción: La misma definición puede expresarse haciendo explícitos todos los tipos de contextos: $C[M \{x\leftarrow N\}]$

$$\dfrac{}{(\lambda x. M) \, N \to_\beta M \{x\leftarrow N\}} (\beta) \qquad \dfrac{M \to_\beta N}{C[M] \to_\beta C[N]} (\gamma)$$ $$\dfrac{}{(\lambda x. M) \, N \to_\beta M \{x\leftarrow N\}} (\beta) \\ \dfrac{M \to_\beta N}{\lambda x. M \to_\beta \lambda x. N} (C_\lambda) \qquad \dfrac{M \to_\beta N}{M \, P \to_\beta N \, P} (C_{@\lt}) \qquad \dfrac{M \to_\beta N}{P \, M \to_\beta P \, N} (C_{@\gt})$$

Esta definición produce una reducción beta, es decir, una noción de evaluación que permite reducir cualquier subterráneo. Los cálculos realizados en lenguajes de programación a menudo no permiten la reducción de subterms dentro de las funciones: la regla de reducción solo se puede aplicar en el nivel superior, o en el lado izquierdo o derecho de una aplicación. Podemos expresar esto definiendo un nuevo tipo de contexto que no permita todas las formas sintácticas: Podemos usar esta sintaxis para definir la noción semántica de evaluación no parcial: También podríamos presentar esta definición expandiéndola, como hicimos anteriormente para la reducción beta completa:

$$D ::= [] \mid x \mid t \, D \mid D \, t$$ $$\dfrac{}{(\lambda x. M) \, N \to_{np} M \{x\leftarrow N\}} \qquad \dfrac{M \to_{np} N}{D[M] \to_{np} D[N]}$$ $$\dfrac{}{(\lambda x. M) \, N \to_{np} M \{x\leftarrow N\}} (\beta) \\ \dfrac{M \to_{np} N}{M \, P \to_{np} N \, P} (C_{@\lt}) \qquad \dfrac{M \to_{np} N}{P \, M \to_{np} P \, N} (C_{@\gt})$$ $D$ se llamaría contexto de evaluación porque se utiliza para definir una noción de evaluación. Un contexto de evaluación no es un tipo especial de contexto; más bien, llamarlo contexto de evaluación es una cuestión de para qué se utiliza el contexto .

Daré un ejemplo más de contexto. Definamos los valores acuerdo con la siguiente sintaxis: Ahora definamos otro tipo de contextos: Comparado con arriba, el agujero puede estar en el lado de la función de una aplicación si el argumento de la aplicación es un valor. Defina entonces la siguiente noción de reducción: $V$

$$V ::= x V_1 \ldots V_n \mid \lambda x. M$$ $$E ::= [] \mid M \, E \mid E \, V$$ $D$ $$\dfrac{}{(\lambda x. M) \, V \to_{cbva} M \{x\leftarrow V\}} (\beta_{cbva}) \qquad \dfrac{M \to_\beta N}{E[M] \to_{cbva} E[N]} (\gamma_{cbva})$$ Con la restricción de que el argumento de la función debe ser un valor en la primera regla y que las abstracciones lambda no son contextos, estamos definiendo una estrategia de evaluación llamada por valor. Con la restricción adicional de que el argumento se evalúa antes de la función, esta es una llamada de orden aplicativo por valor.