### Ord, Countable Ordinals, and an Idea of sigfpe

This post is literate Haskell.

In the comments on my last post about ordinals, sigfpe suggests the following type constructors:

type One = () type Two = Either One One type N = [One] type Nplus1 = Either N One type NplusN = Either N N type NtimesN = (N,N) type NpowN = [N] type NpowNplusN = Either NpowN N

The idea is that each of these has an `Ord`

instance
defined. I think he's suggesting that the `Ord`

instance
for each (ignoring _|_) has an order type that is the same as the
ordinal its name corresponds to. I have some quibbles with his
implementation, but I really like the idea, and so I'll expand on it
below.

I'll start with my disagreements. My first is with the order for
`NpowN`

. In NpowN

[[(),()]] > [[()],[(),()]] > [[()],[()],[(),()]] > . . .

or in simpler form

[2] > [1,2] > [1,1,2] > . . .

Since no ordinal has an infinite decreasing sequence, the order type
of `[N]`

is not that of an ordinal. For now, we'll just
disregard the `[]`

type constructor.

My second quibble is with `Times`

. sigfpe does not make
this explicit, but the inference I drew from his examples was that we
could define `Times`

as

type Times = (,)

That doesn't quite work, though. Ordinal
arithmetic places the least significant part first, but the
`Ord`

instance for `(,)`

places the most
significant part first.

Now that we have these differences out of the way, let's get to the code.

We'll need these options for type class machinery later.

