# Start a new discussion

## Not signed in

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

## Site Tag Cloud

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

• CommentRowNumber1.
• CommentAuthoratmacen
• CommentTimeMay 14th 2019

For now, a place to try putting some typing rules for proto CLF.

• CommentRowNumber2.
• CommentAuthoratmacen
• CommentTimeMay 14th 2019

• CommentRowNumber3.
• CommentAuthoratmacen
• CommentTimeMay 14th 2019

• CommentRowNumber4.
• CommentAuthorUrs
• CommentTimeMay 14th 2019

have equipped a bunch of keywords with hyperlinks

• CommentRowNumber5.
• CommentAuthoratmacen
• CommentTimeMay 14th 2019
Thanks!
• CommentRowNumber6.
• CommentAuthoratmacen
• CommentTimeMay 14th 2019

type checking is currently a redirect to decidability, so I merged those links. I also added my name, since this is my work.

• CommentRowNumber7.
• CommentAuthorUrs
• CommentTimeMay 14th 2019

Okay, good.

• CommentRowNumber8.
• CommentAuthorUrs
• CommentTimeMay 14th 2019

• CommentRowNumber9.
• CommentAuthoratmacen
• CommentTimeMay 14th 2019

Why are these rules appearing in such a small font? And how do I make a line break? (Am trying to look into this; just recording my problem.)

• CommentRowNumber10.
• CommentAuthorUrs
• CommentTimeMay 14th 2019

You make a line break by typing

  \linebreak


Regarding typesetting the deduction rules: I seem to remember that Todd had looked into this at some point and found a good solution. But I forget where and how. (Once we remember, we should record this at HowTo…)

• CommentRowNumber11.
• CommentAuthoratmacen
• CommentTimeMay 14th 2019

Using double-dollar-sign itex blocks. Fixes the font size of the rules. Probably shoulda known.

• CommentRowNumber12.
• CommentAuthoratmacen
• CommentTimeMay 14th 2019
Oops. But then consecutive rules don’t have enough space between them.
• CommentRowNumber13.
• CommentAuthoratmacen
• CommentTimeMay 14th 2019

\linebreak works to put space between rules, but it’s too much space. Better than too little.

• CommentRowNumber14.
• CommentAuthorUrs
• CommentTimeMay 14th 2019

I do believe there was a decent solution, but I didn’t pay attention back then. Maybe open a thread with the question, so that people see it.

• CommentRowNumber15.
• CommentAuthoratmacen
• CommentTimeMay 15th 2019

Fixed references for equality formation and PER comprehension.

• CommentRowNumber16.
• CommentAuthoratmacen
• CommentTimeMay 15th 2019

I think that does it for the rules!

• CommentRowNumber17.
• CommentAuthoratmacen
• CommentTimeMay 16th 2019

Whoops, forgot the variable rule! (Because I was copying from HOAS rules.)

• CommentRowNumber18.
• CommentAuthoratmacen
• CommentTimeMay 16th 2019

From another thread, which changed subject to conservativity of Nuprl-style systems:

Can you save me some time by pointing out exactly how the inductive definition of A.3 differs from, say, MLTT+UIP, or whatever intrinsically typed system it is easiest to compare it to?

Looking at A.3 more closely now (it’s been a while since I read it carefully), I’m remembering how weird those rules are. What I call reflexivity is (usually?) admissible, not a rule. On A.3.16, introduction is like the CLF “selectivity” rules. because is obviously unsound; it’s like Coq’s Admitted. Elimination rules tend to be sequent-style “left rules”, rather than the usual MLTT style. Universes and inductive types (rectype) won’t work; ignore. Atoms and integers should be sufficiently similar to natural numbers.

I guess the first thing to compare it to would be ETT (or MLTT+UIP) with Pi, funext, Sigma, empty type, natural numbers, lists, regular propositional truncation, and quotients. Actually, I guess regular propositional truncation is definable from the other stuff.

In your prototype CLF, to start with I have no idea what “$Comp$” would mean in categorical semantics.

My question is not about finding categorical characterizations of all the type constructors, but whether it’s a conservative extension of ETT. The $Comp$ type is not in ETT, so conservativity doesn’t say anything about that. (I think the other CLF type constructors have order theoretic characterizations relative to $Comp$. Like a function type is the greatest type of apply-able computations.)

For a possible analogy, material and structural set theories have different styles, but if you translate propositions from structural to material set theory, is there a difference in provability?

• CommentRowNumber19.
• CommentAuthoratmacen
• CommentTimeMay 16th 2019

Discussion of admissible rules, and a bunch of empty sections I ought to fill.

• CommentRowNumber20.
• CommentAuthoratmacen
• CommentTimeMay 16th 2019

