8
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ Reduction is not a congruence with reduction strategies such as call-by-value. See also here. $\endgroup$ – Martin Berger Mar 23 '14 at 20:31
  • $\begingroup$ I don't understand your answer; your usage of "congruence" as a verb makes no sense to me. I have read the answers in the link you have provided, but I still do not understand why $E$ is presented as a syntactic form, yet it is never actually used in the syntax of the language for which it is defined. $\endgroup$ – baffld Mar 29 '14 at 22:47
  • $\begingroup$ I'm not using congruence as a verb. I don't understand what you mean. E is a meta-variable ranging over evaluation contexts. Evaluations contexts are a proper subset of contexts. Contexts are programs with a hole. $\endgroup$ – Martin Berger Mar 30 '14 at 11:26
8
$\begingroup$

The subtlety lies in where the distinction between language and metalanguage is made. As René Magritte put it:

Ceci n'est pas une pipe.

$(\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.

$\endgroup$
  • 2
    $\begingroup$ In connection with your last paragraph: all logicians and anyone who ever studies syntax should be made to implement substitution. $\endgroup$ – Andrej Bauer Apr 1 '14 at 8:22

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.