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.
Yeah, its complicated. Right now if we put all adjectives together we get "Polymorphic Predicative Calculus of Cumulative Inductive Constructions"
predicative being extremely deceptive here
Yes :)
And if we look to the future, with sort polymorphism it certainly wouldn't make sense to keep it in the name
But you're right, we already have Prop which is a distinguishing feature
We probably want a name for the theory that doesn't change when we extend it.
And if forgot that some papers use (Co)-Inductive
too, so "Calculus of Cumulative (Co)-Inductive Constructions". That's a lot of C's
could be pronounced koko
something about primitive records too, or is that counted in inductive constructions?
also the module system
or "Polymorphic Calculus of Cumulative (Co)-Inductive Constructions" a.k.a. "PoCaCuICo"
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
"PoCaCuICo"
with some more effort you can get to Acapulco, and have a drink ;-)
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.
Yes, I agree with that, it's too technical for a software name
Then maybe the sentence in cic.rst
should be changed to The underlying formal language of Coq is _the_ Calculus of Inductive Constructions (CIC)
?
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 :)
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 ?)
It seems Agda just says "an extension of MLTT" in comparison.
This thread reminds of the famous "lambda bar mu mu-tilde"
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.
Not so sure that catenating all language features leads to something readable
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
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
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"
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.
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.
@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 :))
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
?
Wasn’t Prop another major difference? But also not that relevant anymore
An impredicative sort is a relevant difference
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
Meven Lennon-Bertrand said:
Wasn’t Prop another major difference? But also not that relevant anymore
Why is it not relevant anymore?
I think Meven was referring to the fact that Agda now has Prop
(corresponding to Coq's SProp
) too.
IIRC it's a predicative version (so there's Prop@{i} next to Type@{i})
Gaëtan Gilbert said:
IIRC it's a predicative version (so there's Prop@{i} next to Type@{i})
Yes.
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
Thanks for clarifying.
@Yannick Forster its just that you might want to distinguish the source/surface and target/kernel languages, as in Gallina and Gallina-Core
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 :/
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)
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
How about SATT for "State of the Art Type Theory" :-)
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
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)
What is the distinction between Gallina and CIC/Coq's type theory?
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?
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.
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).
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 :)
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.
Do all these subsequent extensions have any influence on the consistency strength? The first item here
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?
@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.
(the first paper gives a model in ZFC, not ZF, but ZFC and ZF are equiconsistent)
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?
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.
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 :)
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: Nov 29 2023 at 17:01 UTC