Jason (jcreed) wrote,

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.
Tags: games, linear logic, logic, math

  • (no subject)

    noms is a project apparently influenced by camlistore and git. Has a bunch of juicy buzzwords attached to it (Content-addressable, monotonic,…

  • (no subject)

    Great list of computer books from days of yore, with pictures: http://tedfelix.com/books/ I remember "BASIC Fun: Computer Games, Puzzles, and…

  • (no subject)

    One of two large (~$X00) purchases arrived today: a new desktop, since my five-year-old one is starting to show signs of dying. I already pulled all…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded