<p>The extended calculus of constructions (ECC) is basically the calculus of constructions with cumulative universes. I use the definition which Zhaohui Luo used in his PhD theses which contained a proof of strong normalization of the calculus.</p>
<p>Unfortunately the strong normalization proof presented in Luo's thesis is not contructive (as far as I understand). It uses the definition of the level of a type which is defined as the lowest universe a type lives in modulo conversion. The definition is classically sound since the universes form a wellorder and therefore a nonempty set of universes must have a least element. However I don't see any possibility to give a constructive definition of the level of a type.</p>
<p>Having no constructive definition of the level of a type, I am not able to make a constructive version of Luo's proof of strong normalisation. This implies to me that I cannot write a type checker for ECC e.g. in Coq without using axioms.</p>
<p>Is this result general? Is it impossible to write a typechecker for ECC in Coq?</p>
<p>This restriction would be rather unfortunate, because it would draw a strict line between the calculus of constructions where the strong normalization can be proved constructively and ECC where no such proof is possible.</p>
<p>Any comments hints on this topic?</p>

CC BY-SA 4.0
2021-06-20T14:33:14.827Z
Can you replace the ordinary natural numbers with [upper numbers](https://twitter.com/andrejbauer/status/1394317732494159874?s=20)? That is, the level of a term $t$ is the set of all $n$ such that $t : U_n$. I uppose then the problem is convincing Coq that upper numbers have a suitable inductive property. But there should be one, at least for monotone predicates, and maybe your predicates are monotone. (I am just shooting in the dark here.)
Andrej Bauer
CC BY-SA 4.0
2021-06-20T15:03:18.723Z
@AndrejBauer: This might be an excellent hint. The set of all universes a type resides in is always upper closed because of cumulativity. Therefore I can use a predicate which describes the set of all universes of a type and use it instead of the level. As far as I know, Luo's proof only uses order expressions on levels which might be replaceable by order expression on predicates as well. I have to look into the details, but is sounds promising.
helmut
CC BY-SA 4.0
2021-06-20T19:41:41.617Z
What bothers me is that I don't see how to derive an induction principle for upper numbers in Coq. You might need something like that somewhere.
Andrej Bauer
CC BY-SA 4.0
2024-06-23T05:50:09.923Z
Three years after the original question: did you have any progress in this?
paulotorrens
<lo.logic><type-theory><dependent-type><typed-lambda-calculus>
Constructive Strong Normalization of the Extended Calculus of Constructions
helmut
# Constructive Strong Normalization of the Extended Calculus of Constructions

(Asked by: username_0 on 2021-06-20)

The extended calculus of constructions (ECC) is basically the calculus of constructions with cumulative universes. I use the definition which Zhaohui Luo used in his PhD theses which contained a proof of strong normalization of the calculus.

Unfortunately the strong normalization proof presented in Luo's thesis is not contructive (as far as I understand). It uses the definition of the level of a type which is defined as the lowest universe a type lives in modulo conversion. The definition is classically sound since the universes form a wellorder and therefore a nonempty set of universes must have a least element. However I don't see any possibility to give a constructive definition of the level of a type.

Having no constructive definition of the level of a type, I am not able to make a constructive version of Luo's proof of strong normalisation. This implies to me that I cannot write a type checker for ECC e.g. in Coq without using axioms.

Is this result general? Is it impossible to write a typechecker for ECC in Coq?

This restriction would be rather unfortunate, because it would draw a strict line between the calculus of constructions where the strong normalization can be proved constructively and ECC where no such proof is possible.

Any comments hints on this topic?

**Tags:** lo.logic, type-theory, dependent-type, typed-lambda-calculus
> **Comments:**
> **username_1**: Can you replace the ordinary natural numbers with [upper numbers](https://twitter.com/andrejbauer/status/1394317732494159874?s=20)? That is, the level of a term $t$ is the set of all $n$ such that $t : U_n$. I uppose then the problem is convincing Coq that upper numbers have a suitable inductive property. But there should be one, at least for monotone predicates, and maybe your predicates are monotone. (I am just shooting in the dark here.)  
> **username_0**: @AndrejBauer: This might be an excellent hint. The set of all universes a type resides in is always upper closed because of cumulativity. Therefore I can use a predicate which describes the set of all universes of a type and use it instead of the level. As far as I know, Luo's proof only uses order expressions on levels which might be replaceable by order expression on predicates as well. I have to look into the details, but is sounds promising.  
> **username_1**: What bothers me is that I don't see how to derive an induction principle for upper numbers in Coq. You might need something like that somewhere.  
> **username_2**: Three years after the original question: did you have any progress in this?  

---

## 0 answers

