nLab eta-conversion

-conversion

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

η\eta-conversion

Idea

In type theory, η\eta-conversion is a conversion rule for “computation” which is “dual” to beta-conversion.

Whereas β\beta-reduction tells us how to simplify a term that involves an eliminator applied to a constructor, η\eta-reduction tells us how to simplify a term that involves a constructor applied to an eliminator.

In contrast to β\beta-reduction, whose “directionality” is universally agreed upon, the directionality of η\eta-conversion is not always the same. Sometimes one may talk about η\eta-reduction, which (usually) simplifies a constructor–eliminator pair by removing it, but we may also talk about η\eta-expansion, which (usually) makes a term more complicated by introducing a constructor–eliminator pair. Although one might expect that of course we always want to use reduction to simplify, it is possible to put bounds on η\eta-expansion, and η\eta-reduction is ill-defined for the unit type (the exception prompting ‘usually’ above).

However, from a category-theoretic POV, it is more natural to consider η\eta to be an expansion, which paired with β\beta as a reduction can be used as a syntax for a lax 2-adjunction (Seely).

The equivalence relation generated by η\eta-reduction/expansion is called η\eta-equivalence, and the whole collection of processes is called η\eta-conversion.

Examples

For function types

The most common example is for a function type ABA \to B.

In this case, the constructor of ABA \to B is a λ\lambda-expression: given a term bb of type BB containing a free variable xx of type AA, then λx.b\lambda x.b is a term of type ABA \to B.

The eliminator of ABA \to B says that given a term ff of type ABA \to B and a term aa of type AA, we can apply ff to aa to obtain a term f(a)f(a) of type BB.

An etaeta-redex? (a term that can be reduced by η\eta-reduction) is then of the form λx.f(x)\lambda x.\, f(x) – the constructor (lambda expression) applied to the eliminator (application). Eta reduction reduces such a redex to the term ff.

Conversely, η\eta-expansion expands any bare function term ff to the form λx.f(x)\lambda x.\, f(x). If η\eta-expansion is applied again to this, we get λx.(λy.f(y))(x)\lambda x.\, (\lambda y.\, f(y))(x), but β\beta-reduction returns this to λx.f(x)\lambda x.\, f(x); therefore, this last form is considered to be fully η\eta-expanded. In general, the rule when applying η\eta-expansion is to use it only when the result is not a β\beta-redex.

For product types

Although function types are the most publicized notion of η\eta-reduction, basically all types in type theory can have a form of it. For instance, in the negative presentation of a product type A×BA \times B, the constructor is an ordered pair (a,b):A×B(a,b)\colon A\times B, while the eliminators are projections π 1\pi_1 and π 2\pi_2 which yield elements of AA or BB.

The η\eta-expansion rule then says that for a term p:A×Bp\colon A\times B, the term (π 1p,π 2p)(\pi_1 p, \pi_2 p) — the constructor applied to the eliminators — is equivalent to pp itself. (Again, we do not repeat the η\eta-expansion, as this would produce a β\beta-redex.) If we use η\eta-reduction instead, then we simplify any subterm of the form (π 1p,π 2p)(\pi_1 p, \pi_2 p) to pp (and leave anything not of that form alone).

For unit types

Above we did a product type with two factors, although it's easy to generalise to any natural number of factors. The case with zero factors is known as the unit type, and η\eta-conversion behaves a bit oddly there; let us examine it.

In the negative presentation of the unit type 11, the constructor is an empty list ():1()\colon 1, while there are no eliminators. The η\eta-expansion rule then says that any term p:1p\colon 1 is equivalent to the term ()() — the constructor applied to no eliminators. In this case, if we repeat the η\eta-expansion, this does not produce a β\beta-redex (indeed, there is no β\beta-reduction for the unit type), but simply makes no change. If we try to apply η\eta-reduction to ()(), then this is ill-defined; we could ‘simplify’ this to any term p:1p\colon 1 that we might be able to construct.

The positive presentation of the unit type does have a well-defined η\eta-reduction, however; see unit type.

