Modeling gameplay in Celf, Part 2: Simulating Interactivity

Where I last left off, I gave a toy example of using Celf to specify a game's causal structure, summarized by the following ruleset:
start_to_den_or_cellar : start -o {den & cellar}.
den_to_cellar_lamp_or_key : den -o 
        {cellar
         & (nolamp -o {getlamp}) 
         & (nokey -o {getkey})}.
get_lamp : getlamp -o {gotlamp * den}.
get_key : getkey -o {gotkey * den}.
cellar_to_den_or_door : cellar -o {den & opendoor}.
open_door_without_key : opendoor * nokey -o {cellar * nokey}.
open_door_with_key : opendoor * gotkey -o {dark}.
dark_with_lamp : dark * gotlamp -o {win}.
dark_without_lamp : dark * nolamp -o {lose}.
init : type = {nokey * nolamp * start}.
As presented, this is effectively "half a game", with no delineation between player choice and game logic -- a fact that allowed us to randomly sample the space of all possible play sequences by querying any final gameplay state -- but that's ultimately uninformative about interactivity.

The key idea of the transformation I'll outline in this post is that we can delineate the boundary between game and player using two atoms treated as "signals", one corresponding to a choice or query from the player (think "event handling") and one corresponding to the end of the game's internal computation, returning control to the player (or, in a more complex setting, to a renderer or printing mechanism).

Each rule that handles a player control will have an extra guard premise cur_act(A) for an action A corresponding to that rule, and each rule that returns control to the player will simply issue a tick, which will be handled by a rule serving as proxy between game and player.

