\(\newcommand{vrt}[2]{\left ( \begin{array}{l} #1 \\ #2 \end{array} \right )}\) \(\newcommand{defeq}{\overset{\mathit{def}}{=}}\) \(\newcommand{am}{\text{a.m.}}\) \(\newcommand{pm}{\text{p.m.}}\)

Overview

This post is a continuation of Towards a Mathematical Model of Computer Games. Unlike that post, this one is focused on mathematical rigor rather than motivation. Rather than defining a mathematical model of a MegaZeux game, it pursues the less ambitious goal of defining a mathematical model of tic-tac-toe.

The game tic-tac-toe shares some common characteristics with a MegaZeux game. It involves two players. Each of these players is analogous to a MegaZeux robot, and the game board is analogous to the MegaZeux environment. The players repeatedly make requests to the board to alter its state. The board may or may not honor these requests depending on whether they obey its “laws of physics”.

The two players together with their environment will form a closed system, i.e. a set \(\mathit{GameState}\) with an update function

\[\mathit{nextState} : \mathit{GameState} \to \mathit{GameState}\]

Or equivalently, a set of two functions, using \(1 = \{ \ast \}\) as both the input and output sets:

\[\mathit{output} : \mathit{GameState} \to 1\]

and

\[\mathit{nextState} : 1 \times \mathit{GameState} \to \mathit{GameState}\]

We will construct this closed system out of open systems such as the players. The players are open systems that take observations of the board state as inputs and produce move choices as outputs. As a rough first approximation, a player can be diagrammed as follows:

The above system is considered open because its input and output are not one-element sets; they contain actual information that must be received from and sent to unspecified destinations. Each turn, an element of BoardState is received as input. The player uses the current board state, possibly along with the player’s own internal state, to decide a move to submit to the board.

Now, let’s develop a formalism that allows us to compose complex systems from simpler systems.

Lenses

We model open systems mathematically using a construct called lenses. I learned about lenses from Categorical Systems Theory, which I highly recommend. In the interest of self-containment, I will rehash the fundamentals of lenses now.

Definitions

Definition

An arena \(\vrt{A^-}{A^+}\) is a pair consisting of two sets \(A^-\) and \(A^+\).

Definition

A lens \(\vrt{f^\sharp}{f} : \vrt{A^-}{A^+} \leftrightarrows \vrt{B^-}{B^+}\) is a pair consisting of two functions:

  • A passforward function \(f : A^+ \to B^+\)
  • A passback function \(f^\sharp : A^+ \times B^- \to A^-\)

The arena \(\vrt{A^-}{A^+}\) is called the domain of \(\vrt{f^\sharp}{f}\) and the arena \(\vrt{B^-}{B^+}\) is called the codomain of \(\vrt{f^\sharp}{f}\).

The passforward function of a lens can be viewed as sending information “downstream” and the passback function can be viewed as sending information “upstream”. One particularly important type of lens is a discrete dynamical system.

Definition

A discrete dynamical system (or dynamical system for short) is a lens of the form

\[\vrt{\mathit{nextState}}{\mathit{output}} : \vrt{\mathit{State}}{\mathit{State}} \leftrightarrows \vrt{\mathit{In}}{\mathit{Out}}\]

That is, a dynamical system is a lens whose domain is an arena of the form \(\vrt{\mathit{State}}{\mathit{State}}\) for some set \(\mathit{State}\).

Above, we consider \(\mathit{State}\) the type of our dynamical system’s internal state, \(\mathit{In}\) the type of its input, and \(\mathit{Out}\) the type of its output. Expanding the definition of lens, we see that

  • \(\mathit{nextState} : \mathit{State} \times \mathit{In} \to \mathit{State}\) is a function that takes a pair of a “current” state and an input to a “next” state.
  • \(\mathit{output} : \mathit{State} \to \mathit{Out}\) is a function that takes a state to an output.

This matches the intuitive structure of game engines that I presented previously. Those familiar with digital logic may know the distinction between Moore machines and Mealy machines. The output of a Mealy machine may depend both on its input and its current state, whereas the output of a Moore machine may only depend on its current state. In this sense, a dynamical system is like a Moore machine rather than a Mealy machine: before its input can affect its output, it must store the input in its state as an intermediate step. This can be a bit awkward sometimes, but it’s not a fundamental problem.

A dynamical system \(S : \vrt{\mathit{State}_S}{\mathit{State}_S} \leftrightarrows \vrt{\mathit{In}_S}{\mathit{Out}_S}\) can be depicted as follows.

Figure 1

Note that the set \(\mathit{State}_S\) does not appear in the diagram, because it does not affect the systems that \(S\) interacts with.

If the codomain of one lens matches the domain of another then we can compose them together.

Definition

Given lenses \(\vrt{f^\sharp}{f} : \vrt{A^-}{A^+} \leftrightarrows \vrt{B^-}{B^+}\) and \(\vrt{g^\sharp}{g} : \vrt{B^-}{B^+} \leftrightarrows \vrt{C^-}{C^+}\) their composite \(\vrt{g^\sharp}{g} \circ \vrt{f^{\sharp}}{f}\) is defined as \(\vrt{h^\sharp}{h} : \vrt{A^-}{A^+} \leftrightarrows \vrt{C^-}{C^+}\), where

  • \(h\) is defined as the function composite \(g \circ f\)
  • \(h^\sharp\) is defined such that \(h^\sharp(a^+, c^-) \defeq f^\sharp(a^+, g^\sharp(f(a^+), c^-))\)

We also have a parallel composition operator on lenses.

Definition

Given two lenses \(\vrt{f^\sharp}{f} : \vrt{A^-}{A^+} \leftrightarrows \vrt{B^-}{B^+}\) and \(\vrt{g^\sharp}{g} : \vrt{C^-}{C^+} \leftrightarrows \vrt{D^-}{D^+}\) we define their parallel product \(\vrt{f^\sharp}{f} \otimes \vrt{g^\sharp}{g} : \vrt{A^- \times C^-}{A^+ \times C^+} \leftrightarrows \vrt{B^- \times D^-}{B^+ \times D^+}\) as the lens \(\vrt{h^\sharp}{h}\), where

\[h(a^+, c^+) \defeq (f(a^+), g(c^+))\]

and

\[h^\sharp(a^+, c^+, b^-, d^-) \defeq (f^\sharp(a^+, b^-), g^\sharp(c^+, d^-))\]

Given dynamical systems

\[S : \vrt{\mathit{State}_S}{\mathit{State}_S} \leftrightarrows \vrt{\mathit{In}_S}{\mathit{Out}_S}\]

and

\[T : \vrt{\mathit{State}_T}{\mathit{State}_T} \leftrightarrows \vrt{\mathit{In}_T}{\mathit{Out}_T}\]

their parallel product

\[S \otimes T : \vrt{\mathit{State}_S \times \mathit{State}_T}{\mathit{State}_S \times \mathit{State}_T} \leftrightarrows \vrt{\mathit{In}_S \times \mathit{In}_T}{\mathit{Out}_S \times \mathit{Out}_T}\]

can be depicted by juxtaposing the two dynamical systems:

Figure 2

Example

Here is an example of a dynamical system from Categorical Dynamical Systems. Define the set

\[\mathit{Hour} \defeq \{ 1,2,3,4,5,6,7,8,9,10,11,12 \}\]

We define a dynamical system

\[\mathit{Clock} : \vrt{\mathit{Hour}}{\mathit{Hour}} \leftrightarrows \vrt{1}{\mathit{Hour}} \defeq \vrt{f^\sharp}{f}\]

where \(f\) is the identity function

\[f(x) \defeq x\]

and

\[f^\sharp(h, \ast) \defeq \begin{cases} 1 & \text{ if } h = 12 \\ h + 1 & \text{ otherwise} \end{cases}\]

This system represents a wall clock, which takes no external input and advances one hour forward at each step.

Figure 3

Note that we don’t need to draw an incoming edge; because the input is \(1 = \{ \ast \}\), it transmits only one possible choice of value \(\ast\). So instead of receiving input from an external source, \(\mathit{Clock}\) can fabricate the value \(\ast\) at every step, knowing it is the correct choice.

The above clock does not distinguish between \(\am\) and \(\pm\) To fix this, we define a dynamical system called \(Meridiem\) that shifts between \(\am\) and \(\pm\) We first define the set \(\am/\pm \defeq \{ \am, \pm \}\) Then we define

\[\mathit{Meridiem} : \vrt{\am/\pm}{\am/\pm} \leftrightarrows \vrt{\mathit{Hour}}{\am/\pm} \defeq \vrt{f^\sharp}{f}\]

where

\[f(m) \defeq m\]

and

\[f^\sharp(\am,h) \defeq \begin{cases} \pm & \text{if } h = 11 \\ \am & \text{otherwise} \end{cases}\] \[f^\sharp(\pm,h) \defeq \begin{cases} \am & \text{if } h = 11 \\ \pm & \text{otherwise} \end{cases}\]

Now we need to “wire together” the \(\mathit{Clock}\) and \(\mathit{Meridiem}\) systems. As a first step, we take their parallel product.

\[\mathit{Clock} \otimes \mathit{Meridiem} : \vrt{\mathit{Hour} \times \am/\pm}{\mathit{Hour} \times \am/\pm} \leftrightarrows \vrt{1 \times \mathit{Hour}}{\mathit{Hour} \times \am/\pm}\]
Figure 4

To feed the output of \(\mathit{Clock}\) into \(\mathit{Meridiem}\), we use composition, which can be depicted as nesting.

Figure 5

The inner dotted box is the parallel product \(\mathit{Clock} \otimes \mathit{Meridiem}\). The outer dotted box is the fully wired system. The section between the two boxes depicts a new lens

\[\vrt{w^\sharp}{w} : \vrt{1 \times \mathit{Hour}}{\mathit{Hour} \times \am/\pm} \leftrightarrows \vrt{1}{\mathit{Hour} \times \am/\pm}\]

defined such that

\[w(h,m) \defeq (h,m)\]

and

\[w^\sharp(h, m, \ast) \defeq (\ast, h)\]

The fully wired system, which we shall call \(\mathit{Clock}'\) is then defined as

\[\mathit{Clock}' : \vrt{\mathit{Hour} \times \am/\pm}{\mathit{Hour} \times \am/\pm} \leftrightarrows \vrt{1}{\mathit{Hour} \times \am/\pm} \defeq \vrt{w^\sharp}{w} \circ (\mathit{Clock} \otimes \mathit{Meridiem})\]

Combinational Systems

Suppose that we want to translate the output of the \(\mathit{Clock}'\) system above to 24-hour time, also known as “military time”, instead of \(\am/\pm\) Let

\[\mathit{Hour24} \defeq \{ 0, 1, 2, \ldots, 23 \}\]

We must “post-compose” a function \(f : \mathit{Hour} \times \am/\pm \to \mathit{Hour24}\) after the \(\mathit{Clock}'\) system, where \(f\) is defined as follows:

\[f(h, \am) \defeq \begin{cases} 0 & \text{if } h = 12 \\ h & \text{otherwise} \end{cases}\] \[f(h, \pm) \defeq \begin{cases} 12 & \text{if } h = 12 \\ 12 + h & \text{otherwise} \end{cases}\]

Such a post-composition is depicted below

Figure 6

Note that \(f\) is just a function, not a dynamical system with state.

In digital logic, a circuit that stores state is called sequential, whereas a circuit that merely computes a function is called combinational. The function \(f\) above, having no internal state, is combinational. We can post-compose a dynamical system by a combinational system using lens combination.

Without loss of generality, let \(\mathit{Out}_0 \defeq \mathit{Hour} \times \am/\pm\), let \(\mathit{Out}_1 \defeq \mathit{Hour24}\), and let \(\mathit{In} \defeq 1\). Then this lens should translate the system’s output using a function \(f : \mathit{Out}_0 \to \mathit{Out}_1\) but leave the input \(\mathit{In}\) unchanged. Hence we define it as

\[\vrt{\pi_1}{f} : \vrt{\mathit{In}}{\mathit{Out_0}} \leftrightarrows \vrt{\mathit{In}}{\mathit{Out}_1}\]

where \(\pi_1 : \mathit{Out_0} \times \mathit{In} \to \mathit{In}\) is the projection of the second component \((o,i) \mapsto i\).

We then obtain our military time clock as

\[\mathit{MilitaryClock} \defeq \vrt{\pi_1}{f} \circ \mathit{Clock'}\]

Demultiplexors

Imagine a turn-based board game with multiple players. At each turn, we want to provide exactly one player with the state of the board so that they can make an informed move. The challenge is to send a payload value along a different wire depending on some selector value, and to send “nothing” along all other wires. More precisely, we need a combinational circuit, called a demultiplexor, that takes two inputs. Letting each bold natural number \(\mathbf{n}\) denote the set of natural numbers less than it, i.e. \(\mathbf{n} \defeq \{ 0, 1, \ldots, n-1 \}\), these inputs are:

  • The payload, whose type \(\mathit{Payload}\) may vary
  • The selector of type n + 1, deciding which, if any, of \(n\) output destinations to transmit the payload to

The demultiplexor circuit has \(n\) different output wires. Their type is not quite \(\mathit{Payload}\); each wire may contain a value of type \(\mathit{Payload}\) or, if it has not been selected, it may contain a \(\ast\) of type \(1\).

To express the set of values that each belong to exactly one of the disjoint sets \(\mathit{Payload}\) or \(1\) we need to use a set theoretic operation called the sum, which is not as well known as its evil twin the Cartesian product.

Definition Given sets \(X\) and \(Y\), their sum \(X + Y\) is defined as

\[X + Y \defeq \{ (0,x) \mid x \in X \} \cup \{ (1,y) \mid y \in Y \}\]

By tagging values with either \(0\) or \(1\), we ensure that the elements of the two operands are treated as mutually exclusive; it may be instructive to compare the set \(1 = 1 \cup 1\) with the set \(1 + 1\). Each of a demultiplexor’s output wires then has type \(\mathit{Payload} + 1\).

Recall that, if \(X\) is a set, then \(X \times \overset{n}{\cdots} \times X\) is the set of \(n\)-ary tuples \((x_0, \ldots, x_{n-1})\). We are now ready to formally define the notion of demultiplexor circuits.

Definition Let \(\mathit{In}\) and \(X\) be sets, and let \(n\) be a natural number. The demultiplexor \(\mathit{demux}(\mathit{In}, X, n)\) is the combinational lens

\[\vrt{\pi_1}{f} : \vrt{\mathit{In}}{X \times (\mathbf{n + 1})} \leftrightarrows \vrt{\mathit{In}}{(1 + X) \times \overset{n}{\cdots} \times (1 + X)}\]

where \(f : X \times (\mathbf{n + 1}) \to (1 + X) \times \overset{n}{\cdots} \times (1 + X)\) is defined such that

\[f(x, m) \defeq (t_0, \ldots, t_{n-1}) \\ \text{ where } t_i = \begin{cases} (1,x) & \text{ if } m = i \\ (0,\ast) & \text{ if } m \neq i \end{cases}\]

and \(\pi_1 : (X \times (\mathbf{n + 1})) \times \mathit{In} \to \mathit{In}\) is the second projection function

\[\pi_1((x, m), i) \defeq i\]

Thus, the demultiplexor \(\mathit{demux}(\mathit{In}, X,n)\) allows us to either

  • Select some \(m \in \mathbf{n}\) such that \((1,x)\) is transmitted along the \(m^{\mathit{th}}\) output wire and \((0,\ast)\) is transmitted along all other output wires.
  • Or, if \(m = n\), then transmit \((0,\ast)\) along all wires.

\(\mathit{demux}(\mathit{In}, X,n)\) is depicted below, where we’ve elided all but the first and last of the \(n\) output wires.

Figure 7

Note that \(\mathit{demux}(\mathit{In}, X, n)\) can only be post-composed with a dynamical system whose input set is \(\mathit{In}\). When a demultiplexor is post-composed with a system \(S : \vrt{\mathit{State}_S}{\mathit{State}_S} \leftrightarrows \vrt{\mathit{In}_S}{\mathit{Out}_S}\), we elide the \(\mathit{In}\) argument from \(\mathit{demux}\), instead inferring from context that \(\mathit{In} = \mathit{In}_S\):

Figure 8

Multiplexors

Assume \(n\) inputs of type \((1 + X)\), and further assume that we expect at most one input to have the form \((1, x)\) while the others have the form \((0,\ast)\). We want a combinational lens that produces a single output of type \(1 + X\), and which forwards \((1,x)\) if a single input has the form \((1,x)\) and forwards \((0,\ast)\) otherwise.

Definition The multiplexor \(\mathit{mux}(\mathit{In}, X, n)\) is the combinational lens

\[\vrt{\pi_1}{f} : \vrt{\mathit{In}}{(1 + X) \times \overset{n}{\cdots} \times (1 + X)} \leftrightarrows \vrt{\mathit{In}}{1 + X}\]

where \(f : (1 + X) \times \overset{n}{\cdots} \times (1 + X) \to (1 + X)\) is defined as

\[f(t_0, \ldots, t_{n-1}) \defeq \begin{cases} t_i & \text{if there exists a unique } i \in \mathbf{n} \text{ such that } t_i = (1, x) \text{ for some } x \\ (0,\ast) & \text{otherwise} \end{cases}\]

and \(\pi_1 : ((1 + X) \times \overset{n}{\cdots} \times (1 + X)) \times \mathit{In} \to \mathit{In}\) is the second projection function

\[\pi_1((t_0, \ldots, t_{n-1}), i) \defeq i\]
Figure 9

Similar to \(\mathit{demux}\), we typically infer the \(\mathit{In}\) argument.

Figure 10

Tic-tac-toe

Now we use the dynamical system techniques described above to model the game of tic-tac-toe. We do not model any notion of a winning condition, but instead focus on the evolution of the game over time, where two agents (players) influence the environment (the board) by submitting moves in a turn-based fashion.

Overview

To model the board, we first need a notion of cell locations. Recall that each bold natural number \(\mathbf{n}\) denotes the set of natural numbers less than it. A location on a tic-tac-toe board consists of an x-coordinate and a y-coordinate, so we define the set \(\mathit{Loc}\) of locations as

\[\mathit{Loc} \defeq \mathbf{3} \times \mathbf{3}\]

We name the two players Player 0 and Player 1. Elements of the set \(\mathit{Players}\) identify players

\[\mathit{Players} \defeq \{ 0, 1 \}\]

In a typical game of tic-tac-toe, the players use the symbols \(X\) and \(O\) to mark their cells. In our version of tic-tac-toe each player uses its own symbol, either \(0\) or \(1\) to mark cells. An unmarked cell holds the symbol \(\_\). We let \(\mathit{Sym}\) denote the set of possible symbols at a cell:

\[\mathit{Sym} \defeq \{ 0, 1, \_ \}\]

The state of the board is then the set of functions from locations to symbols. We thus define the set of possible board states \(\mathit{Board}\) as

\[\mathit{Board} \defeq \mathit{Loc} \to \mathit{Sym}\]

The dynamical system underlying our tic-tac-toe game stepper is then depicted as follows:

Figure 11

It contains three yet undefined stateful subsystems: \(\mathit{Player0}\), \(\mathit{Player1}\), and \(\mathit{Environment}\). Intuitively, the game stepper advances in a periodic pattern consisting of steps of four types, in order:

  • \(\mathit{Environment}\) receives a move from \(\mathit{Player0}\) and executes its move
  • \(\mathit{Environment}\) submits the resulting board to \(\mathit{Player1}\)
  • \(\mathit{Environment}\) receives a move from \(\mathit{Player1}\) and executes its move
  • \(\mathit{Environment}\) submits the resulting board to \(\mathit{Player0}\)

In sets of the form \(1 + X\), the \(1\) component on the left is typically used to mean “inactive”. For example, on turns in which \(\mathit{Player0}\) submits its move, and on turns in which the environment submits the board to a player, \(\mathit{Player1}\) outputs \((0,\ast)\). Likewise, when \(\mathit{Environment}\) submits a board to \(\mathit{Player0}\), the demultiplexor outputs \((0, \ast)\) along the bottom channel leading to \(\mathit{Player1}\).

Note that players can submit any location to the environment as a move. However, if the cell at the submitted location is already occupied with either \(0\) or \(1\), then the \(\mathit{Environment}\) will choose not to perform the action and advance control to the next player without changing the board.

Environment

We now define the \(\mathit{Environment}\) dynamical system. Our first task is deciding its set \(\mathit{State}_{\mathit{Environment}}\) of states. First, each state should convey the current execution step type

\[\mathit{StepType} \defeq \{ \mathit{ReceiveFrom}(0), \mathit{SubmitTo}(0), \mathit{ReceiveFrom}(1), \mathit{SubmitTo}(1), \mathit{IllegalState} \}\]

The \(\mathit{IllegalState}\) element above should be used when \(\mathit{Environment}\) receives an invalid input combination (i.e. one which we have prevented it from receiving by design). For those familiar with digital logic, this is somewhat analogous to a “don’t care” value.

Additionally, the state should convey the current board. We’ve already defined the set \(\mathit{Board}\) of board states above. Hence, our full state set is defined as

\[\mathit{State}_{\mathit{Environment}} \defeq \mathit{StepType} \times \mathit{Board}\]

As figure 11 shows, the environment’s output set is

\[\mathit{Out}_{\mathit{Environment}} \defeq (1 + \mathit{Board}) \times \mathbf{3}\]

The environment’s \(\mathit{output}_\mathit{Environment} : \mathit{State}_{\mathit{Environment}} \to \mathit{Out}_{\mathit{Environment}}\) function is then defined as

\[\mathit{output}_\mathit{Environment} : \mathit{StepType} \times \mathit{Board} \to (1 + \mathit{Board}) \times \mathbf{3}\] \[\mathit{output}_\mathit{Environment}(t, b) \defeq \begin{cases} ((1, b), n) & \text{ if } t = SubmitTo(n) \\ ((0, \ast), 2) & \text{ if } t = ReceiveFrom(n) \\ ((0, \ast), 2) & \text{ if } t = IllegalState \end{cases}\]

The top two cases above are self explanatory. But when our environment is in the \(\mathit{IllegalState}\) step type, it’s not clear what to produce as output. Because really we never intend to enter \(\mathit{IllegalState}\) to begin with, it ultimately doesn’t matter what we choose to output while in \(\mathit{IllegalState}\); nonetheless, we must provide some output so that our function is fully defined. This is an awkward distraction which we will resolve in a future post.

Consulting figure 11, we see that

\[\mathit{In}_{\mathit{Environment}} \defeq 1 + \mathit{Loc}\]

For \(b \in \mathit{Board}\), we define \(b[\ell \mapsto n] \in \mathit{Board}\) as follows.

\[b[\ell \mapsto n](k) \defeq \begin{cases} b(k) & \text{if } k \neq \ell \\ n & \text{if } k = \ell \end{cases}\]

We define \(\mathit{nextState}_{\mathit{Environment}} : \mathit{State}_{\mathit{Environment}} \times \mathit{In}_{\mathit{Environment}} \to \mathit{State}_{\mathit{Environment}}\) as \(~\\\) \(\mathit{nextState}_{\mathit{Environment}} : \mathit{StepType} \times \mathit{Board} \times (1 + \mathit{Loc}) \to \mathit{StepType} \times \mathit{Board}\) \(~\\\) \(\mathit{nextState}_{\mathit{Environment}}(ReceiveFrom(n), b, (1,\ell)) \defeq \begin{cases} (SubmitTo((n+1)~\%~2), b[\ell \mapsto n]) & \text{if } b(\ell) = \_ \\ (SubmitTo((n+1)~\%~2), b) & \text{otherwise} \end{cases}\) \(~\\\) \(\mathit{nextState}_{\mathit{Environment}}(SubmitTo(n), b, (0,\ast)) \defeq (ReceiveFrom(n), b)\) \(~\\\) \(\text{and for any other } (s,b,z) \in \mathit{StepType} \times Board \times (1 + Loc) \text{ we define}\) \(~\\\) \(\mathit{nextState}_{\mathit{Environment}}(s,b,z) \defeq (\mathit{IllegalState}, b)\)

Finally, we define

\[\mathit{Environment} : \vrt{\mathit{State}_{\mathit{Environment}}}{\mathit{State}_{\mathit{Environment}}} \leftrightarrows \vrt{\mathit{In}_{\mathit{Environment}}}{\mathit{Out}_{\mathit{Environment}}} \defeq \vrt{\mathit{nextState_{\mathit{Environment}}}}{\mathit{output}_{\mathit{Environment}}}\]

Players

We define \(\mathit{Player0}\), eliding \(\mathit{Player1}\) as it is essentially the same.

The state of the player systems can be used for two purposes. First, the state must record a \(Board\) whenever it is received from the environment. That way the player can use the board to compute a move on the next turn. Second, and optionally, a player’s state can serve as its “brain” by storing information about a plan or strategy that the player is currently executing, or by storing an inferred mental model of the opposing player. We will keep things simple and decide moves in a stateless fashion, using only the current state of the board. Hence, we define

\[\mathit{State}_{\mathit{Player0}} \defeq 1 + \mathit{Board}\]

If the player’s state is \((1, b)\) then it has just received board \(b\) from the environment and is expected to submit a move on the next turn. Otherwise, the player’s state is \((0,\ast)\).

We can see from Figure 11 that

\[\mathit{In}_{\mathit{Player0}} \defeq 1 + \mathit{Board}\]

and

\[\mathit{Out}_{\mathit{Player0}} \defeq 1 + \mathit{Loc}\]

Let \(\phi : \mathit{Board} \to \mathit{Loc}\) be player 0’s “strategy” for deciding a move given the current board; instead of defining it, we leave it as a parameter to the system.

We then define

\[\mathit{output}_{\mathit{Player0}}(x) \defeq \begin{cases} (0, \ast) & \text{if } x = (0, \ast) \\ (1, \phi(b)) & \text{if } x = (1, b) \end{cases}\]

and

\[\mathit{nextState}_{\mathit{Player0}}(x, (1, b)) \defeq (1, b)\] \[\mathit{nextState}_{\mathit{Player0}}(x, (0, \ast)) \defeq (0, \ast)\]

The \(\mathit{Player0}\) dynamical system is then defined as

\[\mathit{Player0} : \vrt{\mathit{State}_{\mathit{Player0}}}{\mathit{State}_{\mathit{Player0}}} \leftrightarrows \vrt{\mathit{In}_{\mathit{Player0}}}{\mathit{Out}_{\mathit{Player0}}} \defeq \vrt{\mathit{nextState}_{\mathit{Player0}}}{\mathit{output}_{\mathit{Player0}}}\]

Putting things together

Now that all of the components of our system have been defined, we will wire them together using the lens composition technique, expressing the system as a whole as a mathematical expression.

As a first step, we note that our system can be obtained by wiring together the two dynamical systems named \(A\) and \(B\) displayed below.

Figure 12

Where

\[A \defeq \mathit{mux}(\mathit{Move}, 2) \circ (\mathit{Player0} \otimes \mathit{Player1})\]

and

\[B \defeq \mathit{demux}(\mathit{Board}, 2) \circ \mathit{Environment}\]

Next, we take their parallel product \(A \otimes B\), which is depicted below.

Figure 13

Finally, to close off our system, we must wire together the two components using lens composition, similar to how we wired together the \(\mathit{Clock}\) and \(\mathit{Meridiem}\) systems above.

We use the wiring lens

\[\vrt{w^\sharp}{w} : \vrt{(1 + \mathit{Board}) \times (1 + \mathit{Board}) \times (1 + \mathit{Loc})}{(1 + \mathit{Loc}) \times (1 + \mathit{Board}) \times (1 + \mathit{Board})} \leftrightarrows \vrt{1}{1}\]

where

\[w(\ell, b_0, b_1) \defeq \ast\]

and

\[w^\sharp(\ell, b_0, b_1, \ast) \defeq (b_0, b_1, \ell)\]

Our complete system is then equal to:

\[\vrt{w^\sharp}{w} \circ (A \otimes B)\]

Conclusion

Evaluating the Dynamical Systems Formalism

It’s worth taking a step back to ask whether the lens-based dynamical systems formalism is an appropriate tool for modelling turn-based computer games. The ability of lenses to represent cyclic data flow, from the players to the environment and back to the players, is essential. Additionally, lens based dynamical systems make it easy for us to encapsulate data, restricting players to mutate only their own mental state, and restricting the environment to only mutate the physical world.

One drawback is that, due to the inherently concurrent nature of lens-based dynamical systems, we’ve needed to insert machinery for synchronization which has little to do with dynamics of our turn-based games. For example, giving most wires the type \(1 + X\) instead of \(X\) is a distraction, but a necessary one in this formalism.

Looking Ahead

Recall that defining \(\mathit{nextState}_\mathit{Environment}\) required us to handle the awkward \(\mathit{IllegalState}\) case — a state that our system should never actually reach. In the next post, we’ll address this by introducing partial lenses and partial dynamical systems, which let us formally distinguish between expected and unexpected behavior without cluttering our definitions.

Next: Partial Systems