Modeling gameplay in Celf, Part 1: Fuzz Testing

I'm hereby resolving to stop biting off more than I can chew wrt blog posts - I've got two behemoths in drafts over just the past few days and nothing to show for them (yet). So right now I'm going to try to carefully explain a tiny example that I just worked out over the past half hour and I think nicely encapsulates a few ideas about using Celf and linear logic in the context of interactivity.

Assumed background for this post: familiarity with linear logic connectives, some familiarity with logic programming and the forward/backward chaining distinction.

Here's an informal spec for a simple branching game with a couple pieces of global state that track whether certain paths have been taken:

The cellar and the den are connected rooms. The lamp and the key are in the den. The cellar contains a door, which is locked and must be opened with the key. Once the door is unlocked, the player enters darkness, and if they have a lamp, they win; otherwise, they are eaten by a grue and lose.

Here is the author's eye view of the game as we'd write it in Twine:

(You can interact with the output of the build here.)

The pieces of global state here are represented by two boolean variables ("<<set $x = ...>>" and "<<if $x eq ...>>" are Javascript macros under the hood). Double-brace [[links]] make a player control to navigate to the linked passage, and the edges in the graph show what's linked to what. This simple visual authoring tool gets a lot of people started writing their first games/interactive stories, and many have used it to build stunningly complex and evocative narratives.

Here's how I'd translate this game into a purely-atomic, forward chaining linear logic program, adding one rule at a time:

start -o {den & cellar}. 

When the player begins, they choose to go to the den or the cellar.

den -o {cellar & getlamp & getkey}.  

This works if we always want to display the option to get the lamp and the key, even after they've been retrieved. If we want to conditionally display those choices, we'd need a rule like this:

den -o  
         & (nolamp -o {getlamp}) 
         & (nokey -o {getkey})}.

We stay in the den if we try to get the key or the lamp.

getlamp -o {gotlamp * den}.
getkey -o {gotkey * den}.

Instead of changing a boolean value, we consume one piece of state and replace it with one intended as its complement (most logic programming languages don't support negation directly, but it's easy to encode with a predicate, so this is really just a shortcut).

cellar -o {den & opendoor}.

From the cellar, we can go back to the den or try to open the door.

opendoor * nokey -o {cellar * nokey}.
opendoor * gotkey -o {dark}.

Opening the door without the key keeps us in the cellar and retains the fact that we do not have the key. Opening the door with the key takes us to darkness.

dark * gotlamp -o {win}.
dark * nolamp -o {lose}.

If we have the lamp, we win; otherwise, we lose.

Okay, so far, all we've done is transcribe the game in a funnier-looking notation. Instead of trying to make arguments about linear logic versus imperative programming and their relative scalability for programming state, I want to point out something distinctly cool we can now do.

First, let's make this a properly parsing Celf program with rule names that might be somewhat informative. I've also added a reporting mechanism, breaking slightly from the atoms-only fragment with a dependent type whose index is w if we win and l if we lose. We also set up the initial state {nokey * nolamp * start}.

Now note the query at the bottom:

#query * * * 10 init -o {report X}.

This says (letting the first three arguments to query, which I can never remember, be whatever their defaults are) that we want to run the query 10 times, starting the state with init and succeeding if the final state reports a value.

Due to the nondeterminism in forward chaining, what this does is actually randomly simulate ten complete gameplay iterations. And if we've named our rules cleverly enough, the proof terms it outputs, such as the one below, show us exactly the trace of that gameplay:

