Everything in Context

In Dale's Proof Search Foundations for Logic Programming talk, he gives a great minimalist example of an interactive system: toggling a switch. The encoding in Forum , a logic programming language based on full linear logic, goes like this: flip on off. flip off on. toggle G o- sw V * flip V U * (sw U -o G) or in logic, \[ \exists u,v.[sw\ v\otimes flip\ v\ u \otimes (sw\ u \multimap G)] \multimap toggle\ G \] (Yes, I mainly did that to test the $$\LaTeX$$ rendering script I'm using.) The talk I linked to gives a derivation (which I won't painstakingly copy here) illustrating the execution of the program: the goal sequent $$\Gamma; \Delta, sw\ on \longrightarrow toggle\ G$$ evolves through proof search into $$\Gamma; \Delta, sw\ off \longrightarrow G$$. But this is something of a counterintuitive, higher-order encoding. The "action" by a hypothetical user of toggling the switch must be indexed by $$G$$, the goal that continues the program. Her

As a teaser-trailer to the ideas I have been long overdue to write up, allow me to play some silly games with words. All claims herein are nontechnical and unsubstantiated. PL theorists are fond of the snowclone X-as-Y, "props-as-types" and "proofs-as-programs" being the pervasive example in functional programming. When we similarly try to explain logic programming logically , what comes out is more like "props as programs" and "proofs as traces ". Put another way, in functional progamming, computation is proof reduction while in logic programming, computation is proof search . So, then, what is a game? (I mean in the sense of "something humans play for fun," and specifically "as a piece of software", not the game-theory sense.*) At a rough gloss, a game is an interactive program. An execution of a game alternates computation and accepting human input. Interactive fiction is a minimal distillation of the idea (in that it