## 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 Church-style type-annotated intrinsically-typed 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 willy-nilly.

## Ξ·-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 ill-typed 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 [2],
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 ill-typed terms can still be convertible,
and that equality reflection only makes sense when everything is well-typed.
In particular, you cannot simultaneously have congruence and transitivity of conversion,
since it allows you to derive an inconsistency.
Concretely, using an ill-typed 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 ill-typedness 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β
βββββββββββββββββββββββ (catch-all 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.

## References

[1] McBride, Conor. (9 January 2015). *universe hierarchies*. α΄ΚΚ:https://pigworker.wordpress.com/2015/01/09/universe-hierarchies/.

[2] Oury, Nicolas. (TPHOLs 2005). *Extensionality in the Calculus of Constructions*. α΄
α΄Ιͺ:10.1007/11541868_18.