Describing Tic-Tac-Toe Using Dependent Sum Types

tic-tac-toe-dependent-types.md

Problem

Can we use Type Theory to show that a given Petri-Net correctly models a game of Tic-Tac-Toe?

Terms

• Entropy (information theory)
• Big O Complexity
• Dependent Sum Types
• Petri-Net
• Sets & Abstract Data Types

Related

• Previous post

Method

Given a Petri-Net to model a game of Tic-Tac-Toe.

We hope to demonstrate that it describes both the exponential complexity of the algorithm used to compute the state-space and the factorial complexity of the state-space output.

Here the output of the system generates represent every posssible game of Tic-Tac-Toe.

Big O notation

• O(c^{n}) - exponential complexity

  • Finding the (exact) solution to the travelling salesman problem

• O(n!) - factorial complexity

  • Solving the travelling salesman problem via brute-force search

From the wikipedia entry on Game Complexity

We see that Tic-Tac-Toe has a Game-Tree complexity of 5 (though we do not derive this information in this post)

Type <-> Set Equivilance

We attempt to define a set of abstract data types in an effort to represent the entropy of the state space as it is described by mathematical sets.

In a way we are focusing on 'decision events' rather than the 'atoms' of the problem space.

Also, because we are modeling completed games we are free to describe the Game Tree or the State Space without having to use the original branching complexity that describes gameplay for 2 players.

Model as Single Player

Instead we model the game as a single player game.

Where it can be explained as:

a game where a player pulls 9 marbles out of a bag

• the bag contains 18 marbles
• each marble is marked with numbers 1-9
• additionally each marble is marked with 'X' or 'O'
• there are an equal number of 'X' and 'O' marbles
• for each set of 'X' and 'O' marbles there is no duplicate numbering
• for the first move of the game only 'X' is valid
• on each turn the marble drawn should invert the X/O selection of the previous turn
• on each turn marbles marked with numbers that have previously been drawn are invalid

Petri-Net

Initial game state:

Example after 5 Moves:

See above: consider that the (incomplete) game state can described as a set of moves:

Move Sequence: ('X,1,1', 'O,2,0', 'X,0,0', 'O,0,1', 'X,2,2')

Converting To Sets

Because we can imagine using the above Petr-Nets to play a game of Tic-Tac-Toe it is easy to make an intuitive leap to see that it correctly describes the moves of the game.

However, we intend to show how that mathematical complexity of the game is fully described by the input net.

To do so we will demonstrate how information for the 'full' solution set can be derived from the information contained in the graph when combined with the possible set of 'game inputs'

Game Output

The output of a single game can be described by the 9 input moves that created it.

NOTE: that Big O deals with probabilty and worst case complexity.

Even though the above game already has a winner - we delare that every game in the state space has has exactly 9 Moves.

single game move sequence: (1, 2, 3, 4, 5, 6, 7, 8, 9) # size => 9

Game Inputs

Since game inputs are modeled as a set of moves we can represent the possible game actions as a set:

game actions: ( 00, 01, 02, 10, 11, 12, 20, 21, 22 )  # size => 9

NOTE: that the encoding used to describe game actions exactly corresponds to the information needed to indicate which square on the tic-tac-toe board is being played

Game State

Addtionally we need to be able to describe the 'state space' of the board:

partial states: ( 00, 01, 02, 10, 11, 12, 20, 21, 22, EMPTY) # size => 10

NOTE: that here we also include the EMPTY set - as a way to describe the initial state of the board.

Due to the design of Petri-Nets, the transition between states is modeled w/o enumerating the entire state space. Because of this, we need a way to describe the opening move of the game: Empty => ( move1 )

Encoded Symbols

Finally we introduce the set of all symbols used to describe the game:

symbols/types: ( EMPTY, 1, 2, 3, 4, 5, 6, 7, 8, 9, x, y, X, O ) # size => 14

Encoded Information

Notice: that we also include these other non-numeric symbols that are used during encoding:

'x', 'y', 'X', 'O'

These symbols are used to encode information into the Petri-Net, and so must be included when trying to calculate total entropy of the system.

Conclusion

If we have made the proper choices when selecting symbols and relations between sets, We should be able factor out the computational complexity of the system by using it's Big O bounded function.

As we've previously stated: Tic-Tac-Toe has a branching exponent of '5' So we can describe the compuational complexity using O(c^{n}).

