13
$\begingroup$

I've heard about a folklore claim that

If all terms of ℕ are literals, all closed terms admit canonical form.

In MLTT-style type theories.

I am assured that it's true for Bool if one also assumes consistency, namely the canonicity for empty type. Unfortunately, I don't know much about the general case, and couldn't find references. I suppose that it's related to encoding terms by natural numbers or something similar...

Does anyone know a rigorous formulation or a proof (or a disproof)?

$\endgroup$
5
  • $\begingroup$ Excuse a possibly silly question, but why is the assumption of consistency needed? $\endgroup$ Mar 11, 2022 at 8:18
  • $\begingroup$ What is the precise question here? In MLTT it is true that "if all closed terms of $\mathbb{N}$ have canonical forms then all closed terms have canonical forms" simply because "all closed terms have canonical forms" (for those types that have a reasonable notion of canonicity). Are you asking whether the implication holds more broadly for other type theories? Almost nothing is true more broadly for other type theories, because there are some pretty crazy ones. Please explain the context and the scope of the question a bit more. $\endgroup$ Mar 11, 2022 at 8:21
  • $\begingroup$ While you are at it, what is the canonical form of a term of type $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$? Strong normal form? $\endgroup$ Mar 11, 2022 at 8:21
  • $\begingroup$ @AndrejBauer Ahh... My bad. I don't think consistency is needed. I should have said that consistency is not a corollary of ℕ-canonicity and hence ought to be assumed additionally. $\endgroup$ Mar 12, 2022 at 1:54
  • $\begingroup$ It's vague because I'm not sure how to describe it more precisely. Maybe I should narrow things a bit. It makes more sense to talk about canonical form of an inductive type, so that a term is canonical if it composed solely of constructors and application of constructors. $\endgroup$ Mar 12, 2022 at 1:59

1 Answer 1

19
$\begingroup$

Your question is quite vague, so let me give you both an intuition on why this ought to be true, and a counterexample.

As for intuition, let me show how supposing only canonicity for $\mathbb{N}$ (natural numbers) one can deduce canonicity for $\mathbb{B}$ (booleans). Suppose we are given a closed boolean $\vdash b : \mathbb{B}$, and consider $$\mathtt{if}~b~\mathtt{then}~0~\mathtt{else}~0$$ This is a natural number in the empty context, so it must reduce to a canonical form. But to do so it must be the case that $b$ also reduces to a canonical form, because this is the only way for the $\mathtt{if}$ statement to reduce!

Abstracting a bit, if we can construct a context $\vdash C[\cdot] : T \Rightarrow T'$, that is a term with a hole such that whenever a term $\vdash t : T$ is plugged in said hole the whole term is of type $T'$, and such that $C[t]$ has a canonical form only if $t$ has, then canonicity for $T'$ implies canonicity for $T$.

But there are perfectly valid cases where such a context cannot be built, and this is intentional! My favorite example is the sort of (proof-irrelevant) propositions $\mathtt{SProp}$. As shown in a recent article (and its predecessor), you can prove canonicity for natural numbers in MLTT extended with $\mathtt{SProp}$ without proving canonicity of inhabitants of strict propositions – you only have to assume consistency. The trick is to control the way one can use those to build relevant terms (in our case, natural numbers) so that no context like the above can be built. The idea is roughly to allow for an eliminator from $\mathtt{SProp}$ to $\mathbb{N}$ only for the false proposition. This ensures that a natural number in the empty context cannot be stuck on this eliminator since that would mean that one has an inconsistency in the theory – the term on which the eliminator is applied would be a proof of falsity in the empty context.

$\endgroup$
4
  • $\begingroup$ Nice answer! I have a further question that, for an inductive type T, could one always find 𝐶[⋅]: T ⇒ ℕ that satisfies your condition? If not, what kind of properties have to be imposed on T? $\endgroup$ Mar 12, 2022 at 2:09
  • $\begingroup$ As soon as your inductive type has an eliminator that you are allowed to use to inhabit ℕ, then you can use that eliminator in the same way I used if-then-else, so you should be good. $\endgroup$ Mar 12, 2022 at 15:23
  • $\begingroup$ Yeah. But not so obvious how to do that when the constructors are complicated. $\endgroup$ Mar 12, 2022 at 15:41
  • $\begingroup$ You can always use a constant function in every "branch" as I did in the bool case, no matter how complex the inductive type. In Coq, you would do something like match s return nat with | c _ … _ => 0 | … end, the only issue being the number of underscores. $\endgroup$ Mar 14, 2022 at 7:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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