September 9th, 2012

beartato phd

(no subject)

Ah, my cherished recent conjecture that BI is complete for the category of graphs (equipped with the (perhaps unique non-cartesian?) monoidal product that I described before) is false. Sad!

Here's the counterexamples that occurred to me this morning. The first one I found was
(A ⊗ ⊤) ∧ 1 ⊢ A ∧ 1
which is a special case of the distributivity property
(A ⊗ B) ∧ 1 ⊢ (A ∧ 1) ⊗ (B ∧ 1)

Both are true of my intended interpretation in Grph, but not provable in BI.

The operations of "∧ 1" and "⊗ ⊤" are kind of interesting in their own right. The graph A ∧ 1 strips all edges off of A, leaving only the vertices behind. (Since 1 is the one-vertex, no-edge graph, and edges in the cartesian product A ∧ B of two graphs generally consist of pairs of edges, one from A, one from B) the graph A ⊗ ⊤ takes A and adds self-loops at every vertex (since ⊤ is the one-vertex, one-self-edge graph, and edges in the tensor product A ⊗ B consist of pairs that are either a vertex from A and an edge from B, or an edge from A and a vertex from B).

But in that case it's clear that if you add some self-edges, then obliterate all edges, including the ones you just added, it's the same thing as just obliterating all edges, thus (A ⊗ ⊤) ∧ 1 ⊢ A ∧ 1.

In the separation-logic-ish interpretation of BI as talking about memory in a program, this seems to be hypothesizing a heap about which we know
(a) It divides into two parts, one of which has property A, and the other half we know nothing in particular about
(b) That it is empty
and it actually seems reasonable to conclude that therefore property A does hold of the heap, since any part of the empty heap is empty, and the current heap is empty.

So this dredges up dim memories I have of neelk and noam and rob talking in front of a whiteboard somewhere in Wean about extra-axiomatic stuff that you might want to add in a separation logic that would imply things like

A ∧ 1 ⊢ A ⊗ A

whose heuristic "proof" also involves making hay out of the known emptiness of A.

Oh wait, and the graph model validates this sentence, too! So this is a third counterexample.




Stillll though I think my previous rambling might possibly lead to a purely-equational reduction of BI to first-order logic, but I guess I'm now convinced that in order to do so, it has to depart somewhat from my graph-ish intuitions. I start suspecting I have to replace the binary + on booleans with something noncommutative, so that I end up representing paths through the BI context-tree...

Anyway, ♥ ♥ ♥ math ♥ ♥ ♥.
beartato phd

(no subject)

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)