Problem Detail: In the pure lambda calculus, we have the inductively defined set of terms (the grammar): $$e::= x mid lambda x . e mid e_1 e_2$$ Under the call-by-value evaluation strategy, we have the inference rules for beta-reduction and rules on how to evaluate applications (congruence rules). I am trying to understand how evaluation contexts can replace the congruence rules without actually changing the syntax of the language. Without evaluation contexts, we have the following: $$ frac{e_1 rightarrow e_1′}{e_1e_2 rightarrow e_1’e_2} $$ and $$ frac{e_2 rightarrow e_2′}{ve_2 rightarrow ve_2′}. $$ This makes sense, since if we have an instance of an expression $t = (lambda f . lambda x. f x)((lambda y .y)lambda z .z)lambda w.w$, it is clear that it is of the form $e_1e_2 rightarrow e_1’e_2$ and thus $$(lambda f . lambda x. f x)((lambda y .y)lambda z .z)lambda w.w rightarrow (lambda f . lambda x. f x)(lambda z .z)lambda w.w$$ If we replace the congruence rules with evaluation contexts: $$E::= [cdot] mid Ee mid vE$$ then we need only a single rule to express the congruence rules of the language: $$ frac{e rightarrow e’}{E[e] rightarrow E[e’]}. $$ I am confused as to how evaluation contexts can tell us how to evaluate the expression $t$ from above without changing the syntax of the language. I don’t understand how the evaluation context “works” without rewriting $t$ as $$E_t = (lambda f . lambda x. f x)[cdot]lambda w.w$$ where $t = E_t[((lambda y .y)lambda z .z)]$. There is no obvious a priori reason to evaluate $t$ under call-by-value without knowledge of $E_t$. I really have no idea where I am going wrong. Can someone help correct my thinking?
Asked By : baffld
Answered By : Gilles
The subtlety lies in where the distinction between language and metalanguage is made. As René Magritte put it: 
$(lambda f. lambda x. f x) ((lambda y.y) (lambda z.z)) (lambda w.w)$ is a lambda-term, written in the syntax for lambda-terms. Let’s call this lambda-term $t$. Let $M$ be the lambda-term $(lambda f. lambda x. f x) ((lambda y.y) (lambda z.z))$. I can write $t = M , (lambda w.w)$ (and this is a true equality): all I did was to give a name to a subterm. If you consider the right-hand side of this equality “$M , (lambda w.w)$”, it is not written in the syntax of lambda-terms; it is written in a mathematical notation where we allow a letter to stand for a lambda-term. When we write a rule like $$ frac{e_2 to e_2′}{v , e_2 to v , e_2′} $$ it states the following axiom: for any lambda-terms $e_2$ and $e_2’$ and any value $v$, if $e_2$ reduces to $e_2’$ then $v , e_2$ reduces to $v , e_2’$. Here we’re again using meta-notations (i.e. mathematical notations to reason about a language): the arrow $to$ to express the reduction relation; metavariables where a letter indicates the sort ($e$ for lambda-terms, $v$ for values) and subscripts and primes distinguish between metavariables of the same sort; the fraction notation to write an inductive axiom. When we write the rule $$ frac{e to e’}{E[e] to v E[e’]} $$ then again $E[cdot]$ is a meta-notation, part of the metalanguage and not of the lambda-term syntax. The rule means: for any lambda-terms $e$ and $e’$ and any evaluation context $E[cdot]$, if $e$ reduces to $e’$ then $E[e]$ reduces to $E[e’]$. If we call the context $(lambda f. lambda x. f x)[cdot] (lambda w.w)$ by the (meta-)name $E_t$, then $t = E_t[(lambda y.y)(lambda z.z)]$. Again, this is an equality between two lambda-terms, i.e. the same lambda-term is on both sides of the equal sign. What we have on the left and on the right are two different meta-notations for the same lambda term $(lambda f. lambda x. f x) ((lambda y.y) (lambda z.z)) (lambda w.w)$: one that uses a name that we gave to it, another that’s a bit more complicated involving a context that we gave a name to. Given the term $t$, how do you find how it can reduce?
$(lambda f. lambda x. f x) ((lambda y.y) (lambda z.z)) (lambda w.w)$ is a lambda-term, written in the syntax for lambda-terms. Let’s call this lambda-term $t$. Let $M$ be the lambda-term $(lambda f. lambda x. f x) ((lambda y.y) (lambda z.z))$. I can write $t = M , (lambda w.w)$ (and this is a true equality): all I did was to give a name to a subterm. If you consider the right-hand side of this equality “$M , (lambda w.w)$”, it is not written in the syntax of lambda-terms; it is written in a mathematical notation where we allow a letter to stand for a lambda-term. When we write a rule like $$ frac{e_2 to e_2′}{v , e_2 to v , e_2′} $$ it states the following axiom: for any lambda-terms $e_2$ and $e_2’$ and any value $v$, if $e_2$ reduces to $e_2’$ then $v , e_2$ reduces to $v , e_2’$. Here we’re again using meta-notations (i.e. mathematical notations to reason about a language): the arrow $to$ to express the reduction relation; metavariables where a letter indicates the sort ($e$ for lambda-terms, $v$ for values) and subscripts and primes distinguish between metavariables of the same sort; the fraction notation to write an inductive axiom. When we write the rule $$ frac{e to e’}{E[e] to v E[e’]} $$ then again $E[cdot]$ is a meta-notation, part of the metalanguage and not of the lambda-term syntax. The rule means: for any lambda-terms $e$ and $e’$ and any evaluation context $E[cdot]$, if $e$ reduces to $e’$ then $E[e]$ reduces to $E[e’]$. If we call the context $(lambda f. lambda x. f x)[cdot] (lambda w.w)$ by the (meta-)name $E_t$, then $t = E_t[(lambda y.y)(lambda z.z)]$. Again, this is an equality between two lambda-terms, i.e. the same lambda-term is on both sides of the equal sign. What we have on the left and on the right are two different meta-notations for the same lambda term $(lambda f. lambda x. f x) ((lambda y.y) (lambda z.z)) (lambda w.w)$: one that uses a name that we gave to it, another that’s a bit more complicated involving a context that we gave a name to. Given the term $t$, how do you find how it can reduce?- With the notation using multiple rules, you have to find a deduction tree (in general — here the derivation is linear, so you merely have to find a chain leading to an axiom).
- With the notation using evaluation contexts, you have to find a suitable evaluation context.
The grammar of evaluation context follows the structure of the evaluation rules, so these are in fact not really two methods but two different ways of expressing the same definition. To understand this, I strongly recommend the following exercise: in your favorite language, implement lambda-term call-by-value evaluation in a straightforward way, with a type representing lambda-terms and a function performing one reduction step.
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/22954
