8
$\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?

$\endgroup$
3
  • 1
    $\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$ Jun 20 at 14:33
  • $\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
    Jun 20 at 15:03
  • $\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$ Jun 20 at 19:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.