### Countable Ordinals in Haskell

In Haskell: What happens when you divide infinity by 2?, Eric Kidd asks:

...

2. Is it possible to represent any other (more interesting and/or more correct) definitions of infinity in Haskell?

3. What’s the best way to think about the infinite ordinals?

The code below is my answer to those questions for countable ordinals only. I'm not sure if it makes sense to talk about representing uncoutable sets on the kind of computers we have now: We can talk about infinite countable sets as computable limits of finite objects, but what would an uncountable set look like? They can't be objects of `Nat -> Bool`

, since every object of this type is represented in some finite number of bits. It seems like we are stuck in a universe where Goedel's V=L is true.

{-# OPTIONS_GHC -fglasgow-exts #-} {- See: http://en.wikipedia.org/wiki/Ordinal_arithmetic http://en.wikipedia.org/wiki/Large_countable_ordinals To add later: http://citeseer.ist.psu.edu/487179.html -} module Countable where data Finite = Z | S !Finite {- A countable ordinal is 0, a successor, or a limit of a countable sequence. This definition is weak, as the countable sequence should be strictly increasing, but that's hard to express. One way to do so would be to interpret (Limit f) as the limit of (sum i = 0 to n) (1 + f i). Note: this addition is not commutative. This would complicate things, however, so I'll leave it for a later extension. -} data Ordinal = Zero | Succ !Ordinal | Limit (Finite -> Ordinal) deriving (Show) {- I believe that there is no computable Eq or Ord instance for Ordinals. Comments? We make an approximation here by taking the nth value of the limit. This calculation is very slow, and, of course, will equate a lot of ordinals that are not actually equal. -} nth :: Ordinal -> Finite -> Integer nth Zero _ = 0 nth (Succ x) n = 1+(nth x n) nth (Limit f) n = nth (f n) n instance Show (Finite -> Ordinal) where show f = show [f Z, f (S Z), f (S (S Z)), f (S (S (S Z)))] instance Eq Ordinal where x == y = (show x) == (show y) {- The basic ordinal arithmetic. Addition and multiplication are not commutative. -} addOrdinal :: Ordinal -> Ordinal -> Ordinal addOrdinal x Zero = x addOrdinal x (Succ y) = Succ (addOrdinal x y) addOrdinal x (Limit y) = Limit (\z -> addOrdinal x (y z)) multiplyOrdinal :: Ordinal -> Ordinal -> Ordinal multiplyOrdinal x Zero = Zero multiplyOrdinal x (Succ y) = addOrdinal (multiplyOrdinal x y) x multiplyOrdinal x (Limit y) = Limit (\z -> multiplyOrdinal x (y z)) expOrdinal :: Ordinal -> Ordinal -> Ordinal expOrdinal x Zero = Succ Zero expOrdinal x (Succ y) = multiplyOrdinal (expOrdinal x y) x expOrdinal x (Limit y) = Limit (\z -> expOrdinal x (y z)) -- The first infinite ordinal finite :: Finite -> Ordinal finite Z = Zero finite (S x) = Succ (finite x) omega = Limit finite -- Apply a f some number of times, starting at z apply Zero f z = z apply (Succ n) f z = f (apply n f z) apply (Limit g) f z = Limit (\x -> apply (g x) f z) -- With apply, we have more succinct definitions of arithmetic addOrdinal' x y = apply y Succ x multiplyOrdinal' x y = apply y (flip addOrdinal x) Zero expOrdinal' x y = apply y (flip multiplyOrdinal x) (Succ Zero) -- Enumerates the fixed points of a function. fix Zero f = apply omega f Zero fix (Succ n) f = apply omega f (Succ (fix n f)) fix (Limit g) f = Limit (\x -> fix (g x) f) -- Some larger ordinals: epsilon n = fix n (expOrdinal omega) -- The Veblen heirarchy: veblen Zero b = expOrdinal omega b veblen (Succ a) b = fix b (veblen a) veblen (Limit a) b = Limit (\x -> veblen (a x) b) -- Feferman-Schutte ordinals gamma n = fix n (flip veblen Zero)

## 4 comments:

It is indeed impossible for a computer to represent an uncountable set. Such a representation would be a function from the natural numbers to the set, which would constitute a proof that the set was countable.

The V=L axiom has little to do with what you are talking about. You make it sound as if V=L means that "all is countable". In fact, even if you assume V=L there will still be plenty of very large sets around.

Also, it is a bit inaccurate to say that you are representing all countable ordinals. At best you are representing ordinals below the Church-Kleene ordinal.

An Jared said that it is "impossible for a computer to represent uncountable sets". This is false, see e.g., Klaus Weihrauch's book "Computable Analysis" for an explanation about why this is not the case. Actually, I am going to go now and write a blog post about this, since "non-professionals" seem to be a bit misguided about this.

Hi, it is me again. I wrote this for jared and anyone else that might be interested. As my post explains, in the cae of ordinals, the cruicial question is: which operations on ordinals should be computable. For example, is the order relation computable for your representation?

Post a Comment