> {-# OPTIONS -fglasgow-exts #-} > {-# OPTIONS -fallow-incoherent-instances #-}

Ala sigfpe:

> type One = () > type Plus = Either > type Times = Flip Both > > data Both a b = Both a b > newtype Flip f a b = Flip (f b a)

To define `Times`

, we use a pair datatype with the standard
Haskell ordering (see `instance Ordinal2 Both`

below), but
apply the newtype `Flip`

, which warrants its own
definition, as it will be useful elsewhere.

So far, we can only define finite ordinals. In order to represent larger ordinals, we want to be able to represent an unlimited number of applications of a type constructor to a type.

> data ApplyN f x = More (ApplyN f (f x)) > | Stop x

`ApplyN`

does this -- after n applications of
`More`

, the type `x`

is wrapped n times in the
type constructor `f`

. Essentially, `ApplyN f x`

is f^{ω}(x).

Our first example of this will be adding one ω times.

> type N = ApplyN (Flip Plus One) One

This should look like (λ x . x + 1)^{ω} (1).

If `ApplyN`

works as advertized, `N`

should have
order type ω under a naive definition of
`Ord`

. Unfortunately, it does not. First of all, we can't
automatically derive `Ord`

for the type
`ApplyN`

, since it uses a type constructor, `f`

,
to build a new parameter. We will need

> class Ordinal1 f where > comp1 :: Ordinal a => f a -> f a -> Ordering

to describe the contract `f`

must meet to make ```
ApplyN
f x
```

ordered. Note that we use the class `Ordinal`

here, which is used only to avoid messing the with `Eq`

requirement on instances for `Ord`

.

> class Ordinal t where > comp :: t -> t -> Ordering

The second problem with the naive instance of `Ordinal`

on
`ApplyN`

is that each application of `More`

leads to a new type closer to the type we're really talking
about. What I mean by this is that, for the case of `N`

, we
really want to talk about

Flip Plus One (Flip Plus One (Flip Plus One . . . .

Which we can't directly say in Haskell.

We want to be talking about the type that is the limit. Since we can't
do that, to compare two values, we'll compare them at the maximum of
their levels. For instance, if we want to compare the values ```
Stop
()
```

and ```
More $ More $ Stop $ Flip $ Left $ Flip $ Left
()
```

, both of which are of type `N`

, we'll inject the
value `()`

into the higher level. To do this, we also need
`f`

to be have the property that we can inject into it a
value of its type parameter.

> class Container f where > inject :: x -> f x

To bring this back to the ordinals, we'll be representing
ω^{ω} as either and ordinal less than ω, or an
ordinal less than ω^{2}, or an ordinal less than
ω^{3} or …, and to compare two ordinals, we get a
representation of each in a common level, then compare them using the
comparison for ordinals less than the limiting ordinal of that level.

> instance (Container f, Ordinal1 f) => Ordinal1 (ApplyN f) where > comp1 (Stop u) (Stop v) = comp u v > comp1 (Stop u) (More v) = comp (Stop (inject u)) v > comp1 (More u) (Stop v) = comp u (Stop (inject v)) > comp1 (More u) (More v) = comp1 u v

We've defined the ordering on `ApplyN f`

so that

comp (Stop x) (More (Stop (inject x))) == EQ

which is what the paragraph above says, but more concise. We've
defined an equivalence relation on values of the type ```
ApplyN f
t
```

such that `x == inject x`

, so we're off to a good
start.

We'll also want `inject`

to be monotone, that is

x < y ==> inject x < inject y

and for `inject`

to send the order type of the domain not
just to *some* order in the codomain, but to the initial order
in the codomain. So, it's easy to write

> injectPlusL :: a -> Plus a b > injectPlusL x = Left x

or

> instance Container (Flip Plus b) where > inject v = Flip (Left v)

Injecting a into a*b is trickier, since we need the second part of the pair to be the minimal possible value in order for the injection range to be the initial part of the order. For this we define

> class Least x where > least :: x > instance Least One where > least = () > instance Least a => Least (Plus a b) where > least = Left least > instance (Least a, Least b) => Least (Times a b) where > least = Flip (Both least least) > instance Least b => Least (Flip Plus a b) where > least = Flip (Left least) > instance (Least a, Least b) => Least (Flip Times a b) where > least = Flip (Flip (Both least least)) > instance Least x => Least (ApplyN f x) where > least = Stop least

And we can now write the injection from a to a*b:

> instance (Least a) => Container (Flip Times a) where > inject v = Flip (Flip (Both least v))

We also have the trivial

> instance Container (ApplyN f) where > inject x = Stop x

Let's write the base instances for Ordinal in as general a way as possible:

> class Ordinal2 f where > comp2 :: (Ordinal a, Ordinal b) => f a b -> f a b -> Ordering > instance Ordinal2 Plus where > comp2 (Left _) (Right _) = LT > comp2 (Right _) (Left _) = GT > comp2 (Left x) (Left y) = comp x y > comp2 (Right x) (Right y) = comp x y > instance Ordinal2 Both where > comp2 (Both p q) (Both x y) = > case comp p x of > LT -> LT > GT -> GT > EQ -> comp q y > instance Ordinal2 f => Ordinal2 (Flip f) where > comp2 (Flip x) (Flip y) = comp2 x y > > instance Ordinal () where > comp _ _ = EQ

And the conversion instances between the n-ary Ordinal instances:

> instance (Ordinal1 f, Ordinal a) => Ordinal (f a) where > comp = comp1 > instance (Ordinal2 f, Ordinal a, Ordinal b) => Ordinal (f a b) where > comp = comp2 > instance (Ordinal2 f, Ordinal a) => Ordinal1 (f a) where > comp1 = comp2

Now let's do some examples. First we check that `Ordinal`

is
defined for `N`

:

> n_ok = comp (undefined :: N) (undefined :: N)

ω^{ω}:

> type NpowN = ApplyN (Flip Times N) One > npowN_ok = comp (undefined :: NpowN) (undefined :: NpowN)

We can now plug in `NpowN`

into its own definition to get
ω^{ω} * ω = ω^{ω + 1}

> type NpowNplusOne = ApplyN (Flip Times N) NpowN > nPowNplusOne_ok = comp (undefined :: NpowNplusOne) (undefined :: NpowNplusOne)or ω

^{ω * ω}= ω

^{ω2}:

> type NpowNpow2 = ApplyN (Flip Times NpowN) One > npowNpow2_ok = comp (undefined :: NpowNpow2) (undefined :: NpowNpow2)

The second method looks more powerful, but continuing it keeps us
below ω^{ω&omega}, so let's use the
first method of substituting back in to see if we can get further.

ω^{ω + 2}:

> type NpowNplus2 = ApplyN (Flip Times N) NpowNplusOne > nPowNplus2_ok = comp (undefined :: NpowNplus2) (undefined :: NpowNplus2)

We can now plug `ApplyN`

back into itself, and extend this
to ω^{ω + &omega} = ω^{ω * 2}:

> type NpowNtimes2 = ApplyN (ApplyN (Flip Times N)) One > npowNtimes2_ok = comp (undefined :: NpowNtimes2) (undefined :: NpowNtimes2)

Similarly, ω^{ω * 3}:

> type NpowNtimes3 = ApplyN (ApplyN (Flip Times N)) NpowNtimes2 > npowNtimes3_ok = comp (undefined :: NpowNtimes3) (undefined :: NpowNtimes3)

ω^{ω * ω} =
ω^{ω2}, which we apready saw before,
can also be written as

> type NpowNpow2' = ApplyN (ApplyN (ApplyN (Flip Times N))) One > npowNpow2'_ok = comp (undefined :: NpowNpow2') (undefined :: NpowNpow2')

ω^{ω2 * ω} = ω^{ω3} =

> type NpowNpow3 = ApplyN (ApplyN (ApplyN (Flip Times N))) NpowNpow2 > npowNpow3_ok = comp (undefined :: NpowNpow3) (undefined :: NpowNpow3)

ω^{ωω}:

> type NpowNpowN = ApplyN (ApplyN (ApplyN (ApplyN (Flip Times N)))) One > npowNpowN_ok = comp (undefined :: NpowNpowN) (undefined :: NpowNpowN)

ω^{ωω + 1}:

> type NpowNpowNplusOne = ApplyN (ApplyN (ApplyN (ApplyN (Flip Times N)))) NpowNpowN > npowNpowNplusOne_ok = comp (undefined :: NpowNpowNplusOne) (undefined :: NpowNpowNplusOne)

We can continue this process up to, but not including,
ε_{0}. We might be able to go further than this, but
I'll save that for later.

Thanks to sigfpe for the idea!

## 3 comments:

Wow! You took that a lot further than I thought was possible. I did discover the infinite descending chain but my approach to fixing it was much simpler: just defining Eq and Ord so that [a,...,b] was identified with [a,..,b,0,...,0] and lexicographically sorting on that. I think that is well behaved.

Curiously I started thinking about this stuff because I was wondering about proving termination of sets of rewrite rules. I'd always thought about ordinal infinities as being something set theorists did that had no relationship to anything practical. But now I see there are countless papers on program termination and ordinals going back as far as Turing.

I might not understand what you're getting at above; it took me a few run-throughs to understand what you were getting at in the comment that inspired this post, so please excuse me if I've misinterpreted your writing.

I have two quibbles with what you wrote. First is that there is no 0 in the system as it is now. This means that we'd have to use () = 1, so in [One], [] would be identified with [(),()], say. This makes [One] would have the same order type as One. We could use [Plus One One] for N.

The second is that adding small values onto the end of a list doesn't actually change the problematic ordering. Adding them onto the beggining, though, solves the problem. So, I think we would want to define

comp [a_1,…,a_n] [b_1,…,b_m]

as

compare

((replicate ((max m n)-n) least) ++ [a_1,…,a_n])

((replicate ((max m n)-m) least) ++ [b_1,…,b_m])

Then, the type [t] would be ω copies of t, which we would intepret as a product of ω t's, since [t] is isomorphic to Either () (Either (t,()) (Either (t,(t,())) ….

So if the type t had order type κ, the type [t] would have order type κ^ω. The ordinal notation system would then be limited by [[[ &hellip [N] … ]]] = ω^ω^ω.

Does that look right to you?

> I might not understand what you're getting at above

It's a long time since I studied set theory, and even then the course I did was disastrous. So anything you're not getting is probably my mistake! (And do you know a good book on the subject?)

> First is that there is no 0 in the system as it is now.

You can make a reasonably good zero with the line:

data Zero

(But you'll need to switch on ghc extensions for that.)

> The second is that adding small values onto the end of a list doesn't actually change the problematic ordering.

You're right, I want n-element lists embedded in the bottom end of (n+1)-element lists and the 'lower' end is towards the right, not left.

> The ordinal notation system would then be limited by [[[ … [N] … ]]] = ω^ω^ω.

Yes, that was the conclusion I came to, so I like the way you pushed much further.

I'd like to find some nice rewrite rules whose iterations can be mapped into these types.

Post a Comment