linguistic:paraphrasing, structural:reformatting
Reduction

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

There are three kinds of reduction:

We also speak of the resulting equivalences: two expressions are α-equivalent, if they can be α-converted into the same expression. β-equivalence 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 β-redex in expressing the substitution of N for x in M. The expression to which a redex reduces is called its reduct; the reduct of (λ x. M) N is M.

If x is not free in M, λ x. M x is also an η-redex, with a reduct of M.