Does canonicity imply weak normalization?

Question

Context: type theory.

My understanding of:

• WN: every term can rewrite to NF.
• Canonicity: every term rewrites into canonical form.

Then it leads to an intuition where if canonicity holds, then we get NF = canonical form and therefore WN holds. However, I don't see people state this often, like this question talks about canonicity but never mentions NF or normalization. On nLab, canonical form is said to be normal form, which justifies my "NF = canonical form" guess but it doesn't say WN therefore holds. Therefore I'm doubting my intuition.

So, I wonder if it's right (is there a proof?), or if it's wrong (is there a counterexample?).

Answer 1

Canonicity does not imply weak normalization. First, let me phrase the involved definitions more precisely:

• WN: every open term is reducible to a normal term
• Canonicity: every closed term is reducible to a canonical term

(Note: in modern metatheory of type theory, it is more common to talk about conversion instead of reduction, and likewise to talk about unique existence of normal forms instead of weak/strong normalization. This answer remains valid if we replace "reducible" above with "convertible").

Normal and canonical terms are not the same. For example, the x variable in x : Bool context is normal but not canonical. Also, the closed term λ(b : Bool). if true then b else b is canonical but not normal.

Extensional type theory has the canonicity property but not WN, SN, or unique existence of normal forms. That's because in ETT it is possible to add an inconsistent definitional equality to the context, or add an equational theory of a Turing-complete system. For example, in the ETT context n : Nat, p : n = suc n the n variable has no unique normal form, since n can be expanded arbitrarily using p.

However, if we have a closed ETT term, we can't have anything dodgy in the context, so a closed term can be still evaluated to a canonical form.