Iteration 2
Solution: \X1. {
    let {[X2, [X3, X4]]} = X1 in 
    let {X5} = start_to_den_or_cellar X4 in 
    let {X6} = den_to_cellar_lamp_or_key (X5 #1) in 
    let {X7} = cellar_to_den_or_door (X6 #1) in 
    let {[X8, X9]} = open_door_without_key [X7 #2, X2] in 
    let {X10} = cellar_to_den_or_door X8 in 
    let {X11} = den_to_cellar_lamp_or_key (X10 #1) in 
    let {[X12, X13]} = X11 #2 #1 X3 in 
    let {X14} = get_lamp X12 in 
    let {X15} = den_to_cellar_lamp_or_key X13 in 
    let {[X16, X17]} = X15 #2 #2 X9 in 
    let {X18} = get_key X16 in 
    let {X19} = den_to_cellar_lamp_or_key X17 in 
    let {X20} = cellar_to_den_or_door (X19 #1) in 
    let {X21} = den_to_cellar_lamp_or_key (X20 #1) in 
    let {X22} = cellar_to_den_or_door (X21 #1) in 
    let {X23} = den_to_cellar_lamp_or_key (X22 #1) in 
    let {X24} = cellar_to_den_or_door (X23 #1) in 
    let {X25} = open_door_with_key [X24 #2, X18] in 
    let {X26} = dark_with_lamp [X25, X14] in 
    let {X27} = report_win X26 in X27}
 #X = w

Every "#n" indicates a choice between alternatives presented between "&"s, and tuples [X, Y] are the proof terms for tensored resources (A * B). What we get here is a linear sequence of moves carried out by a player, eventually resulting in a win or lose condition. And we get ten iterations to examine, effectively automatically fuzz-testing the playable space.

What's also interesting to consider is that the variable dependencies captured here can let us reconstruct a "causality graph", which shows the structure of this proof up to concurrent equality -- something of interest to computational narratology that I'm currently working on with Gwenn Bosser.

One thing to note is that the player bounces around a lot between the cellar and the den because that's always something available to do. How can we direct proof search to more accurately simulate a goal-driven player search strategy? One end of this spectrum is complete, playable interactivity, but I'd like to explore more points along the spectrum of automation to interaction.


  1. Cool! Interested to hear more about variable dependencies and causality graphs. I wonder what other accordances logic programming offers towards understanding narrative structure.

  2. [copied over from LJ syndication feed:]

    Whoa, this is cool.

    I remember being somewhat uncertain about some of the possible ways of encoding games into linear logic that I've seen you discuss before. I very much like this encoding; it seems you're doing an interactive proof where the player makes one side's choices and the computer makes the other side's. (So far you haven't given the other side any choices; but if the player has an adversary, you could represent the adversary's choices with oplus. Then a theorem prover trying to prove "lose" can stand in for the adversary's AI, and the adversary will play perfectly.)

    I think Twine is a great way to do this, too, because it seems to be structured in a way that translates really well into your linear logic encoding. In part this comes from the way your Twine code has structured each command as a location -- i.e. "get lamp" behaves like a location the player moves to, which gives a lamp and then moves the player to the den. This means every command is a location, which simplifies the semantics.

    Is there some special thing you can easily do to the 'win' and 'lose' atoms to deal with all the extra shit left in the context at the end? It would seem cleaner somehow if you were proving 'win' or 'lose' instead of 'win * stuff'.

    The necessity of using global flags explicitly initialized to 'no' for inventory items seems like something that might be fixable, although I think I remember you talking about how annoying this is before. If you had a way of dealing with the garbage in the rest of the context, it seems like you could perhaps eliminate the 'no' variants of things. E.g.

    dark * getlamp -o win
    dark -o lose

    Then if you have the lamp, you can prove either "win", which is victory, or "getlamp * lose", which is not defeat because it's not just "lose", but a state from which you'd have to backtrack and keep searching for either "win" or "lose". (So far everything you're doing seems pretty affine -- this might be a way you could make linearity work to your advantage on the non-affine side.)

    Trying another example:

    opendoor -o {cellar}.
    opendoor * gotkey -o {dark}.

    Then if you have the key, you end up in either "dark" or "cellar * gotkey"... which is the state you started in. So we can prove "dark" if you have the key, but if you don't have the key we can't prove anything new (we just go "cellar", "opendoor", "cellar".)

    So maybe this kind of scheme works? I'm not sure about the presentation of the user interface; I guess even if proving "opendoor" without the key is useless, the theorem prover will still take "&" as meaning that it must ask the player whether to use "opendoor" or "den" to proceed. The only true issue comes up if you want to create a room where the player has only one link, but you want to give the player the link to click; then you need some way to distinguish that from a situation where you just want the prover to continue without asking the player anything.

    I guess the thing I don't know is how to rewrite the "den" rule without using the "nofoo" atoms, while ensuring the player can still only take the objects once. (This is especially important if we insist that all the player's objects be discarded to win; although it would make sense to allow the "win" and "lose" atoms to eat unused inventory; but then my stuff up above stops working? Argh.)

    1. (also copying reply over from lj)

      Is there some special thing you can easily do to the 'win' and 'lose' atoms to deal with all the extra shit left in the context at the end? It would seem cleaner somehow if you were proving 'win' or 'lose' instead of 'win * stuff'.

      Actually, Celf is linear by default - so the fact that the queries are succeeding means that in fact the only thing in the context at the end is "report(w)" or "report(l)". Of course, that's not always what we want - and Celf has a mechanism for declaring things affine, which is nice, but then you don't get the sometimes-convenient counting/conditional mechanism that requiring an empty context gets you.

      dark * getlamp -o win
      dark -o lose

      Then if you have the lamp, you can prove either "win", which is victory, or "getlamp * lose", which is not defeat because it's not just "lose", but a state from which you'd have to backtrack and keep searching for either "win" or "lose".

      The problem with this encoding is that once a choice is made between those two rules in forward-chaining, there's no turning back. So if we have (dark * gotlamp), it'll be possible to choose the (dark -o lose) rule, transition to (gotlamp * lose), transition finally to (gotlamp * report(l)), which doesn't match the query (report(X)) due to the extra junk, and so will fail (without backtracking). This *would* have the appropriate semantics if the linear rules were backward-chaining, because upon failure it would have to try a different rule, namely the (dark * getlamp -o win) one that we wanted to enforce. But then that removes the nondeterminism from proof search that got us somewhere interesting in the first place.


Post a Comment

Popular posts from this blog

Reading academic papers while having ADHD

Using Twine for Games Research (Part II)

Using Twine for Games Research (Part III)