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

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf sheaves simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

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.
    • CommentAuthoratmacen
    • CommentTimeMay 14th 2019

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

    v1, current

    • CommentRowNumber2.
    • CommentAuthoratmacen
    • CommentTimeMay 14th 2019

    Shoot. Bad itex command guessing. Do not read this revision.

    diff, v3, current

    • CommentRowNumber3.
    • CommentAuthoratmacen
    • CommentTimeMay 14th 2019

    Hope this makes things readable.

    diff, v3, current

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeMay 14th 2019

    have equipped a bunch of keywords with hyperlinks

    diff, v4, current

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

    diff, v5, current

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeMay 14th 2019

    Okay, good.

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeMay 14th 2019

    have added a table of contents and a floating context menu

    diff, v6, current

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

    diff, v7, current

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

    diff, v9, current

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

    diff, v11, current

    • CommentRowNumber16.
    • CommentAuthoratmacen
    • CommentTimeMay 15th 2019

    I think that does it for the rules!

    diff, v14, current

    • CommentRowNumber17.
    • CommentAuthoratmacen
    • CommentTimeMay 16th 2019

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

    diff, v17, current

    • 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 “CompComp” 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 CompComp 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 CompComp. 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.

    diff, v18, current

    • CommentRowNumber20.
    • CommentAuthoratmacen
    • CommentTimeMay 16th 2019

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

    diff, v18, current

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

    diff, v21, current

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

    diff, v26, current

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

    diff, v27, current

    • 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 21st 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.

    diff, v31, current

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

    diff, v37, current

    • CommentRowNumber36.
    • CommentAuthoratmacen
    • CommentTimeJun 1st 2019

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

    diff, v38, current

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

    diff, v40, current

    • CommentRowNumber38.
    • CommentAuthoratmacen
    • CommentTimeJun 8th 2019

    Cleaned up and slightly expanded the explanation about nonadmissibility of strengthening.

    diff, v43, current

    • CommentRowNumber39.
    • CommentAuthoratmacen
    • CommentTimeJun 9th 2019

    Finally started adding stuff about logical frameworks.

    diff, v44, current

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

    diff, v50, current

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

    diff, v53, current

    • CommentRowNumber45.
    • CommentAuthoratmacen
    • CommentTimeJul 4th 2019

    Finished filling in the sections on logical frameworks.

    diff, v56, current

    • CommentRowNumber46.
    • CommentAuthoratmacen
    • CommentTimeJan 24th 2020

    It seems that subtyping variance rules are derivable after all, without having to add more primitive rules.

    diff, v60, current

    • CommentRowNumber47.
    • CommentAuthoratmacen
    • CommentTimeJul 11th 2020

    Changing page name because the acronym “CLF” is used for “Concurrent Logical Framework”.

    diff, v63, current