Five-hash subheadings make the text too small. :(

• CommentRowNumber21.
• CommentAuthoratmacen
• CommentTimeMay 17th 2019

Removed the “Discussion” section, hoisting out the subsections, because most of the sections are discussion, and they were too deeply nested.

• CommentRowNumber22.
• CommentAuthorMike Shulman
• CommentTimeMay 19th 2019

Ok, well, in the other thread you said

it’s not clear to me that Nuprl isn’t already a conservative extension. Do you know some incompatibility besides unusual types and funky type equality?

I guess my answer is that the entire frameworks are prima facie incompatible. If you think there should be a conservativity result, the onus is on you to prove it.

• CommentRowNumber23.
• CommentAuthoratmacen
• CommentTimeMay 19th 2019

Clarification of “not all functions are lambdas”: proto CLF does satisfy an eta rule for function types.

• CommentRowNumber24.
• CommentAuthoratmacen
• CommentTimeMay 19th 2019

If you think there should be a conservativity result, the onus is on you to prove it.

Of course. I was wondering two things:

• If you could spot any counterexamples. (I can’t.)
• If conservativity would remove the problem of it being based on a particular semantics.
• CommentRowNumber25.
• CommentAuthoratmacen
• CommentTimeMay 20th 2019

It occurred to me that curly braces was an awful choice of notation for squash, since set theory uses that for singleton sets. BTW, singleton types are ambiguous: you also need to specify equality. But still.

• CommentRowNumber26.
• CommentAuthorMike Shulman
• CommentTimeMay 20th 2019

I don’t immediately see any counterexamples, but I haven’t really looked. A conservativity result might resolve the semantic problem, though it might depend on the precise form of the result.

• CommentRowNumber27.
• CommentAuthoratmacen
• CommentTimeMay 20th 2019

I’ve been too vague about what I want the result to actually say. I don’t want to commit to a precise formulation because I don’t know what features are needed from ETT to get anywhere.

I think a way to say the gist of what I expect is that the full subcategory corresponding to the small types, of the syntactic category of ETT embeds into the syntactic category of an appropriate Nuprl-style system. The small types are the ETT types in the bottom universe, if the ETT has universes, otherwise it’s all of them.

So there’s a syntactic translation from ETT terms to Nuprl-style terms. That part is clear once all the required type constructors are available on the Nuprl side. (Although it’s not shown (yet?), you can construct sigmas and coproducts in CLF.) So I think the translation, along with a proof that it preserves typing, is a functor, and the conservativity result makes it full and faithful.

• CommentRowNumber28.
• CommentAuthoratmacen
• CommentTimeMay 20th 2019
So I figure you could pick whatever semantics you like for the relevant ETT, and use the Nuprl-style system to reason about the elements of small types. But you can't use an axiom that uses a universe. (Since discharging the assumption makes the type large.)
• CommentRowNumber29.
• CommentAuthorMike Shulman
• CommentTimeMay 20th 2019

I’m not sure what you mean when talking about universes, but aside from that, yes I think if the syntactic category of one theory embeds full-faithfully in another one then that would be sufficient.

• CommentRowNumber30.
• CommentAuthoratmacen
• CommentTimeMay 20th 2019

Maybe my grammar was too weird. There are generally three categories involved: the syntactic category of an ETT, the syntactic category of a Nuprl-style system, and a full subcategory of small ETT types. The translation functor I have in mind is only an embedding of the small types.

• CommentRowNumber31.
• CommentAuthorMike Shulman
• CommentTimeMay 20th 2019

Hmm. One does generally want to prove things about large types too.

• CommentRowNumber32.
• CommentAuthoratmacen
• CommentTimeMay 21st 2019

The problem with large types (if my expectations are correct) is the universes. Nuprl-style universes are different from ETT universes. I’m wondering if that’s really a problem though, since neither kind of universe is univalent. They’re both arbitrary ways of coding for the “real” types, from a univalent perspective. Are ETT universes somehow preferable anyway?

• CommentRowNumber33.
• CommentAuthorMike Shulman
• CommentTimeMay 21st 2019

Probably depends on what you’re trying to do.

• CommentRowNumber34.
• CommentAuthoratmacen
• CommentTimeMay 28th 2019

Greatly expanded “Idea” section, with more discussion about the “why” and “how” of CLF, gist of the expected proof system, and connection to Cedille. Also, an extra reference, about proof checking.

• CommentRowNumber35.
• CommentAuthoratmacen
• CommentTimeMay 30th 2019

Noting that on-the-fly realizer extraction, aka dependent proof refinement, is also implemented in RedPRL, and is apparently a style of elaboration.

• CommentRowNumber36.
• CommentAuthoratmacen
• CommentTimeMay 31st 2019

Expanded the “Idea/Method” subsection with explanation of how checking proof terms relates to tactic engines.

• CommentRowNumber37.
• CommentAuthoratmacen
• CommentTimeJun 1st 2019

Added section about how “constructive”, “intuitionistic”, and classical propositions are represented in CLF (and also Nuprl), along with discussion of the difference between constructive and intuitionistic in this sense.

• CommentRowNumber38.
• CommentAuthoratmacen
• CommentTimeJun 8th 2019

• CommentRowNumber39.
• CommentAuthoratmacen
• CommentTimeJun 9th 2019

• CommentRowNumber40.
• CommentAuthoratmacen
• CommentTimeJun 9th 2019

I probably ought to split this page up. Also, a lot of the stuff on logical frameworks should probably be on logical framework.

• CommentRowNumber41.
• CommentAuthoratmacen
• CommentTimeJun 12th 2019

Finally put stuff in “PER theory”, although it’s not the material I was originally planning to put there. For now, it explains refinement-style quotients.

• CommentRowNumber42.
• CommentAuthorTodd_Trimble
• CommentTimeJun 12th 2019

atmacen, are you Matt Oliveri?

• CommentRowNumber43.
• CommentAuthoratmacen
• CommentTimeJun 12th 2019
Yes.
• CommentRowNumber44.
• CommentAuthoratmacen
• CommentTimeJun 23rd 2019

Filled in the LF= section. Improved the reference to Andromeda. (There’s now also an arXiv link.)

• CommentRowNumber45.
• CommentAuthoratmacen
• CommentTimeJul 4th 2019

Finished filling in the sections on logical frameworks.