Comments on Everyone Else is Crazy: Ord, Countable Ordinals, and an Idea of sigfpe

> I might not understand what you're gettin...

2007-07-24T11:06:00.000-07:00

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

I might not understand what you're getting at abov...

2007-07-24T09:21:00.000-07:00

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?

Wow! You took that a lot further than I thought wa...

2007-07-24T07:53:00.000-07:00

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.