Implementation

Eta-reduction/expansion is not as well-behaved formally as beta-reduction, and its introduction can make computational equality undecidable. For this reason and others, it is not always implemented in computer proof assistants.

Coq versions 8.3 and prior do not implement η\eta-equivalence (definitionally), but versions 8.4 and higher do implement it for dependent product types (which include function types). Even in Coq v8.4, η\eta-equivalence is not implemented for other types, such as inductive and coinductive types. This is a good thing for homotopy type theory, since η\eta-equivalence for identity types forces us into set-level type theory.

When η\eta-equivalence is not an implemented as a direct identity, it may be derived for a defined (coarser than identity) equality. For example, if f= ABgf =_{A \to B} g is defined to mean x.f(x)= Bg(x)\forall x.\, f(x) =_B g(x) (where = B=_B is assumed to have been previously defined) and (λx.b)(a)(\lambda x.\, b)(a) is taken to be identical to b[a/x]b[a/x] (implementing β\beta-reduction), then ff and λx.f(x)\lambda x.\, f(x) are provably equal even if not identical. Thus, eta-equivalence for function types follows from function extensionality (relative to any appropriate notion of equality).

Similarly, if “equality” refers to a Martin-Löf identity type in dependent type theory, then a suitable form of η\eta-equivalence is provable for inductively defined types (with β\beta-reduction and a dependent eliminator). This includes the identity types themselves, but this form of η\eta-equivalence does not imply the identity types are valued in propositions because the identity type itself must be incorporated in stating the equivalence. See the next section.

Propositional η\eta-conversion

In dependent type theory, an important role is played by propositional η\eta-conversions which “compute to identities” along constructors. For example, consider binary products with β\beta-reduction, but not (definitional) η\eta-conversion. We say that η\eta-conversion holds propositionally if

  1. For any p:A×Bp\colon A\times B we have a term η p:Id A×B(p,(π 1p,π 2p))\eta_p \colon Id_{A\times B}(p, (\pi_1 p, \pi_2 p)), and

  2. For a:Aa\colon A and b:Bb\colon B we have a definitional equality η (a,b)=1 (a,b)\eta_{(a,b)} = 1_{(a,b)} (where 1 (a,b)1_{(a,b)} denotes the reflexivity constructor of the identity type).

Similar definitions apply for any other type.

The reason this notion is important is that it is “equivalent” to the ability to extend the eliminator of non-dependent type theory to a dependent eliminator, where the type being eliminated into is dependent on the type under consideration.

For instance, in the case of the binary product, suppose that η\eta-conversion holds propositionally as above, and that we have a dependent type z:A×BC(z):Typez\colon A\times B \vdash C(z)\colon Type along with a term x:A,y:Bc(x,y):C((x,y))x\colon A, y\colon B \vdash c(x,y) \colon C((x,y)) defined over the constructor. Then for any p:A×Bp\colon A\times B we can “transport” along η p\eta_p to obtain a term defined over pp, yielding the dependent eliminator. The rule η (a,b)=1 (a,b)\eta_{(a,b)} = 1_{(a,b)} ensures that this dependent eliminator satisfies the appropriate β\beta-reduction rule.

Conversely, if we have a dependent eliminator, then η p\eta_p can be defined by eliminating into the dependent type z:A×Bid A×B(z,(π 1z,π 2z))z\colon A\times B \vdash id_{A\times B}(z,(\pi_1 z, \pi_2 z)), since when zz is (x,y)(x,y) we have 1 (x,y)1_{(x,y)} inhabiting this type.

Note that this “equivalence” is itself only “propositional”, however; if we go back and forth, we should not expect to get literally the same dependent eliminator or propositional η\eta term, only a propositionally-equal one.

The same principle applies to other types, particularly dependent sum types and dependent product types/function types (although the latter are a bit trickier).

References

  • Seely, Modelling computations: a 2-categorical framework, pdf

Last revised on October 2, 2023 at 16:02:12. See the history of this page for a list of all contributions to it.