Lambda calculus: difference between contexts and evaluation contexts

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.

• 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.

• When is one to be preferred to the other and why?

• Could you point to relevant articles that could help me sort out this matter?

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.

StackExchange Computer Science Q#22864, answer score: 15