In type theory with a type $\mathbb{N}$ of natural numbers (or some other base type such as booleans) and judgmental equality instead of reductions, canonicity is a meta-theoretical statement claiming that a closed term of type $\mathbb{N}$ is judgmentally equal to a unique numeral (and hopefully the metatheory is constructive or proves the existence of untyped lambda calculus expression that computes such a numeral).

Most presentations of strong normalization on the other hand require picking a directed beta reduction relation, not just an undirected judgmental equality, such as the $\rhd$ in Definition 2.1.2 in An Extended Calculus of Constructions by Luo.

Is there an equivalent characterization of strong normalization that can be stated without picking a notion of reduction for CoC in a similar manner to canonicity, i.e. can it be stated purely in terms of seemingly undirected judgmental equality?


1 Answer 1


You could define a predicate $N(t)$ whose intuitive meaning is “term $t$ is in normal form”, and prove a theorem stating that for every closed term $t$ there is precisely one term $t'$ such that $N(t')$ and $t \equiv t'$. This way you capture the notion of "normal form". You cannot really capture the "strong" in "strong normalization" because that specifically refers to sequences of reductions.

Of course, we could just appeal to the axiom of choice and pick one term from each equivalence class, and declare it to be “normal”. The real work begins once we start asking how is the predicate $N$ given, precisely. In lucky cases, one can specify $N(t)$ by a simple syntactic criterion, such as “$t$ does not contain any redeces“.


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.