There are many different evaluation strategies for the -calculus. The most permissive is full reduction, which allows any redex--i.e., any expression of the form --to step to at any time. It is defined formally by the following small-step operational semantics rules: The call by value (CBV) strategy enforces a more restrictive strategy: it only allows an application to reduce after its argument has been reduced to a value (i.e., a -abstraction) and does not allow evaluation under a . It is described by the following small-step operational semantics rules (here we show a left-to-right version of CBV): Finally, the call by name (CBN) strategy allows an application to reduce even when its argument is not a value but does not allow evaluation under a . It is described by the following small-step operational semantics rules:
Confluence
It is not hard to see that the full reduction strategy is non-deterministic. This raises an interesting question: does the choices made during the evaluation of an expression affect the final result? The answer turns out to be no: full reduction is confluent in the following sense.
Theorem (Confluence). If and then there exists such that and .
Confluence can be depicted graphically as follows:
e *↙ ↘* e1 e2 *↘ ↙* e'
Confluence is often also called the Church–Rosser property.
Substitution
Each of the evaluation relations for -calculus has a defined in terms of a substitution operation on expressions. Because the expressions involved in the substitution may share some variable names (and because we are working up to -equivalence) the definition of this operation is slightly subtle and defining it precisely turns out to be tricker than might first appear.
As a first attempt, consider an obvious (but incorrect) definition of the substitution operator. Here we are substituting for in some other expression: The intuitive idea is that the last rule relies on 𝛼-equivalence to “rewrite” abstractions that use so they do not conflict. Unfortunately, this definition produces the wrong results when we substitute an expression with free variables under a . For example, To fix this problem, we need to revise our definition so that when we substitute under a we do not accidentally bind variables in the expression we are substituting. The following definition correctly implements capture-avoiding substitution: Note that in the case for -abstractions, we require that the bound variable be different from the variable we are substituting for and that not appear in the free variables of , the expression we are substituting. Because we work up to -equivalence, we can always pick to satisfy these side conditions. For example, to calculate we first rewrite to and then apply the substitution, obtaining as the result.
