- 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/ordinals-new.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 order-preserving 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 top-down, 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!}