## Monday, July 23, 2007

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

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

``` > [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!

sigfpe said...

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.

Jim Apple said...

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?

sigfpe said...

> 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.