Approach to Conway arithmetic in Haskell.
[ Written 1999-12-06 16:25:30]

Conway numbers are named after their inventor John H. Conway.  They
generalise Cantor's ordinal numbers to support subtraction, division.
They form a complete, non-Archimedean ordered field, and have many
applications within mathematics.

They arise from consideration of a certain kind of two person game.  A
game configuration consists of a set of game configurations that
"Left" can move to if they move first, and a set of game
configurations that "Right" can move to if they move first.  The game
configurations are supposed to be built up inductively, so that there
are no infinite plays.

For some motivation see http://www.dcs.ed.ac.uk/~pgh/conway.html.

It is reasonably easy to represent Conway games in Haskell, using
lists to represent sets. Because one has infinite lists (ie. streams),
one can event represent certain transfinite and infinitesimal Conway games.

CODE

I have no idea what should be exported.  This is a guess.

> module Conway(Game,mk_game,left_moves,right_moves
>              ,(+),(-),zero,swap   -- commutative group
>              ,(*),one             -- commutative ring
>              ,eq0,gt0,lt0         -- 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

addition is a kind of interleaving

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

multiplication I have just copied from Conway's book.  It is 
incomprehensible to me.

> (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 ])


strat1L means that you have a winning strategy if you start on the left
strat2L means that you have a winning strategy if you're left, and right starts
etc

> strat1L (t@(Game ls _)) 
>      = or [ strat2L l | l <- ls ]
> strat2L (t@(Game _ rs))
>      = and [ strat1L r | r <- rs ]
> strat1R = strat1L . swap
> strat2R = strat2L . swap

A game is positive (gt0) in Conway's sense if left has a winning
strategy regardless who is first to go. 

> gt0 g = strat1L g && strat2L g
> lt0 g = gt0 . swap 

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

> eq0 t = strat2L t && strat2R t 

        = not (strat1L t || strat1R t) 

eq means there is a bisimulation between the games.

> eq t1 t2 = eq0 (t1 - t2)

> instance Eq Game where (==) = eq
> instance Ord Game where (<=) = (<=)

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

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

Some examples. 

> 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]

Some sanity tests.

> test1 = two + three         == three + two 
> test2 = (two + three) + one == two + (three + one)
> test3 = two * two           == two + two 
> test4 = two * three         == two + two + two  -- crucifies computer...

test3 causes control stack overflow...
 
Detritus

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

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

  > union = (++)  

  > union xs ys = sort (xs++ys)

> union xs ys = nub (xs ++ ys)

> sort [] = []
> sort (x:xs) = sort [ y | y <- xs, y < x ] ++ (x:sort [ y | y <- xs, x < y])

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

Joyal has a paper which takes Conway numbers as its
starting point, and constructs a category.  As I 
remember, his definition of addition is different from Conway's.
I can't find the Joyal paper.

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

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

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