# Conway games

J.H.Conway's astounding book `On Numbers and Games' (ONAG) has recently (2001) been republished by A K Peters, Ltd. It was first published by the Academic Press 1976. Conway's idea was to combine Cantor's theory of transfinite ordinals with Dedekind's analysis of the continuum, by developing an `arithmetic' in which a `number' is the strength (ie. competitive advantage) of a position in a certain kind of terminating two-person game. This is done in ONAG, which I strongly encourage you to get hold of and read.

Conway's ideas have been taken up and pursued by a few others (eg. Knuth, Gonshor, Kruskal, Joyal, game theorists, Ehrlich). To me they raise some fascinating questions in computer science, proof theory, and other fields. How about nonterminating games? What are the implications of confining winning strategies to be written in a particular formal system? And so on.

Here I will simply write down a definition of the kind of games considered by Conway, and his arithmetic operations +, * and -. If you want to read something much better written, see this wikipedia article. or this article (pdf).

The games are defined inductively, in a manner reminiscent of Peter Aczel's `tree set' interpretation of constructive ZF in Martin-Löfs type theory. In preparation, here is a brief sketch of this interpretation.

## Tree set interpretation

Aczel fixes a universe of sets ` { T(u) | u : U } ` closed under a suitable set of set-forming operators (0, 1, +, Sigma, Pi, what have you - I won't be specific), and interprets `epsilon' sets using well founded trees of type ` W(U,T)`, where ``` W ``` is Martin-Löf's well-ordering `quantifier', ie the least solution ` X ` of
```
X = (Sigma u : U) T(u) -> X
```
with typical element
```
sup(u,f)
where   u : U,  f : T(u) -> W(U,T)
```
To (over-)simplify, he defines the epsilon relation ` .eps. `, and the auxiliary relations of inclusion ` .sub. ` and equality ` .eq. ` between trees in ` W(U,T) ` recursively. (Well, actually, he's more careful than that. See below.) The idea is
```
x .eps. sup(u,f)   ==   (Sigma t : T(u)) x .eq. f(t)
sup(u,f) .sub. y   ==   (Pi z : T(u)) f(t) .eps. y
x .eq. y           ==   x .sub. y   /\  y .sub. x
```
Then one proves that `.eq.` is an equivalence relation compatible with `.eps.` and `.sub.`; then we figure out which set-theoretical axioms hold, depending on the closure properties of the universe `(U,T)`.

(To really formalise the construction in some version of Martin-Löf type theory, one has to be more careful -- as Aczel was. See for example "The type-theoretic interpretation of constructive set theory: Choice Sequences", in "The L.E.J.Brouwer Centenary Symposium", North-Holland 1982, eds. Troelstra, van Dalen. From memory, one has to define for each `a : W(U,T)` the pair of predicates `((a .sub.), (.sub. a))` by recursion. By defining both predicates together, one has access to `.eq.`.)

## Bi-Trees

For Conway games, we consider a mild isotope ` W2 ` of the ` W ` quantifier, where `W2(U,T)` is the least solution ` X ` of
```
X = ((Sigma uL : U) T(uL) -> X) * ((Sigma uR : U) T(u) -> X)
```
(The symbol `*` means binary Cartesian product) with typical element
```
sup2(uL, fL, uR, fR)
where   uL, uR : U,
fL : T(uL) -> W2(U,T), fR : T(uR) -> W2(U,T)
```
Such things might perhaps be called bi-trees. As it were, we have `sets' with 2 kinds (or `colours') of epsilon relation. How are these games? Actually they are positions in games. The games are played between 2 players, which we call `L' and `R'. If it is L's go, then she can move to any of the positions ```{ fL(t) | t : T(uL) }``` and (natch) if is R's go, she can move to any of ```{ fR(t) | t : T(uR) }```. Then they take turns. The first player who cannot move (their family being empty) `loses', and the other `wins'. Since `W2` is inductively defined, one or other of the players will inevitably win.

An interesting thing about the Conway games is that either player can go first; in other structures I have thought about eg here) it is `built in' that one or other of the players goes first.

## Arithmetic of bi-trees

Conway defines a position to have zero value if the second player has a winning strategy. He calls it positive (resp. negative) if `L` (resp. `R`) has a winning strategy. (It is also possible that the first player can win - such games are called `fuzzy'. Conway does not count them as numbers, though they are interesting as games.)

To define the arithmetic operations `+,*,-`, it helps to use Conway's own `cut' notation. He writes a game position in the form

```
x = { .., xL, .. | .., xR, .. }
```
where `xL` denotes (the destination position of) a typical one of `L`'s moves, and `xR` similarly one of `R`'s. Then (recursively):
```

x + y    ==   { .., xL + y, .. , x + yL, ..
| .., x + yR, .. , xR + y, .. }

x * y    ==   { .., xL*y + x*yL - xL*yL, .. , xR*y + x*yR - xR*yR, ..
| .., xL*y + x*yR - xL*yR, .. , xR*y + x*yL - xR*yL, .. }

- x      ==   { .., - xR, ..  | .. , - xL, .. }
```
(When the definitions are written out with full logical hygiene, it must be assumed that the universe of sets `(U,T)` is closed under binary disjoint union.) (There seems to be a typo in the definition of product on p. 291 of Conway and Guy's "The book of numbers".) The intuition for `+` is clearly a kind of interleaving between the two summands. I don't understand `*` well enough to say anything about it. Minus is a systematic swapping of roles between the two players. (Conway considers a lot of other operators on games, including one which is much closer to the ordinary non-commutative ordinal sum than `+`.)

Here is one approach to dealing with Conway games in Haskell.

One can then define an equivalence relation (like strong bisimulation) between game positions ` x ` and ` y `, which equates them if ` x - y ` has zero value (ie. the second player to move has a winning strategy). When quotiented by this relation, and supplemented by analogously defined order relations, it turns out, astoundingly, that (non-fuzzy) game positions form a linearly ordered real-closed field, with a very strong universal embedding property. (A field is formally real if `-1` is not a sum of squares, and real closed if it in addition it has no proper formally real algebraic extensions.) There are the so-called "surreal" numbers (so-called by Knuth), that includes not only transfinite ordinals, but their reciprocals, roots, powers, logarithms, factorials, and so on. (Exactly what we get depends on the universe we start with.)

## Joyal's version

Joyal has considered yet another definition of `+`:

```

x + y    ==   { .., xL + y, .. | .., x + yR, .. }

```
Note the difference from Conway's definition: he ignores leftmoves in `y` and rightmoves in `x`. Can this be right??

He defines (recursively) two sets of strategies: `S0(x)` (the set of winning strategies for the left player when they go second) and `S1(x)` (the set of winning strategies for the left player when they go first):

```
S0(x)   == (Pi xR) S1(xR)
S1(x)   == (Sigma xL) S0(xL)

```
Joyal shows that if one defines a morphism from `x` to `y` to be an element of `S0(y + (-x))`, then one has a monoidal, closed, symmetric(??) and auto-dual category.

## Some interesting things

It seems interesting to investigate the development of surreal arithmetic in a constructive framework. There has been some impressive work on this, by Jacob Lurie, JSL Vol 63, June 1998: "The Effective Content of Surreal Algebra"; there's an realaudio interview with him at interview. He's looked at the recursion theory of Conway games. Lurie has written a review of "On Numbers and Games" in JSL, vol. 63, no. 4, Dec 1998, pp. 1602-1604.)

Also interesting is the `two epsilons' set theory to which Conway tantalisingly alludes on p. 66 of his book. (It may be useful to think of the indices of the two families in a bi-tree as `actions' and `co-actions', in the spirit of Milner's CCS.) What would an axiomatision of 2-epsilon set theory look like?

A philosopher with an interesting perspective on surreal arithmetic, generalised continua, "the infinite" and so on is Philip Ehrlich. He alludes to "a vast generalisation of Cantor's theory of arithmetic". It sounds as if he has something more general than Conway's surreals; unfortunately, he doesn't put his papers online.

Andre Joyal has apparently given a category-theoretic description of Conway games. (There is a short paper from 1977.) According to a paper by Martin Hyland(??) they form a `compact closed' category. I think the definition of the hom-sets is based on the properties of addition. I don't know what a compact closed category is but I've the impression it is a rather grotty mechanistic kind of category. Perhaps one gets a category with better properties by allowing that games needn't terminate? Then the aritmetic operations can no longer be defined by well-founded induction. Instead of an initial algebra for ` S |-> (Fam S)^2 ` one might look instead at final coalgebras for this or some other functor. This raises questions of what happens to the concepts of winning and losing. My feeling is that one should focus on the notion of having a strategy to avoid losing, which is being driven or painted into "a corner" in which there is no further room for maneuver, or deadlock.