Stream: Miscellaneous

Topic: Official name of Coq's type theory

Yannick Forster (Apr 08 2021 at 09:16):

Related to the other discussion, but in a very different spirit I tried to pinpoint what the name of the type theory Coq implements is. One could for instance see Gallina as the short name for Coq's type theory. The reference manual says The underlying formal language of Coq is a Calculus of Inductive Constructions (CIC) (https://coq.github.io/doc/v8.13/refman/language/cic.html) and The logical language used by Coq is a variety of type theory, called the Calculus of Inductive Constructions. (https://coq.github.io/doc/v8.13/refman/history.html)/ The Coq Coq Correct paper says the Polymorphic, Cumulative Calculus of Inductive Constructions (PCUIC) at the basis of Coq (https://dl.acm.org/doi/pdf/10.1145/3371076). And then there's Amin's and Matthieu's paper Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC) (https://arxiv.org/abs/1710.03912),

Depending on whether people think that Coq's type theory has a name and what it is, one way for the other problem could be to (re)name Coq's type theory, keep coq for the implementation, and refer to the whole project via the type theory's name. But for now I'm interested in opinions what the official name of Coq's type theory is.

Matthieu Sozeau (Apr 08 2021 at 09:18):

Yeah, its complicated. Right now if we put all adjectives together we get "Polymorphic Predicative Calculus of Cumulative Inductive Constructions"

Kenji Maillard (Apr 08 2021 at 09:19):

predicative being extremely deceptive here

Matthieu Sozeau (Apr 08 2021 at 09:19):

Yes :)

Matthieu Sozeau (Apr 08 2021 at 09:20):

And if we look to the future, with sort polymorphism it certainly wouldn't make sense to keep it in the name

Matthieu Sozeau (Apr 08 2021 at 09:20):

But you're right, we already have Prop which is a distinguishing feature

Théo Winterhalter (Apr 08 2021 at 09:20):

We probably want a name for the theory that doesn't change when we extend it.

Matthieu Sozeau (Apr 08 2021 at 09:21):

And if forgot that some papers use (Co)-Inductive too, so "Calculus of Cumulative (Co)-Inductive Constructions". That's a lot of C's

Théo Winterhalter (Apr 08 2021 at 09:22):

$C^\omega_\omega$

Kenji Maillard (Apr 08 2021 at 09:23):

$C\omega C\omega$ could be pronounced koko

Gaëtan Gilbert (Apr 08 2021 at 09:23):

something about primitive records too, or is that counted in inductive constructions?
also the module system

Matthieu Sozeau (Apr 08 2021 at 09:24):

or "Polymorphic Calculus of Cumulative (Co)-Inductive Constructions" a.k.a. "PoCaCuICo"

Matthieu Sozeau (Apr 08 2021 at 09:25):

We usually don't see the module system as part of the core calculus but it's true it's another defining feature of Coq

Enrico Tassi (Apr 08 2021 at 09:28):

"PoCaCuICo"

with some more effort you can get to Acapulco, and have a drink ;-)

Théo Zimmermann (Apr 08 2021 at 09:49):

I was never so fan of the pCuIC at al. attempts at modifying the name to properly encompass what is contained in the theory. I think we should stick to calling the current (evolving) theory CIC and this is what the refman does.

Matthieu Sozeau (Apr 08 2021 at 09:52):

Yes, I agree with that, it's too technical for a software name

Yannick Forster (Apr 08 2021 at 09:53):

Then maybe the sentence in cic.rst should be changed to The underlying formal language of Coq is _the_ Calculus of Inductive Constructions (CIC)?

Matthieu Sozeau (Apr 08 2021 at 09:59):

Well, I agree with the idea to use CIC for short reference, but ideally the refman should reflect the precise theory that is implemented, so PCCuIC, and my (dream?) plan is to update it once we have the Coq proofs finished in MetaCoq for the core calculus :)

Kenji Maillard (Apr 08 2021 at 10:05):

Is it really needed/useful to have an accronym for the "exact/precise" content of the type theory implemented by Coq ? I expect that it any such acronym will anyway need to be accompanied by at least a large paragraph, probably rather a full paper to be intelligible, and will quickly be out of date. Wouldn't it be easier to just say the type theory underlying Coq ? (and if you really want a short way to name it, just say CoqTT ?)

Théo Winterhalter (Apr 08 2021 at 10:07):

It seems Agda just says "an extension of MLTT" in comparison.

Enrico Tassi (Apr 08 2021 at 10:10):

This thread reminds of the famous "lambda bar mu mu-tilde"

Meven Lennon-Bertrand (Apr 08 2021 at 10:11):

It wouldn’t hurt to have a thing like CoqTT or something along these lines, that clearly means "the exact type theory of Coq" (and hopefully with MetaCoq as a reference in the not-so-distant future). You could even say CoqTT x.y to refer to the type theory described in MetaCoq version x.y if the theory is going to evolve in time. And then say that this is an extension of CIC with a paragraph long of features.

