Approach to Conway arithmetic in Haskell.
[ Written 1999-12-06 16:25:30]
For some motivation see http://www.dcs.ed.ac.uk/~pgh/conway.html.

I am not sure what to export.  Can we locate this somewhere
among the Haskell "Num"'s?

> module Conway(Game,mk_game,left_moves,right_moves
>              ,(+),(-),zero,swap   -- commutative group
>              ,(*),one             -- commutative ring
>              ,eq0,pos,neg         -- ordered
>              ,(<),(<=),eq) 
> where
> import Prelude hiding ((+),(-),(*),(<),(<=))
> infixl 6 + 
> infixl 6 -
> infixr 7 *

> data Game = Game [ Game ] [ Game ] deriving Show
> left_moves (Game ls _) = ls
> right_moves (Game _ rs) = rs
> mk_game = Game

replace left with right

> swap (Game ls rs) = Game [ swap r | r <- rs ] [ swap l | l <- ls ]
> minus = swap

interleaving

> (t1@(Game ls1 rs1)) + (t2@(Game ls2 rs2)) 
>    = Game ([ l1 + t2 | l1 <- ls1 ] ++ [ t1 + l2 | l2 <- ls2 ])
>           ([ t1 + r2 | r2 <- rs2 ] ++ [ r1 + t2 | r1 <- rs1 ])
> t1 - t2 = t1 + minus t2

multiplication I have just copied from Conway's book.  Someone
once told me why it's inevitable but I have forgotten.

> (t1@(Game ls1 rs1)) * (t2@(Game ls2 rs2)) 
>    = Game (   [ l1 * t2 + t1 * l2 - l1 * l2 | l1 <- ls1, l2 <- ls2 ] 
>            ++ [ r1 * t1 + t2 * r2 - r1 * r2 | r1 <- rs1, r2 <- rs2 ])
>           (   [ l1 * t2 + t1 * r2 - l1 * r2 | l1 <- ls1, r2 <- rs2 ] 
>            ++ [ r1 * t2 + t1 * l2 - r1 * l2 | r1 <- rs1, l2 <- ls2 ])

pos means that you have a winning strategy if you start on the left.

> pos (t@(Game ls _)) 
>      = or [ pos' l | l <- ls ]
>        where pos' (t'@(Game _ rs')) 
>                   = and [ pos r | r <- rs' ]

neg means you have winning strategy if you start on the right.

> neg = pos . swap

eq0 means the second player to go has a winning strategy.
Clearly eq0 = eq0 . swap, and eq0 zero. 

> eq0 t = not (pos t || neg t) 

eq means there is a bisimulation between the games.

> eq t1 t2 = eq0 (t1 - t2)

> instance Eq Game where (==) = eq

We have a commutative ordered ring, whose elements are
equivalence classes under (==). 

> t1 < t2 = pos (t2 - t1)
> t1 <= t2 = not (t2 < t1) 

Some "numbers" for testing.

> zero = Game [] []
> one  = Game [zero] []
> minus_one = swap one
> two = one + one 
> three = two + one

> half = Game [zero] [one]
> minus_half = swap half 
> quarter = Game [zero] [half,one]
> minus_three_quarters = Game [minus_one] [minus_half,zero]

> test1 = two + three == three + two 
> test2 = (two + three) + one == two + (three + one)
> test3 = two * two == two + two 
> test4 = two * three == two + two + two
 
Afterthoughts:

  One needs a way of "canonicalising" a game, or reducing it
  to a normal form with all the junk stripped out. 
  (If we are to able to multiply two by three!)
  I seem to remember this is very connected with Dedekind cuts.

  Since we have infinite streams, we can presumably define omega?

> omega = let nos = zero:[ x + one | x <- nos]
>         in  Game nos []

  What is the definition of reciprocal? 

Detritus

> nub [] = []
> nub (x:xs) = x:[ y | y <- nub xs, y /= x ]

> norm (Game ls rs) = Game ls' rs' 
>                      where ls' = nub [ norm l' | l' <- ls ]
>                            rs' = nub [ norm r' | r' <- rs ]

------------------------------------------------

Joyal definition: can this be right??

> jplus (t1@(Game ls1 rs1)) (t2@(Game ls2 rs2)) 
>    = Game [ jplus l1 t2 | l1 <- ls1 ] 
>           [ jplus t1 r2 | r2 <- rs2 ] 
> jminus t1 t2 = jplus t1 (swap t2)

s0 g means there is a winning strategy for left, going second
s1 g means there is a winning strategy for left, going first

> s0 (t@(Game ls rs)) = and [ s1 r | r <- rs ]
> s1 (t@(Game ls rs)) = or  [ s0 l | l <- ls ]

> jzero = Game [] []
> jone = Game [jzero] []
> js = jzero : map (jplus jone) js
> js' = jzero : map (flip jplus jone) js