 Ordinal notations for $\Gamma_0$
Here is a Haskell data type for ordinal notations up
to $\Gamma_0$, together with an assignment of fundamental
sequences which generates the correct wellordering. Using
this assignment, we can map an ordinal notation to the
tree (of transfinite depth) of its predecessors.
[ This material should probably be compared with
Dershowitz's ideas, expressed e.g. in
http://www.math.tau.ac.il/~nachum/papers/ordinalsnew.ps.gz
]
Because Haskell is lazy, we can represent functions defined
on the natural numbers by infinite streams, and so represent the
predecessor tree as a Rose tree.
> infixl `W`
> infixr `V`
I parameterise by a type of atoms. This is for possible
further development.
> data E x = N  Nought, represents 0
>  W (E x) (E x)  W a b represents a + w^b
>  V (E x) (E x)  V a b represents phi_a b
>  At x  atoms of type x
> deriving (Eq)
> sE = (`W` N)
For each expression, I define a list (which may be infinite) of its
immediate predecessors.
> pd :: E x > [E x]
> pd N = []
> pd (a `W` N) = [a]
> pd (a `W` (b `W` N)) = iterate (`W` b) a
> pd (a `W` b) = map (a `W`) (pd b)
> pd (N `V` N) = iterate (N `W`) N
> pd (N `V` (a `W` N)) = iterate (N `W`) t where t = sE (N `V` a)
> pd ((a `W` N) `V` N) = iterate (a `V`) N
> pd ((a `W` N) `V` ( b `W` N))
> = iterate (a `V`) t where t = sE (a `V` b)
> pd (a `V` N) = map (`V` N) (pd a)
> pd (a `V` (b `W` N)) = map (`V` t) (pd a) where t = sE (a `V` b)
> pd (a `V` b) = map (a `V`) (pd b)
Using this, we may map expressions in an orderpreserving way to
trees. The paths in the tree are `slowly' descending chains, in
which each descent is always to an \emph{immediate} predecessor.
> data Tree x = Tree x [Tree x] deriving (Show,Eq)
> tree :: E x > Tree (E x)
> tree e = Tree e (map tree (pd e))
> paths :: Tree x > [[x]]
> paths (Tree x []) = [[x]]
> paths (Tree x ts) = [ x:p  t < ts, p < paths t ]
 IO
To enter and show lists, I use `W` as a left associative infix operator.
and `V` as a right associative infix operator.
> instance (Show x) => Show (E x) where
> showsPrec p e =
> f e False where f N = \ c > showString "N"
> f (a `W` b) = g False " `W` " a b
> f (a `V` b) = g True " `V` " a b
> g t str a b = \ c > (if c then brack else id)
> (f a t . showString str . f b (not t))
> brack f = showString "(" . f . showString ")"
 printing a numbered list, one entry per line.
It is useful to have a showable data type which is printed as a numbered list.
Note that there is no effort to justify the number. If the list is
finite, one could probably do something sensible.
> data ShowList x = ShowList [x]
> instance (Show x) => Show (ShowList x) where
> showsPrec p (ShowList x) =
> let show_ent (n,x) = shows n . showString ". " . shows x
> in (composelist . seplist (showString "\n") . map show_ent . zip nos) x
The following are used elsewhere, and hence defined at the global level.
> nos = [1..]
> composelist = foldr (.) id
> seplist s xs = case xs of [x] > xs
> (x:xs') > x:s:seplist s xs'
> _ > xs
 printing a tree
We print a tree topdown, with a line per node, each line being prefixed by the
Dewey decimals of the node. In the following function, the line prefix is
passed around (as a functional buffer) in the variable b.
> data ShowTree x = ShowTree (Tree x)
> instance (Show x) => Show (ShowTree x) where
> showsPrec p (ShowTree x) = st x id
> where st (Tree x ts) b = b . showString ": "
> . shows x
> . showString "\n"
> . rest b ts
> rest b = composelist
> . map (\(n,t)> st t (b . showString "." . shows n))
> . zip nos
Hack a tree back to something we can show, by lopping off branches beyond n.
> hack :: Int > Tree x > Tree x
> hack n (Tree x ts) = Tree x ( take n ( map (hack n) ts ))
For example, the following expression shows some of the ordinal
structure of $\omega^\omega$.

 (ShowTree . hack 5 . tree) (expw omega)

> zer, one, omega, epsilon0 :: E String
> plus :: E String > E String > E String
> expw :: E String > E String
> zer = N
> one = zer `W` N
> two = one `W` N
> omega = N `W` one
> plus a b = case b of N > a
> b1 `W` b2 > (a `plus` b1) `W` b2
> _ > a `W` b
> expw = (N `W`)
> epsilon0 = N `V` N
> g0fs = epsilon0 : map (`V` N) g0fs
> finite n = (it sE !! n ) zer
> it f = id : [ f . g  g < it f ]
Depth of a tree.
> depth (Tree x ts) = 1 + foldr max 0 (map depth ts)
Size of a tree.
> size (Tree x ts) = 1 + foldr (+) 0 (map depth ts)
Example
 Main> [(size . hack x . tree) (expw two)  x < [0..]]
 [1,2,5,13,29,56,97,155,233,334,{Interrupted!}