Theoretical Computer Science
- type-theory calculus-of-constructions normalization
- Updated Fri, 07 Oct 2022 10:45:18 GMT
-
Defining normalization with respect to judgmental equality instead of reduction
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?
Solution
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.
External Links
External links referenced by this document: