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.


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/