Friday, July 20, 2007

Ordinal Notation and Computer Proof

Last ordinal post here

There is an implementation in Coq of the countable ordinals up to Γ0.

2 comments:

sigfpe said...

Funny you should post that. I just wrote this and I need to compare notes with someone. I think I'm representing (some) ordinals as Haskell types here (not values, types). Essentially all ordinals that can be constructed from a finite number of applications of addition, multiplication and exponentiation to 1. But the important thing is that I'm not just modelling the underlying sets with types. I'm modelling the actual *ordinals* with types because () is an instance of () and so each of these types is also an instance of Ord. Does this look correct? Ordinal arithmetic isn't my field :-)

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

sigfpe said...

s/instance of ()/instance of Ord/