Enrico Tassi (Apr 08 2021 at 10:11):

Not so sure that catenating all language features leads to something readable

Yannick Forster (Apr 08 2021 at 10:11):

I have been saying "Coq's type theory" in the title of papers. Now I need to pick a title for my thesis, and of course I can use this strategy again. But then we're back to the problem that for outsiders, this title will sound strange, and if I can replace "Coq's type theory" by a correct, non-misleading name that would be great

Yannick Forster (Apr 08 2021 at 10:12):

It might be nice to consider "the Calculus of Inductive Constructions" the current theory underlying Coq, and not a historical thing. Then Coq's type theory becomes exactly CIC, not CIC plus a paragraph, and not some acronym with CIC as substring

Matthieu Sozeau (Apr 08 2021 at 10:13):

I'm not saying the refman should use a "PoCaCuiCo"-like shorthand, just that the exact theory should be in the refman, even if we refer to it as "a variant/extension of CIC"

Meven Lennon-Bertrand (Apr 08 2021 at 10:15):

I’m not sure CIC is such a good name, for me it’s more of an umbrella name like MLTT, and it seems to me that restricting it to mean "the theory of Coq" might cause confusion with people using it in other contexts.

Pierre-Marie Pédrot (Apr 08 2021 at 10:16):

Historically, it seems that the main point of perceived divergence between CIC and MLTT was pattern-matching vs combinators. Not sure if that relevant anymore.

Matthieu Sozeau (Apr 08 2021 at 10:16):

@Meven That's right, so we need another new name :) (I have to stop using internet for a while and actually do some work, though :))

Enrico Tassi (Apr 08 2021 at 10:17):

Pierre-Marie Pédrot said:

Historically, it seems that the main point of perceived divergence between CIC and MLTT was pattern-matching vs combinators. Not sure if that relevant anymore.

Prop?

Meven Lennon-Bertrand (Apr 08 2021 at 10:17):

Wasn’t Prop another major difference? But also not that relevant anymore

Enrico Tassi (Apr 08 2021 at 10:18):

An impredicative sort is a relevant difference

Yannick Forster (Apr 08 2021 at 10:19):

From my perspective, it's still an option to call Coq's type theory Gallina. I don't see reasons in having a naming-difference in the programming language and it's type theory, but I have not though about it for a long time

Dan Frumin (Apr 08 2021 at 10:57):

Meven Lennon-Bertrand said:

Wasn’t Prop another major difference? But also not that relevant anymore

Why is it not relevant anymore?

Théo Winterhalter (Apr 08 2021 at 11:10):

I think Meven was referring to the fact that Agda now has Prop (corresponding to Coq's SProp) too.

Gaëtan Gilbert (Apr 08 2021 at 11:12):

IIRC it's a predicative version (so there's Prop@{i} next to Type@{i})

Théo Winterhalter (Apr 08 2021 at 11:14):

Gaëtan Gilbert said:

IIRC it's a predicative version (so there's Prop@{i} next to Type@{i})

Yes.

Meven Lennon-Bertrand (Apr 08 2021 at 11:25):

I was thinking about the fact that in general the universe hierarchies are much richer and flexible in both Agda and Coq than they used to be, and this seems to be a general direction. But it’s still quite a difference to have an impredicative universe, I agree

Dan Frumin (Apr 08 2021 at 12:56):

Thanks for clarifying.

Matthieu Sozeau (Apr 08 2021 at 13:32):

@Yannick Forster its just that you might want to distinguish the source/surface and target/kernel languages, as in Gallina and Gallina-Core

Yannick Forster (Apr 08 2021 at 13:44):

Right, thanks Matthieu, I didn't consider that. Gallina-Core would be the type theory, and that's again not really a nice and catchy name :/

Yannick Forster (Apr 08 2021 at 13:45):

Then I'm personally undecided again between @Théo Zimmermann 's suggestion to consider CIC always to be the current type theory underlying Coq and the suggestion that a new, catchy name is needed for the tip of the CIC+X evolvement tree (while CIC stays the name of the theory it was in the 90s)

Matthieu Sozeau (Apr 08 2021 at 13:48):

Imagine in two years when we have sort polymorphism and setoid type theory, and rewrite rules, and ... we should be looking for a quite generic name

Michael Soegtrop (Apr 08 2021 at 13:50):

How about SATT for "State of the Art Type Theory" :-)

Cody Roux (Apr 08 2021 at 13:58):

Matthieu Sozeau said:

We usually don't see the module system as part of the core calculus but it's true it's another defining feature of Coq

Sadly

Paolo Giarrusso (Apr 09 2021 at 01:55):

