2
$\begingroup$

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?).

Improve this question
$\endgroup$
6
$\begingroup$

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.

Improve this answer
$\endgroup$
4
  • 1
    $\begingroup$ For good entertainment value, extend ETT with the consistent type equality $\mathsf{nat} \to \mathsf{bool} \equiv \mathsf{int} \to \mathsf{nat}$. I think that will also break canonicity, yes? $\endgroup$ – Andrej Bauer Sep 4 '20 at 9:47
  • $\begingroup$ @AndrejBauer I think so. Induction on closed canonical types should imply that $\rightarrow$ is injective on closed arguments. So $\mathsf{nat} \rightarrow \mathsf{bool} \equiv \mathsf{int} \rightarrow \mathsf{nat}$ is incompatible with canonicity. $\endgroup$ – András Kovács Sep 4 '20 at 10:05
  • 1
    $\begingroup$ @AndrejBauer What do you mean by this type equality being consistent? $\endgroup$ – ice1000 Sep 4 '20 at 17:27
  • $\begingroup$ That you cannot use it to inhabit the empty type, or to prove that $0 \equiv 1 : \mathsf{nat}$. $\endgroup$ – Andrej Bauer Sep 4 '20 at 20:01

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.