Jason (jcreed) wrote,

Progress on thesis slowing a little bit but not stopped.

Super exciting new results on this CSL paper Frank and I are trying to work on.

What's interesting to me is that in typical logics, unlike typical programming languages, there are good metrics of what it means to have an embedding that isn't trivial. Like if you get a good flamewar going between an ML hacker and a LISP hacker, the ML will point to their ability to make a type of sexps and shove all of LISP in there, and the LISP hacker will think that an ML typechecker is only willing to compile a fraction of the sensible programs in the world, and only in a funny irregular syntax at that.

But! It is possible to embed focused classical logic into focused intuitionistic logic (and not the opposite) in a sensible primitive-recursive sort of way that preserves focusing --- I hear via Frank that he just worked this out in a conversation with Evan and Kaustuv not so long ago. To preserve focusing is a really strong condition.

And I think we've worked out further how to embed just about every substructural logic I've ever heard of to this same high degree of faithfulness into just the negative connectives of focused first-order linear logic. And it yields cut-elimination, identity, a focusing system, ad completeness of focusing for all those logics for free.

Of course, something could have gone wrong, but that's always the case until you've finished writing it up...
Tags: work

  • (no subject)

    More things to add to the "chord progressions that aren't cliches-I-already-know-about nonetheless covertly appearing in multiple places" file.…

  • (no subject)

    Consider the chord motion in Lights's "Cactus In The Valley" that happens around 49s in: v link goes here | F G C C | F G C C | F G Am D7 | F G…

  • (no subject)

    Cute little synth widget playground: https://blokdust.com/

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded