Lambda calculus: difference between contexts and evaluation contexts

Question

Firstly, I'd like to say that my text below may contain errors, so feel free to point out any mistakes in my formulation of the question.

Consider an untyped lambda calculus with booleans and if-statements whose terms are given by this syntax:

 t ::= v | t t | if t t t | x
 v ::= \x.t | #t | #f

Contexts C in this case would be given according to this syntax:

C ::= [-] | \x. C | C t | t C | if C t t | if t C t | if t t C 

Additionally, one could define evaluation contexts E according to this other syntax:

E ::= [-] | \x. E | v E | E t | if E t t 

I split my question in three sub-points which I'd like to be addressed.

1. When are the two notions used? I know for example that evaluation contexts are used to define the semantics of the calculus, but the usage of contexts still somewhat eludes me. Also I'd like some confirmation of my knowledge here.
2. When is one to be preferred to the other and why?
3. Could you point to relevant articles that could help me sort out this matter?

Answer 1

A context is a syntactic notion. A context is a term with one hole in it. (Occasionally there are multi-hole contexts, the definition will be given clearly in that case.) The syntax of contexts is defined by taking the syntax of terms and allowing one subterm to be a hole $[]$ instead of a term. In BNF (I use the lambda-calculus as an example, without booleans and if statements which don't bring anything to the example.): $$ C ::= [] \mid x \mid t \, C \mid C \, t \mid \lambda x.C $$

Together with the definition of a context comes the definition of putting a term in a context. If $C[]$ is a context and $t$ is a term, then $C[t]$ is the term obtained by putting $t$ in the syntax tree where the hole $[]$ is in $C[t]$. This is basically a substitution where the variable is guaranteed to occur exactly once (but note that the “variable” that is substituted is a variable at the meta level, $[]$, not a variable in the lambda-calculus or other language of the terms $t$).

Contexts are used to formulate various definitions in semantics. A common example is that most notions of evaluation involve defining contexts in which evaluation can be performed. For example, consider the lambda-calculus. The fundamental notion of evaluation is given by the beta-reduction rule: $$ (\lambda x. M) \, N \to_\beta M \{x\leftarrow N\} $$ where $M \{x\leftarrow N\}$ is the substitution $x \mapsto N$ applied to $M$.

This isn't the complete definition of beta-reduction: given a term $t$, it can beta-reduce if there are subterms $M$ and $N$ and a variable $x$ such that $t = (\lambda x. M) \, N$; but more generally $t$ can beta-reduce if there is a subterm $t'$ such that $t' = (\lambda x. M) \, N$. Another way to express this is that $t$ can beta-reduce if there is a context $C$ and some terms $M$ and $N$ and a variable $x$ such that $t = C[(\lambda x. M) \, N]$. When there is such a reduction, the right-hand side is $C[M \{x\leftarrow N\}]$. To use a formal notation, beta-reduction is defined by the following deduction rules: $$ \dfrac{}{(\lambda x. M) \, N \to_\beta M \{x\leftarrow N\}} (\beta) \qquad \dfrac{M \to_\beta N}{C[M] \to_\beta C[N]} (\gamma) $$ The same definition can be expressed by making all the kinds of contexts explicit: $$ \dfrac{}{(\lambda x. M) \, N \to_\beta M \{x\leftarrow N\}} (\beta) \\ \dfrac{M \to_\beta N}{\lambda x. M \to_\beta \lambda x. N} (C_\lambda) \qquad \dfrac{M \to_\beta N}{M \, P \to_\beta N \, P} (C_{@\lt}) \qquad \dfrac{M \to_\beta N}{P \, M \to_\beta P \, N} (C_{@\gt}) $$

This definition yields beta-reduction, i.e. a notion of evaluation that allows reducing any subterm. Computations as performed in programming languages often don't allow reducing subterms inside functions: the reduction rule can only be applied at the toplevel, or on the left-hand side or right-hand side of an application. We can express this by defining a new kind of context which does not allow all syntactic forms: $$ D ::= [] \mid x \mid t \, D \mid D \, t $$ We can use this syntax to define the semantic notion of non-partial evaluation: $$ \dfrac{}{(\lambda x. M) \, N \to_{np} M \{x\leftarrow N\}} \qquad \dfrac{M \to_{np} N}{D[M] \to_{np} D[N]} $$ We could also present this definition by expanding it, like we did above for full beta reduction: $$ \dfrac{}{(\lambda x. M) \, N \to_{np} M \{x\leftarrow N\}} (\beta) \\ \dfrac{M \to_{np} N}{M \, P \to_{np} N \, P} (C_{@\lt}) \qquad \dfrac{M \to_{np} N}{P \, M \to_{np} P \, N} (C_{@\gt}) $$ $D$ would be called an evaluation context because it is used to define a notion of evaluation. An evaluation context isn't a special kind of context; rather, calling it an evaluation context is a matter of what the context is used for.

I'll give one more example of context. Let's define values $V$ according to the following syntax: $$ V ::= x V_1 \ldots V_n \mid \lambda x. M $$ Now let's define another kind of contexts: $$ E ::= [] \mid M \, E \mid E \, V $$ Compared with $D$ above, the hole can be on the function side of an application if the argument of the application is a value. Define then the following notion of reduction: $$ \dfrac{}{(\lambda x. M) \, V \to_{cbva} M \{x\leftarrow V\}} (\beta_{cbva}) \qquad \dfrac{M \to_\beta N}{E[M] \to_{cbva} E[N]} (\gamma_{cbva}) $$ With the restriction that the argument of the function must be a value in the first rule and that lambda abstractions are not contexts, we're defining a call-by-value evaluation strategy. With the further restriction that the argument is evaluated before the function, this is applicative order call by value.

Answer 2

Context are used for many purposes, but typically to define congruences on programs. Evaluation contexts are a subset of contexts. They are typically used to define reduction relations. Let me give an example of each.

One formal way of defining program equality is to say two programs $M$ and $N$ are contextually equal they can replace each other in each context without a change of behaviour. We can define this as follows: $M$ and $N$ are contextually equal provided for all closing contexts $C[\cdot]$ for $M$ and $N$: $C[M] \Downarrow t$ if and only if $C[N] \Downarrow t$. We say a context is closing for $M, N$ if neither $C[M]$ nor $C[N]$ have free variables. The expression $M \Downarrow t$ means that the program $M$ reduces in a finite number of steps to the value $t$. (As an aside, note that the definition of contextual equivalence is more involved for rich notions of computation, e.g. concurrent processes.)

In contrast, evaluation contexts are contexts that do not block evaluation. More precisely, an evaluation context is a term with a hole at the point where the next atomic reduction step must take place (or may take place for non-deterministic computation). So the following rule should hold for evaluation contexts: $$ \frac{M \rightarrow N}{E[M] \rightarrow E[N]} $$ As an example of using evaluation contexts, consider the reduction rules for call-by-value $\lambda$-calculus, where we do not reduce under $\lambda$. So even when $M \rightarrow N$, we don't have a reduction $\lambda x.M \rightarrow \lambda x.N$. This can easily be expressed with the general contextual rule above, together with a grammar for evaluation contexts that omits $\lambda$-expressions. Evaluation contexts were first used in The Revised Report On The Syntactic Theories of Sequential Control and State by Felleisen and Hieb.