structural:scholar_edition, structural:reformatting, information:highlighting
β-reduction

β-reduction (beta reduction) captures the idea of function application. β-reduction is defined in terms of substitution: the β-reduction of (λ x. M) N is M.

For example, assuming some encoding of 2, 7, ×, we have the following β-reduction: (λ n. n × 2) 7 → 7 × 2.

β-reduction can be seen to be the same as the concept of local reducibility in natural deduction, via the Curry–Howard isomorphism.