Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: calculus of constructions

Bottom of Page

1 to 23 of 23

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeOct 4th 2012
    • (edited Oct 4th 2012)

    I have added the following paragraph to calculus of constructions, I’d be grateful if experts could briefly give me a sanity check that this is an accurate characterization:

    More in detail, the Calculus of (co)Inductive Constructions is

    1. a system of natural deduction with dependent types;

    2. with the natural-deduction rules for dependent product types specified;

    3. and with a rule for how to introduce new such natural-deduction rules for arbitrary (co)inductive types.

    4. and with a type of types (hierarchy).

    • CommentRowNumber2.
    • CommentAuthorUlrik
    • CommentTimeOct 4th 2012

    Number 4 should be more precise: An impredicative universe (type of types), Prop, and a cumulative hierarchy of predicative universes (types of types), Typei_i, on top of Prop.

    Otherwise it looks fine!

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeOct 4th 2012
    • (edited Oct 4th 2012)

    Thanks! (On both accounts.)

    I have changed it now as suggested in the entry.

    But: can’t we allow ourselves not to demand the Prop-universe and still speak of a “calculus of constructions”?

    • CommentRowNumber4.
    • CommentAuthorUlrik
    • CommentTimeOct 4th 2012

    Great.

    But: can’t we allow ourselves not to demand the Prop-universe and still speak of a “calculus of constructions”?

    Quite possibly when you say a CoC as opposed to the CoC! But I’m not sure how I’d define a CoC. I think the version with only predicative universes goes by the name of predicative type theory, but that’s also not quite a definite phrase.

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeOct 4th 2012
    • (edited Oct 4th 2012)

    Okay, thanks.

    I gather that one of the four (or so) “teams” at the IAS HoTT program is concerned with doing something like re-writing Coq to make it homotopy-native.

    I assume that in the course of doing so, they will re-examine these notions. I assume they will come up with a Calculus of homotopy-inductive Constructions, which

    1. refines inductive types to higher inductive types;

    2. drops the Prop-universe.

    Maybe in the near future there’ll be some preliminary notes on this, and then maybe I’ll be allowed to point to it as “another CoC” without Prop-universe :-)

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeOct 5th 2012

    Let’s not proliferate terminology! “The CoC” is a particular type theory, with impredicative quantification. “The predicative CoC” is another one, as is “the predicative CoiC” — the latter is roughly the one that Coq is based on. We already have general notions like “a pure type system” and “a type theory” and “a dependent type theory” — I don’t see any need for a general notion of “a calculus of constructions”.

    • CommentRowNumber7.
    • CommentAuthorUlrik
    • CommentTimeOct 5th 2012

    I agree with Mike about not proliferating terminology.

    I know the Coq manual refers to the “predicative calculus of constructions” (with one impredicative sort, Prop) to distinguish it from the “impredicative calculus of constructions” (with two impredicative sorts, Prop and Set). However, I think I’m not the only one who finds that terminology confusing!

    What do we then call the base of Agda? (I know, that’s a moving target!) – Last I checked, Agda had a non-cumulative hierarchy of predicative universes, and type of universe levels, rather fancy indexed induction-recursion and induction-induction, and a monadic(?) way of treating coinduction with operators ♯ and♭.

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeOct 5th 2012

    @Ulrik, that’s sure a good point about “predicative CoC” including impredicative Prop! Maybe it would be better called “semipredicative”.

    I don’t think I’ve heard anyone call the type theory underlying Agda anything but “the type theory underlying Agda”. (-:

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeOct 5th 2012

    What’s the technical definition of “cumulative hierarchy”. Can a hierarchy of universes not be cumulative?

    • CommentRowNumber10.
    • CommentAuthorUlrik
    • CommentTimeOct 5th 2012
    • (edited Oct 5th 2012)

    Cumulativity means that A:Type iA:Type_i implies A:Type i+1A:Type_{i+1} (so Type iType_i is a subtype of Type i+1Type_{i+1}). In Agda, you have to use an explicit raise operator Type i→Type i+1Type_i\to Type_{i+1}. It’s much easier not to worry about subtyping rules. With subtyping, you have to work a bit to get principal types. I think that was first worked out in Luo’s PhD thesis, An Extended Calculus of Constructions, and in Harper and Pollack’s Type Checking with Universes. However, I’m not an expert here, so perhaps Mike can ask someone at IAS about the precise history.

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeOct 5th 2012

    Where “easier” means “easier for the formal theory of the type system, but much more tedious for the actual user”. (-:

    • CommentRowNumber12.
    • CommentAuthorUlrik
    • CommentTimeOct 5th 2012

    Absolutely! (-:

    Also, concerning type checking with universes, we should mention Gérard Huet’s Extending the Calculus of Constructions with Type:Type, which is an unpublished manuscript from 1987 that’s often referred to. But I haven’t seen it.

    • CommentRowNumber13.
    • CommentAuthorheades
    • CommentTimeOct 6th 2012
    I don't think number three above is quite right.

    CoC is a particular pure type system which did not originally have inductive or co-inductive types.

    CiC was the extension of CoC with (co)-inductive types.

    ECC is the the Extended Calculus of Constructions. Coq is based on ECC.
    • CommentRowNumber14.
    • CommentAuthorheades
    • CommentTimeOct 6th 2012
    Mike you were saying:

    Let’s not proliferate terminology! “The CoC” is a particular type theory, with impredicative quantification. “The predicative CoC” is another one, as
    is “the predicative CoiC” — the latter is roughly the one that Coq is based on. We already have general notions like “a pure type system” and
    “a type theory” and “a dependent type theory” — I don’t see any need for a general notion of “a calculus of constructions”.

    I think that there is more to say about CoC. Coquand's original definition was not as a pure type system. This was pointed out later. Not to mention
    that CoC can also be viewed as a extension of system F-omega. Just some points that might be useful notes.
    • CommentRowNumber15.
    • CommentAuthorheades
    • CommentTimeOct 6th 2012
    In response to my previous response. I may have misunderstood what you meant by "general notion."
    • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeOct 6th 2012

    Yes, probably. (-:

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeOct 6th 2012
    • (edited Oct 6th 2012)

    @heades in #13,

    could you say more concretely what’s wrong with the entry, if anything? Where it gives that numberd item list it does refer to CiC and “with inductive types”. That seems to agree with your #13!?

    I also have a general question: what is the difference between CoC and PTS? It seems to me that if I remove from CiC the inductive types I am left with just PTS. Well, and universes. Is that the difference?

    • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeOct 6th 2012

    PTS refers to a class of type theories, not to any particular one. CoC can be presented as a PTS.

    • CommentRowNumber19.
    • CommentAuthorheades
    • CommentTimeOct 6th 2012
    Urs, Sorry, you are right. I miss read the first post of this discussion and I didn't look
    at the actual entry. It is correct and sorry about that.

    As for your question. Mike is correct we should pin down the terminology in order to be
    precise. CoC is a particular PTS with two sorts and the complete set of rules for these
    two sorts. It is the strongest among the eight systems of the lambda-cube.

    There is no difference between CoC and the PTS defining CoC. If by difference we
    mean expressibility -- which is itself understood as provability. Now as for CiC which
    as you know is the extension of CoC with inductive types and and an impredicative
    universe Set in addition to Type and Prop. As of Coq 8 it is based on predicative CiC.

    Now if we only remove the inductive types from CiC then we obtain CoC with Set which
    is still a PTS. It is however outside the lambda-cube. PTS' may have any number
    of universes as long as they are impredicative.

    I hope this helps.
    • CommentRowNumber20.
    • CommentAuthorheades
    • CommentTimeOct 6th 2012
    One small last remark. I wasn't being all that precise in my last paragraph.

    I was just remembering that in CiC we must stratify Type to maintain
    consistency. Usually, universes or sorts of PTS are not stratified at least by
    the original definition of what a PTS is in general. So this is another
    difference. Just to summarize the major difference between CoC and
    CiC are inductive types, an additional impredicative universe Set, and
    the stratification of Type.
    • CommentRowNumber21.
    • CommentAuthorMike Shulman
    • CommentTimeOct 6th 2012

    Hmm, that’s interesting. I wasn’t aware that Set was considered part of CiC but not CoC.

    • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeJan 3rd 2023
    • (edited Jan 3rd 2023)

    added this pointer:

    diff, v15, current

  23. updated link to Martin Hyland draft

    Anonymouse

    diff, v18, current

1 to 23 of 23

  1.