I keep fiddling around with the logic/embedding thingy from yesterday, even though its relationship to BI is highly unclear... I know sometime in the deep past of mid-thesis times I set up a labelled deduction system where the labels existed over some monoid, but I think I understand the focusing consequences of that a lot better now.

Say your context is full of propositions at labels p that can be the identity, or a variable, or a (not necessarily commutative!) monoid operation or maybe some other function symbols:

I assume the monoid operation * is associative, and has unit e.

I'm going to need to lift the monoid operation to an action on contexts, but this is totally straightforward:

I then get two interesting modalities, one positive and one negative:

I seem to be forced into this ordering by considering the general case where * is not commutative. I kind of expected modalities to synchronously demand stuff be pulled off the same end that they put it on, but they don't --- they insert and delete at opposite ends of monoid expressions. Maybe this is another shadow of whatever phenomenon makes queue logic happen instead of stack logic?

Anyway I am pretty sure the circle operation I'd been talking about up until now is this box-plus, and the filled-circle I want is box-minus. The plain old conjunction and disjunction and units don't do anything interesting here; they just propagate (or allow) all labels. But implication takes just a little bit of care:

Although I'm writing contexts as Γ and Δ, I still understand contraction and weakening to be implicitly allowed. I just have to do a context merge in implies-left because one of the contexts gets hit with a [p *], while the other doesn't.

Here's what identity and cut:

And here's the encodings of tensor and its right adjoint that I think are correct for some value of "correct":

(full image here)
Tags:
• #### (no subject)

Something that's bugged me for a long time is this: How many paths, starting at the origin, taking N steps either up, down, left or right, end up at…

• #### (no subject)

Still sad that SAC seems to end up being as complicated as it is. Surely there's some deeper duality between…

• #### (no subject)

I had already been meaning to dig into JaneSt's "Incremental" library, which bills itself as a practical implementation (in ocaml) of the ideas in…

• Post a new comment

#### Error

Anonymous comments are disabled in this journal

default userpic