[metadata][%
title: Formalizing Extensible Games with *Turn*
author: Scott Kovach
date: 2026-06-05
theme: light
show-slide-total: off
%]
{ WIP }
[slide][%Purpose%]
- Turn is a language for situations, not algorithms. [pause]
- A program is a set of *rules*; a rule *observes* some part of the situation, then produces some *assertion* or presents a *choice*.
{
most languages, whether objected oriented, functional etc are basically oriented towards algorithms
you write procedures, which have some inputs and an output that is connected in some particular way
usually we say that an algorithm solves a problem, like sorting or converting some markdown language into html, and that problem is understood upfront
games dynamics though are not a solution to a problem
the basic thing about situations is that if I have one situation here, and another there, there is always a composite of the two
maybe they unfold independently or maybe the overlap in some way, but the interesting thing about them is how they unfold depending on the participants choices
relation
the rest of the talk will be about unpacking what I mean by observation, assertion, and choice and how they fit together as language features
}
[slide][%Why?%]
- I really like *Spirit Island* and other games like *MtG*, *Dominion*, *Slay the Spire*, etc.
[pause]
- These games are extremely *extensible*, and formalizing them *naturally* is a legitimate challenge.
{
they have a kind of modularity, but no encapsulation: basically anything that "happens" could be the target of modification by another rule
observational equivalence for this kind of program is very discerning
}
[slide][%Examples%]
- **Augmentation/Replacement**
- *While this card is In Play, during your usual Draw step, draw an extra Card.*
- *During an opponent's Draw step, you may reveal this to prevent their Draw.*
[pause]
- **Reified Time/Causation**
- *If you drew a card this turn...*
- *The next time an Invader is Destroyed in target Land, 1 Fear*.
- *Whenever Adder deals damage...*
[pause]
- **Aggregation**
- *... a land containing 2 or more X ...*
- *If you drew no cards this turn...*
[pause]
- **Complex Choice**
- *Choose a Coastal Land adjacent to a Land containing two or more Invaders*
[slide][%Imperative + Logic Programming%]
[pause]
[code][%
edge X Y, ^path X Y
edge X Y, path Y Z, ^path X Z [pause]
~setup; ~turn
[pause]
setup
~connect a b; -- connect permanently
~connect b c
[pause]
connect X Y, +edge X Y
[pause]
turn
~temp-connect c d; -- connect temporarily [pause]
turn
temp-connect X Y;
^edge X Y
%][timeline]
{ bar vs fact (transient, indelible) }
[slide][%Atoms%]
We call the basic constituent of a situation an *atom* (or a *tuple* if it contains no variables).
[code][%
turn T -- "T is a turn"
card C -- "C is a card"
card:name C pot-of-greed -- "the name of C is pot-of-greed"
%]
[pause]
(variables are capitalized; symbols lower-case)
{
tuples are used both for intervals of time and data
":-" are normal id characters
TODO: add moment/interval diagram in between
}
[slide][%Intervals%]
Every tuple occupies an interval of time.
We write [%~foo%] to assert that [%foo%] takes place in a fresh bounded interval.
[code][%
~a
~b
~c
%][timeline]
[slide][%The Now%]
A query is a sequence of atoms. It describes an interval in time, *the now*,
reading from top to bottom:
[code][%
turn T -- during some Turn... [pause]
play-card C -- a card is played... [pause]
is-action C -- that is an action... [pause]
~activate C -- so activate the card.
%]
{
this is the key idea of the language:
every tuple has an interval attached
a conjunction of atoms only match tuples that overlap
the interval shrinks as you read through the rule
i'll have a diagram in a moment
}
[slide][%Kinds of Assertion%]
- [%~%] (*episode*): creates a new interval contained within now
- [%+%] (*fact*): creates a new interval (left, Top), with left contained in now, extending indefinitely forward in time
- [%^%] (*property*): sets the interval equal to now
{
each tuple has two moments attached (start, end) that define an interval
the moments are symbolic; the only thing we know about their ordering is what's implied by this slide
so if two rules independently assert episodes within a `turn`, they don't overlap because their endpoints are not comparable
}
[slide][%Activating a Rule%]
[code][%
-- Reminder: the rule we want to trigger
-- turn T, play-card C, is-action C, ~activate C [pause]
+is-action C -- create an action card (fact) [pause]
~turn T -- create a Turn (after `action` begins) (episode) [pause]
~play-card C -- play the card (during that turn) (episode)
-- re-introduce the rule... [pause]
turn T, play-card C, is-action C, ~activate C
%][timeline]
[pause]
(inside a query, all atoms must overlap)
{
commutative
so, maybe this looks like a usual datalog program; there's a query and an implication
logic/constraint based approaches to game language seem to have this defect:
they talk about small steps, like what happens across one turn
this is a bad fit for games with complex turns containing many sequences of actions
}
[slide][%Sequencing%]
[code][%
~game
[pause]
game, ~turn
[pause]
turn
( ~action-phase );
( ~buy-phase );
( ~cleanup-phas ) -- these editors are live
%][timeline]
[slide][%The now(s)%]
- Sometimes we *do* need to talk about non-overlapping intervals
within the span of one rule (e.g. sequencing, past tense).
- We use a *sub-rule* [%(...)%] to temporarily modify the now.
[code][%
-- "If you play a card you drew this turn, ..." [pause]
turn T
( draw-phase, draw-card C ) -- "drew C" [pause]
action-phase, play-card C -- "play C" [pause]
~do-something
[pause]
~turn T, (~draw-phase); (~action-phase)
draw-phase, ~draw-card some-card
action-phase, ~play-card some-card
%][timeline]
{ }
[slide][%Co-routines everywhere%]
Goal: assert [%d%] using this rule (*no shortcuts please*):
[code][%
a, ~b, c, ~d
%][timeline]
{ puzzle }
[slide][%Why Co-routines everywhere?%]
{ point about natural language implicature, switch statement }
*When you activate [%dream%], Gain a Power.*
*Then, if you Forgot [%dream%], Play the Gained Power.* [pause]
[code][%
activate It, card:name It dream [pause]
( ~gain-power
(forget It)
(gain New)
); ~play-power New
[pause]
gain-power
~choose-new-power;
~forget-power
[pause]
choose-new-power
?P, !power P -- syntax explained later
~gain P -- definition elided
[pause]
forget-power
?P, !power P, !you-own P
~forget P -- definition elided
%]
[pause]
- [%activate%] treats [%forget%] and [%gain%] like return values, but they don't need to be declared as such. [pause]
- execution of [%activate%] "pauses" while rules matching [%gain-power%] resolve
[slide][%Aggregates%]
*your score is the sum of...*
*if you gained no cards this turn...* [pause]
- Aggregates are **local**. [pause]
- Aggregation can implement **state**.
[slide][%Temporal Aggregates for Free%]
[code][%
~act equip-armor; ~act raise-shield; ~act cower [pause]
#agg defense * -> sum -- let's ignore this for a moment...
act equip-armor, +defense you -> 2
act raise-shield, ^defense you -> 3
[pause]
act _, ~check-defense you
[pause]
check-defense X, defense X -> Y, ^player:defense X Y
%][timeline]
[slide][%Where Am I?%]
[pause] Answer: Santa Cruz
[pause]
- Where is *that thing*? [pause]
- Answer: *wherever we last put it* [pause]
- What is the value of a variable?
[slide][%Aggregation: Last Position%]
[code][%
~game
~step here;
~look;
~step there;
~look;
[pause]
-- declare unary aggregate relation `at`
#agg at * -> last
[pause]
-- We use `step` to move `me` around...
step L, +at me -> L
[pause]
-- and `look` to observe its current location.
look, at me -> L, ~print L
%][timeline]
[slide][%Choice%]
- A rule set is compiled into a pure monotone logic program.
- With no side effects, how can we handle I/O? [pause]
- Inputs: ordinary facts within a distinguished relation
- Outputs: ordinary facts within distinguished relations
- Constraints?
[slide][%Choices are Queries%]
- *Choose a Coastal Land adjacent to a Land containing two or more Invaders* [pause]
[code][%
?L
!(coastal L, adjacent L L', land:invader-count L' X, le 1 X)
%]
[slide][%Choice%]
- Given a set of past decision tuples, this LP computes a set of choices to be made.
- The choice set is represented by a query.
- The query, evaluated at the right moment, matches valid choices.
[slide][%Choice%]
[code][%
choose-card
? Card -- introduces *choice variable*
! card Card -- asserts that any valid decision must be a `card`
~ it Card -- a handle for other queries to grab onto
%]
[slide][%Composable Choice%]
Other rules can independently refine the choice:
[code][%
choose-card
?Card
!card Card
~it Card
[pause]
-- If *Earthquake* is active:
-- when choosing a card, it must be *sturdy*. [pause]
earthquake, choose-card, it C
!sturdy C
%]
[pause]
... that's it!
[slide][%Composable Choice%]
There might be multiple ways for a card to be *sturdy*:
[code][%
+card shelter
+sturdy shelter -- it is a fact that Shelter is sturdy
[pause]
-- "If at least two cards have been
-- played this turn, *Trading Post* is sturdy
turn
( play-card _, play-card-count -> N, le 2 N )
^sturdy trading-post
%]
[slide][%Conclusion: Semantics Summary%]
- A program is a set of rules
- Each rule compiles independently to a monotone logic rule
[pause]
- Computing the least fixpoint of a program yields a set of *obstructions*:
- an aggregation to perform
- a choice to present
- These are exactly the operations that can be non-monotone or interact with the outside world.
[pause]
- Resolving the earliest obstruction allows the program to advance, which is done by simply re-running it from scratch
[slide][%Extras%]
[slide][%Now Stack in Detail%]
[code][%
~t -- <t, t>
( ~a -- <a, a>
); -- a>, t>
( ~b -- <b, b>
); -- b>, t>
%][timeline]
[slide][%last%]
- [%last(a, b) := b%]
- A (non commutative) aggregate function is applied to values in temporal order.
[pause]
[code][%
#agg at * -> last
-- Explanation:[pause]
-- #agg ... -- Directive declaring an accumulated relation[pause]
-- #agg at ... -- named *at*[pause]
-- #agg at * ... -- taking one argument of any type[pause]
-- #agg at * -> last -- aggregated by *last* (?)
%]
[slide][%Making Time%]
- Each tuple needs a pair of fresh *moment* values (its start and stop)
- We construct these deterministically from its context
- This has an unanticipated benefit: the full causal history of a moment or entity is present in its id [pause]
- This method is essentially skolemnization
- "Execution as Data": each entity includes (recursively) its full causal past, starting from the rule+variable substitution that directly created it and going back to top-level assertions
[slide][%Why "Co-routines" everywhere?%]
Step 2: assert [%b%] and [%d%] using the rules:
[code][%
a, ~b
b, c, ~d
%][timeline] [pause]
(this slide is a live demo)
[slide][%"Co-routines" everywhere%]
- The split is semantics preserving at the individual rule level
- [%a, ~b, c, ~d%] -> [%a, ~b%] + [%b, c, ~d%]
- We ensure that the match on [%b%] matches *only* the locally asserted [%b%] (not any other [%b%] from another rule)