Re MLTT vs CIC, “typed vs untyped equality” seemed the 2nd major difference after Prop, even if it’s mostly type theorists who care about this one (while Prop is much more visible)

Li-yao (Apr 09 2021 at 02:19):

What is the distinction between Gallina and CIC/Coq's type theory?

Xuanrui Qi (Apr 09 2021 at 07:02):

Gallina is a programming language that contains many features (module system, type classes) that IIRC do not strengthen the type theory?
In other words, the type theory is the "core" of Gallina?

Meven Lennon-Bertrand (Apr 09 2021 at 07:34):

You can also add existential variables (or anything related to unification) I guess. I’d say Gallina is the user-level programming language, while when we talk about the type theory I think we rather refer to what the kernel implements – a fragment of Gallina to which all Gallina programs are eventually elaborated.

Kenji Maillard (Apr 09 2021 at 07:34):

Typed vs untyped equality is also due to the choice of presentation for the type theory: the PTS approach favored by people working around Coq's type theory is "untyped" (the conversion is derived from a rewriting system on bare terms) whereas the logical framework approach often taken in presentations of MLTT is typed "by design". There are a few papers (by H. Herbelin & V. Siles, H. Geuvers...) showing that the two approaches are not too far apart (even though the latter approach can be extended with type-directed equations that can't be captured by the former).

Talia Ringer (Apr 09 2021 at 23:40):

Is there a good source on the differences between CIC omega and Gallina? Would be nice to cite in my thesis on the chapter I'm currently writing, while I'm here :)

Théo Zimmermann (Apr 10 2021 at 16:46):

No idea if there is a good source, but FWIW, with the new organization of the refman, we tried to more systematically separate what is implemented in the kernel in the Core language chapter from what is only surface language in the Language extensions chapter.

Tadeusz Litak (Apr 11 2021 at 08:32):

Do all these subsequent extensions have any influence on the consistency strength? The first item here

https://github.com/coq/coq/wiki/Presentation#what-do-i-have-to-trust-when-i-see-a-proof-checked-by-coq

says that that "the theory of Coq version 8.9 is generally admitted to be consistent wrt Zermelo-Fraenkel set theory + inaccessible cardinals". "Generally admitted" reads a bit like a weasel word, but I assume there is much more specific meaning behind it. Still, is it known what kind of inaccessible cardinals we are talking about? And are those inaccessible cardinals in question the same for Coq 8.13.1?

Paolo Giarrusso (Apr 11 2021 at 11:54):

@Tadeusz Litak https://arxiv.org/abs/1710.03912 and https://www.irif.fr/~sozeau//research/publications/drafts/Coq_Coq_Correct.pdf seem potentially relevant; the first is about the consistency of the core theory, and the 2nd is about going from the theory to Coq.

Paolo Giarrusso (Apr 11 2021 at 11:57):

(the first paper gives a model in ZFC, not ZF, but ZFC and ZF are equiconsistent)

Tadeusz Litak (Apr 11 2021 at 14:44):

Paolo Giarrusso said:

(the first paper gives a model in ZFC, not ZF, but ZFC and ZF are equiconsistent)

Thanks. Both papers look very interesting. The first one is probably the most relevant to the question. Section 3 says what is assumed on top of ZFC: "a countably infinite strictly increasing hierarchy of uncountable strongly inaccessible cardinals". This seems to follow an earlier paper:

https://lmcs.episciences.org/920

Do I understand correctly that those parts of the core theory which are not explicitly supported, e.g., inductive types in the sort Prop are also known not to affect consistency strength?

Tadeusz Litak (Apr 11 2021 at 14:58):

Ditto for everything else that either has been added since or is presently under consideration. BTW, I recall that Michael Rathjen in Leeds has done a lot of research along similar lines.

Meven Lennon-Bertrand (Apr 12 2021 at 07:56):

As for MetaCoq (the second link), for the moment there is not much work done in the direction of a proof of consistency: a significant part of the library relies on an axiom asserting the strong normalization of the system under consideration (which entails consistency via canonicity). So for now consistency is the blind eye of the formalization, the aim is rather to describe faithfully all nasty features of the real theory of Coq and to prove that this is what a somewhat realistic algorithm indeed checks. But I hope that one not-so-distant day this will come :)

Théo Winterhalter (Apr 12 2021 at 08:18):

Meven Lennon-Bertrand said:

As for MetaCoq (the second link), for the moment there is not much work done in the direction of a proof of consistency: a significant part of the library relies on an axiom asserting the strong normalization of the system under consideration (which entails consistency via canonicity). So for now consistency is the blind eye of the formalization, the aim is rather to describe faithfully all nasty features of the real theory of Coq and to prove that this is what a somewhat realistic algorithm indeed checks. But I hope that one not-so-distant day this will come :)

To rephrase, this is more a verification effort with fewest assumptions possible.

Last updated: Jun 05 2023 at 08:01 UTC