Jason (jcreed) wrote,

I've gotten caught up in the last few days working on a new tack on a vague idea concerning the proof of completeness for focussing, which I first had about this time last year. The underlying dogma I'm clinging to is that focussing is not so much about forcing decomposition into little alternating phases, but more about which logical connectives really exist for a given judgmental setup, and more to the point, which connectives can be coalesced - the answer being, of course, those of the same polarity.

This means that asynchronous connectives need not be eagerly decomposed, and this simplifies the soundness proof. The bookkeeping for showing completeness this way has always been off-puttingly ugly and un-modular, though I did manage to slog through it once. Yesterday afternoon I discovered a nice little encoding of the context discipline of focussing of intuitionistic logic into (depending how you look at it) a variant of ordered logic with a couple of only mildly exotic modal operators, or, if you prefer, perfectly ordinary ordered logic with focussing applied only to positive atoms and the copy rule.

Inside this encoding:

  • The bookkeeping of tracking the long-term effects of asynchronous decomposition can be fully internalized into the language of propositions
  • The essential commutativity properties of asynchronous decomposition fall out as two easy-to-state lemmas, one for positive connectives, and one for negative
  • The total amount of proof-work to establish focalisation is evidently linear in the number of logical connectives

I'm really quite happy with it.
Tags: focussing, math

  • (no subject)

    Playing around with the agda javascript backend, now. Like, my ears are popping from the sudden change of type-theory-pressure.

  • (no subject)

    Trying to understand in general what kind of diagrammatic interactions between degree-three nodes actually read sensibly in the lambda calculus:

  • (no subject)

    Not sure this is the simplest possible inverse (or even that it is correct) but it makes for a fun diagram:

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded