Lambda Calculus - Reduction

Reduction

The meaning of lambda expressions is defined by how expressions can be reduced.

There are three kinds of reduction:

• α-conversion: changing bound variables;
• β-reduction: applying functions to their arguments;
• η-conversion: which captures a notion of extensionality.

We also speak of the resulting equivalences: two expressions are β-equivalent, if they can be β-converted into the same expression, and α/η-equivalence are defined similarly.

The term redex, short for reducible expression, refers to subterms that can be reduced by one of the reduction rules. For example, (λx.M) N is a beta-redex; if x is not free in M, λx.M x is an eta-redex. The expression to which a redex reduces is called its reduct; using the previous example, the reducts of these expressions are respectively M and M.