En el cálculo lambda puro, tenemos el conjunto de términos inductivamente definidos (la gramática):
Bajo la estrategia de evaluación llamada por valor, tenemos las reglas de inferencia para la reducción beta y las reglas sobre cómo evaluar las aplicaciones (reglas de congruencia). Estoy tratando de entender cómo los contextos de evaluación pueden reemplazar las reglas de congruencia sin cambiar realmente la sintaxis del lenguaje. Sin contextos de evaluación, tenemos lo siguiente:
Esto tiene sentido, ya que si tenemos una instancia de una expresión , está claro que es de la forma y por lo tanto
Si reemplazamos las reglas de congruencia con contextos de evaluación: entonces solo necesitamos una sola regla para expresar las reglas de congruencia del lenguaje:
Estoy confundido acerca de cómo los contextos de evaluación pueden decirnos cómo evaluar la expresión desde arriba sin cambiar la sintaxis del lenguaje. No entiendo cómo "funciona" el contexto de evaluación sin reescribir como
donde . No hay una razón obvia a priori para evaluar bajo llamada por valor sin conocimiento de . Realmente no tengo idea de dónde me estoy equivocando. ¿Alguien puede ayudar a corregir mi pensamiento?
Respuestas:
La sutileza reside en dónde se hace la distinción entre lenguaje y metalenguaje. Como lo expresó René Magritte :
Cuando escribimos una regla como establece el siguiente axioma: para cualquier término lambda y y cualquier valor , si se reduce a luego reduce a . Aquí nuevamente estamos usando meta-notaciones (es decir, notaciones matemáticas para razonar sobre un lenguaje): la flecha para expresar la relación de reducción; metavariables donde una letra indica el tipo ( para términos lambda,
Cuando escribimos la regla , nuevamente es una meta-notación, parte del metalenguaje y no del lambda sintaxis a largo plazo. La regla significa: para cualquier término lambda y y cualquier contexto de evaluación , si reduce a entonces reduce a .
Si llamamos al contexto por el (meta-) nombre , entonces . De nuevo, esta es una igualdad entre dos términos lambda, es decir, el mismo término lambda está a ambos lados del signo igual. Lo que tenemos a la izquierda y a la derecha son dos meta-notaciones diferentes para el mismo término lambda : uno que usa un nombre que le dimos, otro que es un poco más complicado e involucra un contexto al que le dimos un nombre.(λf.λx.fx)[⋅](λw.w) Et t=Et[(λy.y)(λz.z)] (λf.λx.fx)((λy.y)(λz.z))(λw.w)
Dado el término , ¿cómo encuentra cómo puede reducirse?t
La gramática del contexto de evaluación sigue la estructura de las reglas de evaluación, por lo que estos no son realmente dos métodos, sino dos formas diferentes de expresar la misma definición.
Para comprender esto, recomiendo encarecidamente el siguiente ejercicio: en su idioma favorito, implemente la evaluación de llamada por valor de término lambda de una manera directa, con un tipo que represente términos lambda y una función que realice un paso de reducción.
fuente