Presentation of context rules for the lambda-calculus

Question

Reading Chris Hankin's book, "An Introduction to Lambda Calculus for Computer Scientists", I learnt that the rules for reductions in the pure $\lambda$-Calculus are the $\beta$-reduction rule, $$(\lambda x.M)N = M[x:= N]$$ and also these: $$\frac{M=N}{N=M}$$ $$\frac{M=N}{MZ=NZ}$$ $$\frac{M=N}{ZM=ZN}$$ $$\frac{M=N}{\lambda x.M = \lambda x.N}$$ The author calls this "The Theory $\lambda$"; and although he formally defines contexts, he does not use them there.

Now, some other works -- for example, Didier Rémy's "Type Systems for Programming languages" -- seem to imply that there are only the $\beta$-reduction rule, and a context-rule: $$(\lambda x.a)v \to a[x:= v]$$ $$\frac{a\to a'}{e[a]\to e[a']}$$ Here $e[]$ is an evaluation context, "$a$" is an arbitrary term, and "$v$" is a value (which the author defines to be an abstraction -- variables, he says, are not values).

I am a bit confused. I think (but I'd need confirmation) that they are saying the same thing, but Rémy's approach actually allows for the specification of evaluation strategy (because I can then decide if the context hole will be to the left or to the right, etc), while the presentation by Hankin does not.

Is this correct, or did I completely miss the point?

Answer 1

The two formulations are saying almost the same thing. Hankin's presentation has a symmetry rule ($\frac{M=N}{N=M}$), which is strange: it ends up defining the relation “$M$ reduces to $N$ or $N$ reduces to $M$”. That's unusual; usually, when a relation is written $=$, it's either explicitly defined to be an equivalence relation (with explicit or deducible rules for reflexivity symmetry and transitivity) or implicitly defined as the equivalence induced by the explicitly-given rules.

Giving separate rules for different context forms is equivalent to stating a single context rule and, separately, describing contexts. For example, for the pure lambda calculus, you can have a separate deduction rule for each way to decompose a term syntactically: $$ \frac{M \to N}{M\,Z \to N\,Z} \qquad \frac{M \to N}{Z\,M \to Z\,N} \qquad \frac{M \to N}{\lambda x.M \to \lambda x.N} $$ or you can have a single deduction rule plus a grammatical presentation of contexts: $$ \frac{M \to N}{C[M] \to C[N]} \qquad C ::= [] \mid C Z \mid Z C \mid \lambda x. C $$ (In both cases, that's in addition to the beta rule.)

Other notions of reduction with more restrictive contexts can be expressed in two ways as well. For example, weak head reduction (which forbids reduction under lambda) can be given as the beta rule plus either $$ \frac{M \to_H N}{M\,Z \to_H N\,Z} \qquad \frac{M \to_H N}{Z\,M \to_H Z\,N} $$ or $$ \frac{M \to_H N}{C_H[M] \to_H C_H[N]} \qquad C_H ::= [] \mid C_H Z \mid Z C_H $$

If you're going to manipulate several different notions of reduction, the presentation in terms of contexts is more compact: there's a single context rule, and its formulation is usually obvious so it can be omitted, all that needs to be stated is the permitted contexts if some syntactically valid contexts disallow reduction.

If you're only ever going to use a single notion of reduction, introducing contexts requires some extra syntactic baggage. But this extra baggage has the advantage of making it clearer what's going on: it makes it easier to see where a reduction is happening in a context and where actual computation is happening. So it's a pedagogical trade-off.