(Edit: I don't know why the formatting insists on being terrible for the rest of the code here. The final, complete text can be referred to in twine-interact.clf on Github.)

As a first pass, we need to disentangle all of the &'d-together choices and present them as separate rules (each of which will get its own guard).
start_to_den : start -o {den}. 
start_to_cellar : start -o {cellar}.
den_to_cellar : den -o {cellar}.
den_to_lamp : den * nolamp -o {getlamp}.
den_to_key : den * nokey -o {getkey}.
get_lamp : getlamp -o {gotlamp * den}.
get_key : getkey -o {gotkey * den}.
cellar_to_den : cellar -o {den}.
cellar_to_door : cellar -o {opendoor}.
open_door_without_key : opendoor * nokey -o {cellar * nokey}.
open_door_with_key : opendoor * gotkey -o {dark}.
dark_with_lamp : dark * gotlamp -o {win}.
dark_without_lamp : dark * nolamp -o {lose}.
Next, we'll specify the allowable player actions. (The ' symbol is just an identifier convention I'm using to distinguish actions; it has no special meaning in Celf.) The rules in green have been modified to only fire when their corresponding action is current. Omitting added type declarations, this is all that's changed:
start_to_dencur_act 'starttoden * start -o {den}.
start_to_cellarcur_act 'starttocellar * start -o {cellar}.
den_to_cellarcur_act 'dentocellar * den -o {cellar}.
den_to_lampcur_act 'getlamp * den * nolamp -o {getlamp}.
den_to_keycur_act 'getkey * den * nokey -o {getkey}.
get_lamp : getlamp -o {gotlamp * den}.
get_key : getkey -o {gotkey * den}.
cellar_to_dencur_act 'cellartoden * cellar -o {den}.
cellar_to_doorcur_act 'cellartodoor * cellar -o {opendoor}.
open_door_without_key : opendoor * nokey -o {cellar * nokey}.
open_door_with_key : opendoor * gotkey -o {dark}.
dark_with_lamp : dark * gotlamp -o {win}.
dark_without_lamp : dark * nolamp -o {lose}.
The job of cur_act is to serve as a sort of "time-varying value" determined by a sequence of actions that can be specified separately. We can encode that sequence as a relation between a natural number N and an action A, saying that the Nth action is A. Here's an example of an action sequence:

% 'starttoden, 'getlamp, 'getkey, 'dentocellar, 'cellartodoor.
act0 : nth_act z 'starttoden.
act1 : nth_act (s z) 'getlamp.
act2 : nth_act (s (s z)) 'getkey.
act3 : nth_act (s (s (s z))) 'dentocellar.
act4 : nth_act (s (s (s (s z)))) 'cellartodoor.
Now we need to connect cur_act to this table. Let's try to be modular by putting it in a single rule:
next_act : cur N * nth_act N A -o {cur_act A * cur (s N)}.
However, this approach poses a problem -- it's not keeping our code synchronized the way we intend. Imagine initializing the context with cur z -- this rule could fire until we'd loaded every action into the context without actually running the game code!

My solution is to add another guard premise. While cur_act passes control from player to game, this one, which I call tick should just pass it back in the other direction, where the next_act rule serves as a proxy for the player.
next_act : tick * cur N * nth_act N A -o {cur_act A * cur (s N)}.

Now we need to do one more global pass on the game logic, issuing a tick at the end of every control sequence. For movement rules, this is just immediately after receiving the action. For rules that involve more complicated checks and have multiple cases (like open_door), this occurs at the end of each branch:
start_to_den : cur_act 'starttoden * start -o {den * tick}.
start_to_cellar : cur_act 'starttocellar * start -o {cellar * tick}.
den_to_cellar : cur_act 'dentocellar * den -o {cellar * tick}.
den_to_lamp : cur_act 'getlamp * den * nolamp -o {getlamp}.
den_to_key : cur_act 'getkey * den * nokey -o {getkey}.
get_lamp : getlamp -o {gotlamp * den * tick}.
get_key : getkey -o {gotkey * den * tick}.
cellar_to_den : cur_act 'cellartoden * cellar -o {den * tick}.
cellar_to_door : cur_act 'cellartodoor * cellar -o {opendoor}.
open_door_without_key : opendoor * nokey -o {cellar * nokey * tick}.
open_door_with_key : opendoor * gotkey -o {dark}.
dark_with_lamp : dark * gotlamp -o {win}.
dark_without_lamp : dark * nolamp -o {lose}.

For fun, we can load up our reporting mechanism with the number of steps we took, then load up the initial context and do a query:
report_win : win * cur N -o {report w N}.
report_loss : lose * cur N -o {report l N}.
init : type = {nokey * nolamp * start * cur z * tick}.
#query * * * 1 init -o {report END NSTEPS}.

Yielding the solution
Solution: \X1. {
    let {[X2, [X3, [X4, [X5, X6]]]]} = X1 in
    let {[X7, X8]} = next_act [X6, [X5, act0]] in
    let {[X9, X10]} = start_to_den [X7, X4] in
    let {[X11, X12]} = next_act [X10, [X8, act1]] in
    let {X13} = den_to_lamp [X11, [X9, X3]] in
    let {[X14, [X15, X16]]} = get_lamp X13 in
    let {[X17, X18]} = next_act [X16, [X12, act2]] in
    let {X19} = den_to_key [X17, [X15, X2]] in
    let {[X20, [X21, X22]]} = get_key X19 in
    let {[X23, X24]} = next_act [X22, [X18, act3]] in
    let {[X25, X26]} = den_to_cellar [X23, X21] in
    let {[X27, X28]} = next_act [X26, [X24, act4]] in
    let {X29} = cellar_to_door [X27, X25] in
    let {X30} = open_door_with_key [X29, X20] in
    let {X31} = dark_with_lamp [X30, X14] in
    let {X32} = report_win [X31, X28] in X32}
 #END = w
 #NSTEPS = s !(s !(s !(s !(s !z))))

The point of all this was (1) to demonstrate how to simulate tightly-controlled interaction in a parametric way (while this was a global transformation of the original program, the only part that depended on the specific action sequence was the table representing that sequence); (2) to show that the very specific, structural use of the "control-passing" atomic formulae suggests, as with "design patterns", a possible useful extension to the language -- specifically, one that lets us express the programmer intent of separate modules or processes, and lets us check that that intent is preserved.

Comments

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)