Beta-equivalence
From The Twelf Project
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:
![{\; \over (\lambda x{:}A.\, e_1)\ e_2 =_\beta [e_2/x] e_1} \beta](/images/math/9/1/f/91f6d0ebeab42007328993d1ddf11108.png)
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](/images/math/9/6/c/96cf3fc41c93468978ff4242bd4f7d23.png)
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.
