Llamar por valor en el cálculo lambda

Question

Estoy trabajando en Types and Programming Languages, y Pierce, para la estrategia de reducción de llamadas mediante la llamada, da el ejemplo del término id (id (λz. id z)). El redex interno id (λz. id z) se reduce primero a λz. id z, dando id (λz. id z) como resultado de la primera reducción, antes de que la redex exterior se reduzca a la forma normal λz. id z.

Pero el orden de llamada por valor se define como 'solo se reducen las redex externas', y 'una redex se reduce solamente cuando su lado derecho ya se ha reducido a un valor'. En el ejemplo id (λz. id z) aparece en el lado derecho de la redex exterior y se reduce. ¿Cómo se cuadra esto con la regla de que solo se reducen los redex más externos?

¿La respuesta de que 'más externo' y 'más interno' solo se refiere a abstracciones lambda? Entonces, para un término t en λz. t, t no se puede reducir, pero en un redex s t, t se reduce a un valor v si esto es posible, y luego se reduce s v?

Answer 1

Respuesta corta: sí. Nunca puede reducir dentro de un término lambda, solo puede reducir el término afuera, comenzando por el derecho.

El conjunto de contextos de evaluación en cálculo lambda por valor se define de la siguiente manera:

E = [ ] | (λ.t)E | Et 

E es lo que puede valorar ..

Por ejemplo, en el cálculo lambda por el nombre del contexto de evaluación es :

E = [ ] | Et | fE 

ya que puede reducir una aplicación incluso si un término no es un valor. Por ejemplo (λx.x)(z λx.x) está atrapado en la llamada por valor, pero en la llamada por nombre reduce a (z λx.x), que es una forma normal.
En el contexto gramatical f es una forma normal (durante la llamada por su nombre) definido como:

f = λx.t | L 
L = x | L f 

Se puede ver otra definición de contextos en el capítulo 19.5.3 de la Pierce.

Answer 2

¿Es la respuesta que 'más externo' y 'más interno' solo se refiere a las abstracciones lambda? Entonces para un término t en λz. t, t no se puede reducir, pero en un redex s t, t se reduce a un valor v si esto es posible, y luego s v se reduce?

Sí, eso es exactamente.