?

Log in

No account? Create an account
Thought some more about what happens when you take positive props… - Notes from a Medium-Sized Island [entries|archive|friends|userinfo]
Jason

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

[Dec. 11th, 2015|09:38 pm]
Jason
[Tags|, , , ]

Thought some more about what happens when you take
positive props P ::= ↓G | P ⊕ P | 0
negative props N ::= ↑G | N & N | ⊤
         games G ::= {N|P}

And the interpretation
{N|P} = (left ⊸ N) & (right ⊸ P)
↓G = left ⊗ G
↑G = right ⊗ G

and you consider the classical negation of {N|P}. It's not quite the negative of a game in the Conway-Berlekamp-Guy sense... (defined by -{P|N} = {-N|-P} and -(P ⊕ P) = -P & -P and -↑G = ↓-G and so on) but it seems related somehow. You get
{N|P} = (left ⊗ N) ⊕ (right ⊗ P)
(↓G) = left ⊸ G
(↑G) = right ⊸ G

and then proof search on, say, left, {N|P} ⊢ 0 actually plays out very similarly to that on left, {-P|-N} ⊢ 0, as long as left ⊸ left ⊸ 0 and right ⊸ right ⊸ 0. I posted on twitter about the idea of making this kind of behavior judgmentally intrinsic.
LinkReply