10
$\begingroup$

Timany and Sozeau's Predicative Calculus of Cumulative Inductive Constructions (pCuIC) [1] adds extra cumulativity to the inductive types of (Lee and Werner's [2], I think?) pCIC. But what does the "Predicative" part of pCuIC and pCIC refer to? As far as I can tell, people don't seem to distinguish pCIC from CIC (e.g. Ziliani and Sozeau (2017) [3] refer to CIC, not pCIC, for the basis of Coq). Both have an impredicative Prop universe and a predicative universe hierarchy Typeᵢ, so I'm not sure what is or isn't predicative.

[1] https://arxiv.org/abs/1710.03912
[2] https://arxiv.org/abs/1111.0123
[3] https://www.cambridge.org/core/journals/journal-of-functional-programming/article/comprehensible-guide-to-a-new-unifier-for-cic-including-universe-polymorphism-and-overloading/19A095CA0645F89A772B7E2B7B3D92B2

$\endgroup$
1
  • 4
    $\begingroup$ Wow, somehow I never realized that people use CIC to refer to the system with a universe hierarchy. Now I really have no idea what all the names mean... I hope one of the experts can chime in. $\endgroup$ Mar 31, 2022 at 9:04

2 Answers 2

4
$\begingroup$

As far as I know, the "Predicative" part refers to the existence of the type hierarchy. But the CIC/PCIC/PCUIC terminologies are not very fixed, and they can vary quite a lot between article… Some use CIC for "the type theory of Coq" (seems like this is the case of your [3]), while others use it rather for a subset of that (typically a hierarchy of Type + Prop + generic inductive types, but sometimes it omits Prop as well). I think it’s best to not concentrate too much on the names and go have a look at the systems themselves. Although I agree it would be nice to have a clear and reliable terminology!

$\endgroup$
1
  • $\begingroup$ This answer is pragmatic and useful. However, I don't understand why it is accepted since it admittedly does not actually answer the question. Perhaps the OP should wait for a more targeted answer? $\endgroup$ Apr 1, 2022 at 6:15
7
$\begingroup$

As an additional bit of trivia: I found the following in Chapter 4 of the Coq Reference Manual, V8.4:

For Cᴏǫ version V7, this Calculus was known as the Calculus of (Co)Inductive Constructions (Cɪᴄ in short). The underlying calculus of Coq version V8.0 and up is a weaker calculus where the sort Set satisfies predicative rules. We call this calculus the Predicative Calculus of (Co)Inductive Constructions (pCɪᴄ in short).

So it sounds like it's also "predicative" in the sense that the Set universe used to be impredicative (by default!) but isn't anymore.

$\endgroup$

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.