? ?
Notes from a Medium-Sized Island [entries|archive|friends|userinfo]

[ website | My Website ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

[Sep. 16th, 2012|08:45 am]
[Tags|, , , , ]

Oh dang the problem of expressing read-only 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 first-class 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 semi-solution, 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 context-split 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 first-year calculus, d/dx (fg) = (df/dx) g + f (dg/dx)) shows up in logic (like it did in that graph-logic 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 c-shaped hole" just because {c} is slightly derivative-like, and derivatives of types are types with holes) like "a c together with a P with a c-shaped 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.

(Deleted comment)
[User Picture]From: jcreed
2012-09-16 07:58 pm (UTC)
Hmm.. I'll double-check the definitions when I get a real computer
(Reply) (Parent) (Thread)