Eta-equivalence

From The Twelf Project
Jump to: navigation, search

Eta-equivalence (η-equivalence) is a notion of proof equivalence in natural deduction logics with introduction and elimination forms. Roughly, it says that any proof of a proposition is equivalent to one which introduces the proposition's principal connective. It is a form of extensional equivalence.

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

Eta-equivalence for terms is the least congruence relation closed under the axiom:

In logics and typed calculi, eta-equivalence is usually oriented to the left yielding a notion of eta-expansion. For example:

Eta-expansion transforms an arbitrary proof of a proposition into a proof that introduces the proposition's principal connective. A term with no sub-terms that can be eta-expanded without introducing beta-redexes is said to be eta-long. Being eta-long is one aspect of being canonical.