Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
added to pure type system in the Idea-section the statement
In other words a pure type system is
a system of natural deduction
with dependent types
and with the dependent product type formation rule.
and to the Related concepts-Section the paragraph
Adding to a pure type sytstem
rules for introduing inductive types
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
I think CiC is a particular pure type system; your phrasing sounds like it is a class of them.
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.
The notational names for those things like $\lambda_\to$ are ad hoc, I wouldn’t pay them too much mind.
What I don’t understand is what $(\ast,\Box)$ and $(\Box, \Box)$ and so on means.
They’re specifying the relevant set $R$ of “relations” as described in the “Definition” section.
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 “$X$” 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.
Ah, I am making progress. $S$ 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?
If putting curly brackets in would help, please do.
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_2$ depending on a type of sort $s_1$ its dependent product type has sort $s_3$.
Does this here parse for you:
symbol | actual value |
---|---|
$S =$ | $\{\ast, \square\}$ |
$A =$ | $\{(\ast : \square)\}$ |
$R =$ | $\{(\ast, \ast), (\ast, \square), (\square, \ast), (\square, \square)\}$ |
?
I am now doing the other tables accordingly. Hope that’s right.
Checking if I am following:
For the case of the PTS that is the CoC (the yes, yes, yes, yes-case :-) we have
$\ast = Prop$
$\Box = Type$
is that right?
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).
Okay, thanks.
I have added a remark in a new subsection to make the special case of the CoC more explicit.
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.
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 to 19 of 19