<p>You could define a predicate <span class="math-container">$N(t)$</span> whose intuitive meaning is “term <span class="math-container">$t$</span> is in normal form”, and prove a theorem stating that for every closed term <span class="math-container">$t$</span> there is precisely one term <span class="math-container">$t'$</span> such that <span class="math-container">$N(t')$</span> and <span class="math-container">$t \equiv t'$</span>. This way you capture the notion of &quot;normal form&quot;. You cannot really capture the &quot;strong&quot; in &quot;strong normalization&quot; because that specifically refers to sequences of reductions.</p>
<p>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 <em>how</em> is the predicate <span class="math-container">$N$</span> given, precisely. In lucky cases, one can specify <span class="math-container">$N(t)$</span> by a simple syntactic criterion, such as “<span class="math-container">$t$</span> does not contain any redeces“.</p>

CC BY-SA 4.0
2022-09-06T16:34:27.330Z
2022-09-07T07:09:52.000Z
2022-09-07T07:09:52.000Z
Andrej Bauer
<p>In type theory with a type <span class="math-container">$\mathbb{N}$</span> 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 <span class="math-container">$\mathbb{N}$</span> 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).</p>
<p>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 <span class="math-container">$\rhd$</span> in Definition 2.1.2 in <a href="https://era.ed.ac.uk/bitstream/handle/1842/12487/Luo1990.Pdf" rel="nofollow noreferrer">An Extended Calculus of Constructions</a> by Luo.</p>
<p>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?</p>

<type-theory><calculus-of-constructions><normalization>
Defining normalization with respect to judgmental equality instead of reduction
Ilk
# Defining normalization with respect to judgmental equality instead of reduction

(Asked by: username_0 on 2022-09-06)

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](https://era.ed.ac.uk/bitstream/handle/1842/12487/Luo1990.Pdf) 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?

**Tags:** type-theory, calculus-of-constructions, normalization

---

## 1 answers

### Answer by username_1 on 2022-09-06. Score: 5 | Accepted answer

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“.


---

