## Friday, June 29, 2007

### Ordinals, part 2

Peter G. Hancock reminded us of the obvious way to define uncountable ordinals. A rough translation into a single data type, rather than a family:

data Ordinal n = Zero (Nat n)
| Succ (Ordinal n)
| forall t . Limit (Less t n) (Ordinal t -> Ordinal n)
The parameter n is the "class" of the ordinal. We need the helper definitions:
data Nat n where
Z :: Nat Z
S :: Nat n -> Nat (S n)
data Z
data S n

data Less a b where
LessZ :: Nat b -> Less Z (S b)
LessS :: Less a b -> Less (S a) (S b)

embed :: Ordinal n -> Ordinal (S n)
embed (Zero x) = Zero (S x)
embed (Succ x) = Succ (embed x)
embed (Limit e f) = Limit (onemore e) (embed . f)
where
onemore :: Less a b -> Less a (S b)
onemore (LessZ x) = LessZ (S x)
onemore (LessS p) = LessS (onemore p)

Then we can define the first uncountable ordinal as
omega_1 = Limit (LessS (LessZ Z)) embed
and the sequence of ωs up to ωω as
omega_n :: Nat n -> Ordinal n
omega_n Z = Zero Z
omega_n (S n) = Limit (plusone n) embed
where
plusone :: Nat n -> Less n (S n)
plusone Z = LessZ Z
plusone (S n) = LessS (plusone n)

Hancock has many other interesting ways to represent ordinals, including as surreal numbers (with code), in which we can provide a more precise answer the the question I was originally responding to, What happens when you divide infinite by two? In the case of surreal numbers, you get, simply, ω/2, just as you do with the hyperreals. Hancock also provides a datatype for the ordinals up to Γ0 without resorting to embedded functions, which means we can do things like computably compare them.