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).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeOct 4th 2012

    added to pure type system in the Idea-section the statement

    In other words a pure type system is

    1. a system of natural deduction

    2. with dependent types

    3. and with the dependent product type formation rule.

    and to the Related concepts-Section the paragraph

    Adding to a pure type sytstem

    1. rules for introduing inductive types

    2. possibly a type of types hierarchy

    makes it a calculus of inductive constructions.

    Finally I added to the References-section a pointer to these slides

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeOct 5th 2012

    I think CiC is a particular pure type system; your phrasing sounds like it is a class of them.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeOct 5th 2012

    Okay.

    Can you maybe help me understand what these 8 different pure type systems in the cube are? I don’t understand the notation when it comes to discussion of that.

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeOct 5th 2012

    The notational names for those things like λ \lambda_\to are ad hoc, I wouldn’t pay them too much mind.

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

    What I don’t understand is what (*,)(\ast,\Box) and (,)(\Box, \Box) and so on means.

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeOct 5th 2012

    They’re specifying the relevant set RR of “relations” as described in the “Definition” section.

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeOct 5th 2012
    • (edited Oct 5th 2012)

    Gee, I still don’t get it. Not only that I don’t understand the message, but I cannot even recognize a message.

    Is “\Box” the name of some generic set? Could I write “XX” instead of “\Box”? Why do we suddenly use geometric figures instead of variables? Is “*\ast” also any set? It’s not meant to be singleton set?

    Then: what does it mean to say that “(*,)(*,\Box)” is a relation? Which relation is this supposed to denote? On which set? And how am I supposed to think of it in words? Which role does that relation play?

    Gee, I must be missing something really basic here. That feels weird.

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeOct 5th 2012
    • (edited Oct 5th 2012)

    Ah, I am making progress. SS is the set with one or two or three elements, right?

    There are a bunch of curly brackets missing in the entry, could that be?

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeOct 5th 2012

    If putting curly brackets in would help, please do.

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

    Okay, here I am, at past 2:00 in the morning, editing an entry that I couldn’t parse a minute ago. :-)

    Right after where the triples appear, I am adding the folllowing remark. Give me a sanity check:

    Remark. These relations will appear in the type formation rule for dependent product types below. They will say that for a type of sort s 2s_2 depending on a type of sort s 1s_1 its dependent product type has sort s 3s_3.

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeOct 5th 2012
    • (edited Oct 5th 2012)

    Does this here parse for you:

    symbol actual value
    S=S = {*,}\{\ast, \square\}
    A=A = {(*:)}\{(\ast : \square)\}
    R=R = {(*,*),(*,),(,*),(,)}\{(\ast, \ast), (\ast, \square), (\square, \ast), (\square, \square)\}

    ?

    I am now doing the other tables accordingly. Hope that’s right.

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeOct 5th 2012
    • (edited Oct 5th 2012)

    Checking if I am following:

    For the case of the PTS that is the CoC (the yes, yes, yes, yes-case :-) we have

    • *=Prop\ast = Prop

    • =Type\Box = Type

    is that right?

    • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeOct 5th 2012

    Yes, I think all of that is right. Sorry, I didn’t realize how opaque the previous entry was! Your added remark after the definition of the “relations” is I think greatly helpful (I fixed a typo).

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeOct 5th 2012

    Okay, thanks.

    I have added a remark in a new subsection to make the special case of the CoC more explicit.

    • CommentRowNumber15.
    • CommentAuthorJonasFrey
    • CommentTimeMay 1st 2015

    Hi, I’ve been looking into pure type systems in the last week, and I also had a look on the nlab page. According to the nlab, a pure type system is a triple (S,A,R) of a set S of “sorts”, a set A of axioms, and a set R of “relations”.

    However, I think the elements of R are called “rules”, not “relations” in the literature that I know. Is there a reason why they are called “relations” here or is it by mistake? If nobody objects I can change it.

    • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeAug 5th 2015

    Belatedly: thanks Jonas!

    I added to pure type system a remark that they can be augmented with a cumulativity relation between sorts, and a reference.

  1. added missing comma

    Anonymous

    diff, v21, current

    • CommentRowNumber18.
    • CommentAuthoratmacen
    • CommentTimeApr 10th 2019

    Changing the metavariable names in the idea section to use b:Bb:B rather than B:CB:C. The latter isn’t following any convention I’ve seen.

    diff, v22, current

  2. corrected a url/link.

    Anonymous

    diff, v23, current