###
ε_{0} in an Ord instance

In my last post, I worked rather hard to approach ε_{0}, but there is a much simpler way to form a type with an `Ord`

instance that has order type ε_{0}, according to Trees, Ordinals and Termination (mirror)

import List data Tree = Node | Tree [Tree] instance Ord Tree where compare Node Node = EQ compare Node (Tree _) = LT compare (Tree _) Node = GT compare (Tree x) (Tree y) = compare (sort x) (sort y) instance Eq Tree where x == y = compare x y == EQOr, according to Ordinal Arithmetic with List Structures (mirror)

data Cons = Nil | Cons Cons Cons instance Ord Cons where compare Nil Nil = EQ compare Nil (Cons _ _) = LT compare (Cons _ _) Nil = GT compare a@(Cons x' y') b@(Cons x y) = case compare x' x of LT -> compare y' b EQ -> compare y' y GT -> compare a y instance Eq Cons where x == y = compare x y == EQThese representations do not help in the general problem of representing all ordinals less than some ordinal κ, but they are much simpler than our previous method.

For trees with larger order types, see What's so special about Kruskal's theorem and the ordinal &Gamma_{0} (mirror)

## No comments:

Post a Comment