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