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: pure type system

Bottom of Page

1 to 19 of 19

  1.  
    • 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.

  17. 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

  19. corrected a url/link.

    Anonymous

    diff, v23, current

1 to 19 of 19

  1.