O(c^{n}) => 2^5

Also note: - we've also chosen '2' as the base. This is a reflection of the choices we see modeled by the Petri-Net.

Notice, that each transition from the model can be viewed as a choice to mark a square 'X' or 'O'.

The state space of Tic-Tac-Toe is has factorial complexity. So we can describe the complexity of the set of all games using: O(n!).

O(n!) => 9!

If we combine these systems we get a an expression of the remaining Entropy of the system:

9!/2^5 = 11340

This remainder should represent the mathematical complexity for a Type system that relates both the state-space and problem-space.

9! / 2 ^ 5 = 9 * 9 * 10 * 14

As shown above entropy is consistent between the set of all solutions and the set of all input factors. This seems to only hold true if you are using the correct branching factor.

Thus, we have confirmed that the information encoded into the Petri-Net is a valid model for describing a process for calculating the set of all games.

NOTE: It seems that more effort should be spent to confirm the choice to use 2^5 to factor out branching tree complexity.

What is happening here?

It seems that by using branching complexity of a system is a good way to remove iterations from a mathematical system.

If this relation holds true, we should be able to use it to examine any mathematically consistent system assuming that the correct Big O bounding function is known.

Game Tree Factor

Continuing to reflect on the choice of inputs for the Exponential function that we used to reduce the state-space:

O(c^{n}) => 2^5

I found a lecture here (http://www.ics.uci.edu/~kkask/Fall-2017%20CS271/slides/04-games.pdf)

In Tic-Tac-Toe

• there are 5 legal actions per state on average, total of 9 plies in game.
• A “ply” = one action by one player, “move” = two plies.

Exploring Game Tree

Game Tree Space

5^9 = 1,953,125 

State Space

9! = 362,880

Iteration Factor

Previous Post

We found experimentally that we could use 2^5 as a factor to remove iteration from our equation,
but we did not try to show how this factor may be derived.

Modeling the Computation Process instead of the Outcome

This seems like this may be a valid choice for modeling a game
if all the moves of the game are known in advance.

NOTE: that in the Peri-Net Diagram - we can see that:

Using a base of 2 seems to be a reasonable choice - because each move is guaranteed to alternate between X & O

Using '5' as the exponent also seems to make since:

There are  5 legal actions per state on average

Reduction to a Single Player Game

It appears that by treating Tic-Tac-Toe like a single player game,
we can use a branching factor that describes the choice between X & O on each turn.

So rather than using 5^9 which is a reflection of the choices as compared with overall available moves.

We can use 2^5 as a reflection of the alternating 'choice' that occurs after the place on the board is chosen.

Assorted comments

• Encoding state as membership of overlapping sets. This is interesting — seems that you’re saying if set A represents a column on the X axis, set B represents column on the Y axis, then membership of both A & B is interpreted as “coordinates X,Y”.

• Possible moves vs legal moves — these overlapping sets, and surely legal moves would be a member set of possible moves. E.g. a tic-tac-toe board could not legally be all-X’s. (You seem to touch on this when describing the game complexity as factorial, and with game tree space vs. state space)

• So in addition to sets representing elements and relationships, there would be sets-of-sets that describe reachable states.

  • Games have legal moves, FSMs have reachable states.

• There is a relationship between entropy and game complexity. Why? Does the relationship point at anything beyond the simple fact greater complexity requires more entry to describe?

• Say entropy is the minimum quantity of bits of needed to describe states of the game (possible or legal) and complexity is the number of elements (places, players, pieces) and the relationships between them: as complexity increases so does entropy.

• “we intend to show how that mathematical complexity of the game is fully described by the input net”

  Isn't the input net already defined as all possible game states and all possible game actions? Aren't they already equivalent as sets?

• It seems like you're exploring two spaces here:

  1. Various approaches to quantifying the complexity of a system (a game). Branching and path search algorithms are considered.
  2. Finding an equivalence or correspondence between the complexity of a Petri net and the complexity of the system it models.

  Am I following you?

Dear past me - here's the answers to these questions https://statebox.org/research/

And here's what we're building now https://github.com/stackdump/finite

Also more interesting material here https://www.euclideanspace.com/maths/discrete/types/dependent/index.htm

It seems like we can claim that the vector representation in code is a dependent sum type.
Meets the rules:

It also has this commentary

In computer programs they provide a sort of 
meta level capability to types in that
terms can be used at compile time and not just runtime.