Log in

No account? Create an account
Thinking further about the logic stuff from a couple of days ago,… - Notes from a Medium-Sized Island [entries|archive|friends|userinfo]

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

[Jan. 20th, 2016|08:19 pm]

Thinking further about the logic stuff from a couple of days ago, realize that I definitely need a possibility modality that acts as if time is linear.

From: neelk
2016-01-21 11:14 am (UTC)
Jennifer Paykin, Steve Zdanciewic and I use the following axiom in our recent FRP stuff:
  ◇A ⊗ ◇B ⊸ ◇((A ⊗ ◇B) + (A ⊗ B) + (◇A ⊗ B))

If I understand the modal logic literature properly, this ensures that the Kripke model is a linear order, by saying that with any pair of events, either A happens first, B happens first, or they occur simultaneously.

When we tried to add it to our language in a way that didn't break cut-elimination, we found that the bind rule for the possibility monad changed into a select operator!

So in addition to the sequential composition for the monad:
  let ⋄x = e in t

we also had a parallel case analysis form:
  select e1; e2 with 
  | ⋄x; y → t1         // x:A; y:⋄B 
  | ⋄x; ⋄y → t2        // x:A; y:B
  | x; ⋄y → t3         // x:⋄A; y:B

If you squint, you can see this as a unary and binary parallel select form. When we tried to generalize this to n-ary selects, we realized that we had to give 2^n clauses (for every subset of simultaneously occuring events). So it made sense to make the select rule nondeterministic:
  select e1; e2 with 
  | ⋄x; y → t1         // x:A; y:⋄B 
  | x; ⋄y → t3         // x:⋄A; y:B

where we choose one of the cases nondeterministically if both events happen simultaneously. Cut-elimination still holds, but it's a now a total but not deterministic relation.
(Reply) (Thread)
[User Picture]From: jcreed
2016-01-21 03:33 pm (UTC)
Yeah, Michael Arntzenius was telling me all about this! Sounds awesome. I was trying to work out for myself what the 'judgmental' story is for that diamond, and my best guess so far is

I think I managed to convince myself that cut-elim holds for that, too. I always hate doing these one-off messy cut proofs, and prefer to get it for free out of encoding the exotic connective out of familiar bits, but this one is a tough nut to crack. Something like the recursive definition

◇A = all a . q(a) -o exists b . q(b) -o !s(a) -o s(b) * ((y(a,b) * A) + (n(a, b) * ◇A))

looks like it is a good step in the right direction (where q and s are arbitrary positive atoms with no axioms, and you axiomatize y and n by
y(a, b) * y(b, c) -o 0
y(a, b) * n(b, c) -o y(a, c)
n(a, b) * y(b, c) -o y(a, c)
n(a, b) * n(b, c) -o n(a, c)
(the absence of n(a, a) is necessary to prevent ◇0)

so that when you try to prove ◇A1, ... ◇An |- ◇C, your premises end up being
A1, ◇A2... ◇An |- C
◇A1, A2... ◇An |- C
◇A1, ◇A2... An |- C
and (unfortunately) also
◇A1, ... ◇An |- ◇C

so maybe with some coinduction magic you can let a proof "spin" in the loop at ◇A1, ... ◇An |- ◇C waiting for one of the events to fire. And then figure out how to force C |- ◇C and ◇◇C |- ◇C to hold.

Edited at 2016-01-21 03:34 pm (UTC)
(Reply) (Parent) (Thread)