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.
type checking is currently a redirect to decidability, so I merged those links. I also added my name, since this is my work.
Okay, good.
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…)
\linebreak works to put space between rules, but it’s too much space. Better than too little.
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.
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 “” 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 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 . 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?
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.
If you think there should be a conservativity result, the onus is on you to prove it.
Of course. I was wondering two things:
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.
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.
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.
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.
Hmm. One does generally want to prove things about large types too.
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?
Probably depends on what you’re trying to do.
I probably ought to split this page up. Also, a lot of the stuff on logical frameworks should probably be on logical framework.
atmacen, are you Matt Oliveri?
1 to 47 of 47