
[Sep. 16th, 201208:45 am]
Jason

Oh dang the problem of expressing readonly access in linear logic (or as chrisamaphone expressed her preference for naming it, the "contingent transition problem") that she and taus were discussing so fruitfully is really fascinating. It was a topic that came up frequently back in early stages of my thesis discussions with Frank, since we kind of thought having firstclass labels for state might provide a solution. But I think they don't provide as strong a solution as can be hoped for.
My digestion of their thoughts goes as follows: (which, incidentally, is meant to repudiate all the comments I left on that post, which are a broken semisolution, I now think)
Suppose c is a positive atom. P and N will stand for general positive and negative propositions. I'd like to add to the logic a propositional notation [c]N, which, when it's on the left of the turnstile, means "you can focus on N as long as c is in the context right now".
Ok, fine, [c]N = c o N, bam, done. PROBLEM: c is consumed, and N wanted to use that delicious, succulent positive atom. Ok, fine, [c]N = c o c * N. PROBLEM: switching back to positive polarity means that by the time you're focusing on N again, the c may no longer be around. Like, the beginning (bottom) of my proof might look like this:
N  P  c, N, c o 1  P  c, c o c * N, c o 1  P
now I'm able to choose to focus on N  or wait until later!  even though c is gone. This is not the intended semantics of [c]N.
Ok, so what I'll try is defining [c]N = c o {c}N and defining {c}N recursively in N.
{c}(^P) = ^(c * P) {c}(N & N) = {c}N1 & {c}N2 {c}(top) = top {c}(P o N) = ({c}P o N) & (P o {c}N) {c}(vN) = v(c o N) {c}(P1 + P2) = {c}P1 + {c}P2 {c}(0) = 0 {c}(P1 * P2) = ({c}P1 * P2) + (P1 * {c}P2) {c}(1) = 0
This threads the c down through the synchronous meat of N down to wherever the shifts are, and whenever they happen, it "gives c back". The & in the case for o (and the + in the case for *) expresses the choice involved in the multiplicative contextsplit between two contexts: we can send the c (the one that we're eventually going to stick in some context, but not until we find a shift) to either side, our choice.
Then we can extend [c]N to more general positive propositions by saying
[P1 + P2]N = [P1]N & [P2]N [P1 * P2]N = [P1][P2]N [0]N = top [1]N = N

Anyway I am again intrigued whenever something kinda like the product rule for derivatives (aka "Leibniz Law" from firstyear calculus, d/dx (fg) = (df/dx) g + f (dg/dx)) shows up in logic (like it did in that graphlogic stuff).
I never had occasion above to define a dual [c]P = c * {c}P, but it almost smells suspiciously (If I'm allowed to imagine {c}P to be "a P with a cshaped hole" just because {c} is slightly derivativelike, and derivatives of types are types with holes) like "a c together with a P with a cshaped hole", which is a satisfying pair of things to have.

Huh! Indeed by an easy induction I can show that always [c]P  P and N  [c]N. This kind of makes sense, I guess? If [c]N on the left means "you can use N as long as you can verify c is present without really consuming it" then [c]N on the right must mean something like "you must make N, but you are provided with the assumption that c is present, without really producing it". So if you already have an N in the context, you should be able to make a [c]N, ignoring the assumption of c's presence. 

