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

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 mostly separates itself from rendering concerns; writing IF is almost entirely writing game mechanics).

So to reiterate, in a logic programming setting, computation is proof search. Hypothesis:

What I would like to post about next is a few of the low-level ideas that can potentially lend service to this overarching motivation.

---

*Or do I? To throw yet another analogy-turned-correspondence into the mix, it turns out that you can give a game semantics to proof search, giving way to types-as-games and proofs-as-strategies -- not all too different from what I am proposing.

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 mostly separates itself from rendering concerns; writing IF is almost entirely writing game mechanics).

So to reiterate, in a logic programming setting, computation is proof search. Hypothesis:

**, or ITP). (Ever heard someone marvel at how using Coq feels like playing a video game?) Allowable actions for a user to take turn into inference rules (at the object level, so horn clauses), and the game can treat this as a suggestion for proof search, after which point it may forward-chain to arrive at the next state of the game. Specifically, some flavor of linear logic programming seems natural to meet the demands of encoding state transitions.***interactive computation*-- that is, a game -- is*interactive proof search*What I would like to post about next is a few of the low-level ideas that can potentially lend service to this overarching motivation.

---

*Or do I? To throw yet another analogy-turned-correspondence into the mix, it turns out that you can give a game semantics to proof search, giving way to types-as-games and proofs-as-strategies -- not all too different from what I am proposing.

Interesting. I recently stumbled on the IF language Inform 7, and I was surprised by the declarative, logic programming side to it. But, it handles state change in ad-hoc ways, and I wondered whether some kind of linear logic could remedy this.

ReplyDeleteSounds like you've gone quite a bit further than just wondering. Any chance of hearing about the low-level ideas?