10
$\begingroup$

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?

Improve this question
$\endgroup$
4
  • 2
    $\begingroup$ Can you replace the ordinary natural numbers with upper numbers? 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.) $\endgroup$
    – Andrej Bauer
    Commented Jun 20, 2021 at 14:33
  • 1
    $\begingroup$ @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. $\endgroup$
    – helmut
    Commented Jun 20, 2021 at 15:03
  • 1
    $\begingroup$ 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. $\endgroup$
    – Andrej Bauer
    Commented Jun 20, 2021 at 19:41
  • $\begingroup$ Three years after the original question: did you have any progress in this? $\endgroup$
    – paulotorrens
    Commented Jun 23 at 5:50

0

Reset to default

Your Answer

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