Untyped Conversion
Untyped conversion (and therefore reduction), I think, is meant to model the implementation of a conversion checker. (Iβm really not the best person to ask.) Ideally, youβd want it to be entirely decoupled from the type checker, which is a very Software Engineering 110 reasonable thing to expect. An implementation outline might look like this:
 Reduce both terms sufficiently.
 If they look different, give up.
 Recur on subterms.
βSufficientlyβ might mean normal form or weak head normal form or whatever reasonable form you like. So we might formalize that as follows:
βββββββββββββββββββββββββ Ξ²
(Ξ»x: Ο. e) e' β³ e[x β¦ e']
ββββββ β³*refl
e β³* e
eβ β³ eβ
eβ β³* eβ
ββββββββ β³*trans
eβ β³* eβ
eα΅’ β³* eα΅’'
βββββββββββββββββββββββ β³*cong
e[x β¦ eα΅’] β³* e[x β¦ eα΅’']
eβ β³* e
eβ β³* e
βββββββ βred
eβ β eβ
The βsufficientlyβ part comes from β³*trans
, where you take as many steps as you need.
The congruence rules are the most tedious, since you need one for every syntactic form,
so Iβve instead lazily written them as a single substitution.
Conversion is an equivalence relation, as youβd expect:
itβs reflexive (by β³*refl
), itβs symmetric (by swapping premises in βred
),
itβs substitutive (by β³*cong
), and itβs transitive if reduction is confluent,
because then you can construct the conversion by where the pairs meet.
(Confluence left as an exercise for the reader.)
eβ β eβ β eβ
\ / \ /
eββ eββ β confluence gives this diamond
\ /
e*
eβ β³* e*
eβ β³* e*
ββββββββ
eβ β eβ
Cumulativity + Ξ·
Dually to Ξ², letβs now add Ξ·contraction, but suppose we had cumulativity
(or more generally, any subtyping relation).
Then Ξ·contraction is no good, since it breaks confluence.
Supposing we had types Ο β€ Ο
, Ξ»x: Ο. (Ξ»y: Ο. f y) x
could either Ξ²reduce to Ξ»x: Ο. f x
,
or Ξ·contract with congruence to Ξ»y: Ο. f y
, but these are no longer Ξ±equivalent due to the type annotation.
Breaking confluence then means breaking transitivity of conversion as well.
Ξ·contraction then isnβt an option with Churchstyle typeannotated intrinsicallytyped terms.
What about Ξ·expansion? If you had a neutral term typed as a function, you may expand it once. But with untyped conversion, thereβs no way to tell whether the term is indeed typed as a function, and you canβt go around Ξ·expanding any old neutral term willynilly.
Ξ·Conversion
The remaining solution is then to add Ξ·equivalence as part of conversion. There are two ways to do this; the first is the obvious way.
ββββββββββββββ βΞ·β (+ βΞ·α΅£ symmetrically)
Ξ»x: Ο. f x β f
This immediately requires explicit transitivity and congruence rules,
since Ξ»x: Ο. Ξ»y: Ο. f x y β f
wouldnβt hold otherwise.
The other way is to check that one side is a function,
then apply the other side.
eβ β³* Ξ»x: Ο. eβ'
eβ β³* eβ'
x β FV(eβ')
eβ' β eβ' x
ββββββββββββββββ βΞ·β (+ βΞ·α΅£ symmetrically)
eβ β eβ
This looks more ideal since it seems like it easily extends the implementation outline:
 Reduce both terms sufficiently.
 If one of them looks like a function, recur according to
βΞ·
.  If they look different, give up.
 Recur on subterms.
You then still need congruence rules for step 4;
otherwise F G β F (Ξ»X: π°. G X)
would not hold given some F: (π° β π°) β π°
and G: π° β π°
.
It seems like transitivity might hold without explicitly adding it as a rule,
again by confluence, but this time requiring induction on derivation heights rather than structural induction,
and first showing that the derivation of any symmetric conversion has the same height.
Multiple Ξ·s
Suppose we were in a setting with multiple syntactic functions, for instance the Calculus of Constructions or System F, where abstraction by and application of a type differs from ordinary term abstractions and applications.
Ξ, x: Ο β’ e: Ο Ξ, Ξ±: β β’ e : Ο
βββββββββββββββββββββββ βββββββββββββββββ
Ξ β’ Ξ»x: Ο. e : Ξ x: Ο. Ο Ξ β’ ΞΞ±. e : βΞ±. Ο
Ξ β’ e : Ξ x: Ο. Ο Ξ β’ e : βΞ±. Ο
Ξ β’ e' : Ο Ξ β’ Ο : β
ββββββββββββββββββββ ββββββββββββββββββββ
Ξ β’ e e' : Ο[x β¦ e'] Ξ β’ e [Ο] : Ο[Ξ± β¦ Ο]
(Ξ»x: Ο. e) e' β³ e[x β¦ e'] (ΞΞ±. e) [Ο] β³ e[Ξ± β¦ Ο]
If both of these functions had Ξ·conversion rules, transitivity wouldnβt hold,
especially for open terms.
Specifically, the conversions Ξ»x: Ο. f x β f
and f β ΞΞ±. f [Ξ±]
are both derivable
(despite being illtyped when considered simultaneously, since conversion is untyped),
but Ξ»x: Ο. f x β ΞΞ±. f [Ξ±]
is impossible to derive.
Equality Reflection + Ξ·
In Ouryβs Extensional Calculus of Constructions^{1},
equality reflection is added to untyped conversion
(β‘
denoting the equality type).
Ξ β’ p: x β‘ y
ββββββββββββ βreflect
Ξ β’ x β y
Thereβs a clash between the fact that illtyped terms can still be convertible,
and that equality reflection only makes sense when everything is welltyped.
In particular, you cannot simultaneously have congruence and transitivity of conversion,
since it allows you to derive an inconsistency.
Concretely, using an illtyped proof of β€ β‘ β₯
(where β€
is trivially inhabited by β
and β₯
is uninhabited),
you can convert from β€
to β₯
.
Β· β’ β€ β (Ξ»p: β€ β‘ β₯. β€) refl (by Ξ²reduction)
β (Ξ»p: β€ β‘ β₯. β₯) refl (by βcong and βreflect on (p: β€ β‘ β₯) β’ p: β€ β‘ β₯)
β β₯ (by Ξ²reduction)
Note the illtypedness of the application:
refl
is clearly not a proof of β€ β‘ β₯
.
Evidently this leads to a contradiction,
since you could then convert the type of β
from β€
to β₯
.
Addendum: What does Coq actually do?
Coqβs conversion algorithm can be found in its kernel,
which is actually one giant algorithm parametrized over whether it should be checking convertibility or cumulativity.
The below is my attempt at writing it down as rules (ignoring cases related to (co)inductives),
with MetaCoqβs conversion in pCuIC as guidance.
[Κ]
represents the relation over which they are parametrized,
which can be either [β]
or [β€]
.
i = j
ββββββββββ βπ°
π°α΅’ [β] π°β±Ό
i β€ j
ββββββββββ β€π°
π°α΅’ [β€] π°β±Ό
Οβ [β] Οβ
Οβ [Κ] Οβ
βββββββββββββββββββββββββ ΚΞ
Ξ x: Οβ. Οβ [Κ] Ξ x: Οβ. Οβ
tβ [Κ] tβ
eβ [β] eβ
βββββββββββββββ Κapp
tβ eβ [Κ] tβ eβ
Οβ [β] Οβ
eβ [Κ] eβ
βββββββββββββββββββββββββ ΚΞ»
Ξ»x: Οβ. eβ [Κ] Ξ»x: Οβ. eβ
Οβ [β] Οβ
tβ [β] tβ
eβ [Κ] eβ
βββββββββββββββββββββββββββββββββββββββββββββ Κlet
let x: Οβ β tβ in eβ [Κ] let x: Οβ β tβ in eβ
eβ [Κ] eβ
βββββββββββββββββββββββ (catchall for remaining syntactic constructs)
t[x β¦ eβ] [Κ] t[x β¦ eβ]
eβ x β³* eβ'
eβ [β] eβ'
ββββββββββββββββ ΚΞ·β
Ξ»x: Ο. eβ [Κ] eβ
eβ x β³* eβ'
eβ' [β] eβ
ββββββββββββββββ ΚΞ·α΅£
eβ [Κ] Ξ»x: Ο. eβ
The βrealβ conversion and subtyping rules are then the confluent closure of the above. The actual implementation performs more reduction as needed; I think this is just for performance reasons, and because thereβs no way to forsee how many steps youβll end up having to take during initial reduction.
eβ β³* eβ'
eβ β³* eβ'
eβ' [β] eβ'
βββββββββββ
eβ β eβ
eβ β³* eβ'
eβ β³* eβ'
eβ' [β€] eβ'
βββββββββββ
eβ β€ eβ
Reflexivity and symmetry of conversion and reflexivity of subtyping are easy to see. Congruence is built into the rules (shown with the same substitution notation as before). Evidently conversion implies subtyping, but this time indirectly.

Nicolas Oury. (TPHOLs 2005). Extensionality in the Calculus of Constructions. α΄ α΄Ιͺ: 10.1007/11541868_18.Β ↩