Beta-equivalence

From The Twelf Project
Jump to: navigation, search

Beta-equivalence (β-equivalence) is a notion of proof equivalence in natural deduction logics with introduction and elimination forms. Roughly, it says that when an elimination form is applied to an introduction form, they cancel.

Consider the simply-typed lambda-calculus with arrow types.

The beta-equivalence induced by the arrow type says that the elimination form "cancels" the introduction form ; formally, it is the least congruence relation closed under the axiom:

Beta-equivalence is usually oriented to the right yielding a notion of beta-reduction. For example:

The term on the left-hand side of the axiom is called a beta-redex, and the term on the right-hand side is its beta-reduct. A term with no beta-redexes is called beta-normal. Being beta-normal is one aspect of being canonical.