Jason (jcreed) wrote,

I just recently (as of breakfast today, basically) figured out another version of that scheme Frank and I were working on to uniformally give a "constructive semantics" of substructural logics. This one doesn't have any of the scary continuation-passing translation that the last one did. On the downside, its image is a somewhat more complicated logic. But not terribly more complicated; it's basically a familiar-looking focusing calculus for intuitionistic propositional logic, with some annotations.

Here's how it looks for plain linear logic. The syntax of propositions is the usual polarized language
P ::= ↓N | P ⊗ P | P ⊕ P | a^+ | 1 | 0
N ::= ↑P | P ⊸ N | N & N | a^- | T

and there are ordinary contexts and asynchronous (ordered) contexts:
Γ ::= · | Γ, N^α
Ω ::= · | Ω, P^α

Those superscript alphas are binding positions of world variables. Every assumption in Gamma and Omega binds a distinct world variable that can be used somewhere to its right.

The crux of the scheme (as with the previous ones) is that you can make your own favorite custom substructural logic by filling in the ellipses in the syntax of "worlds" and "frames":
q ::= α | ...         worlds
f ::= φ | ...         frames
s ::= f ▹ q           structures

Worlds and frames can be generated by arbitrary mutually recursive little languages of algebraic terms. No matter what, you get out some logic that satisfies cut and identity and has a well-behaved focusing discipline. For linear logic, we make them
q ::= α | q ⊗ q       worlds
f ::= φ | q ⊸ f      frames
s ::= f ▹ q           structures

Then the judgments are
Γ ⊢ [P] (q)           right focus
Γ [N] ⊢ P^φ (f)       left focus
Γ ; Ω ⊢ N^φ (s)       right inversion
Γ ; Ω ⊢ P^φ (s)       left inversion
Γ ⊢ P^φ (s)           stable

which look like the familiar five judgments of focusing, except with more annotations. The pattern is: things on the left always bind world variables, the thing on the right binds a frame variable, except things in focus don't bind anything --- and then, at the very far right (past the conclusion of the sequent, even, which, as noted, can bind a frame variable) you get some expression, which is a "structure" if you're not focused on anything, and is a world or frame if you're focused positive or negative, respectively.

Just picking all the judgments correctly was the hard part that took me all of breakfast once I had the courage to believe it was possible; after that point, the inference rules and cut elimination principles mostly write themselves. I should, however, obviously TeX them up at some point soon. One mathematician's "mostly obvious" frequently being, of course, another one's "huhwha?", and I know this from being often enough on the other side of it.

*Side note: I found that my agda installation was broken (since I was using agda emacs-mode to type the greek symbols) and I was getting that infuriating "There is no available version of ghc that satisfies -any" error message. TURNS OUT if you move your ~/.ghc out of the way and try to reinstall agda, it works.
Tags: focusing, logic, math

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded