Beta-equivalence

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.

$A ::= a \mid A_1 \rightarrow A_2$

$e ::= x \mid \lambda x{:}A.\, e \mid e_1\ e_2$

The beta-equivalence induced by the arrow type $A \rightarrow B$ says that the elimination form $e_1\ e_2$ “cancels” the introduction form $\lambda x{:}A.\, e$; formally, it is the least congruence relation $\texttt{}e_1 =_\beta e_2$ closed under the $\texttt{}\beta$ axiom:

${\; \over (\lambda x{:}A.\, e_1)\ e_2 =_\beta [e_2/x] e_1} \beta$

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

$(\lambda x{:}A.\, e_1)\ e_2 \Longrightarrow_\beta [e_2/x] e_1$

The term on the left-hand side of the $\texttt{}\beta$ 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.