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

12

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?

fuente

Respuestas:

15

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 tMNMNC[]MNC[M]tC[N]tM,NC[M]C[N]Mtsignifica 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).Mt

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 λλMNλx. Mλx. Nλ

MNE[M]E[N]
λλMNλx.Mλ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.λ
Martin Berger
fuente
14

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::=[]xtCCtλ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[]tC[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 .

(λx.M)NβM{xN}
M{xN}xNM

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 quetMNxt=(λx.M)Nttt=(λx.M)NtCMNxt=C[(λ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{xN}]

(λx.M)NβM{xN}(β)MβNC[M]βC[N](γ)
(λx.M)NβM{xN}(β)MβNλx.Mβλx.N(Cλ)MβNMPβNP(C@<)MβNPMβPN(C@>)

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::=[]xtDDt
(λx.M)NnpM{xN}MnpND[M]npD[N]
(λx.M)NnpM{xN}(β)MnpNMPnpNP(C@<)MnpNPMnpPN(C@>)
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::=xV1Vnλx.M
E::=[]MEEV
D
(λx.M)VcbvaM{xV}(βcbva)MβNE[M]cbvaE[N](γ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.
Gilles 'SO- deja de ser malvado'
fuente
1
Su última definición de contextos de evaluación está más cerca de la noción original de Felleisen y Hieb. Son un medio sintáctico para ayudar a expresar el orden de evaluación de los términos de un cálculo. Un contexto de evaluación es un tipo especial de contexto, ya que permite factorizar un término de forma única en un contexto y una redex (cuando sea posible), indicando de manera determinista dónde debe ocurrir el siguiente paso de reducción.
Dave Clarke
@DaveClarke Como un aparte, también puede usar contextos de evaluación para definir la evaluación de nociones de cálculo no deterministas, donde no tiene una descomposición única en contexto de evaluación y redex.
Martin Berger
@ MartinBerger: De hecho.
Dave Clarke
@DaveClarke ¿Quiere decir que "un contexto de evaluación determinista es un tipo especial de contexto"? Puedo tomar un conjunto arbitrario de contextos y definir una estrategia de evaluación basada en él.
Gilles 'SO- deja de ser malvado'
@Gilles: Los contextos de evaluación pueden definir una estrategia de reducción determinista. No creo haber visto la frase "contexto de evaluación determinista". Por supuesto, son un tipo especial de contexto. Estoy de acuerdo con tu comentario; el punto es más que su respuesta pierde el significado histórico de los contextos de evaluación, que fue definir una noción determinista de reducción.
Dave Clarke