Ordinals-0.0.0.2: Ordinal arithmetic

Math.Ordinals.MultiSet

Description

Encoding of ordinals up to epsilon_0 as an iterated multiset: definition in Basic Proof Theory by Troelstra and Schwichenberg. Note, this is not the most efficient way to calculate ordinals. This library is better than having none. I think CNF representation would be more efficent, planning to add in the next version of this library.

For further analysis on efficiency of implementations on ordinals see http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.91.8089

FYI, an ordinal calculator that covers wider range beyond epsion_0 can be found at http://www.mtnmath.com/ord/ which is written C++. However, I found a serious error in this calculator (ver 0.2): the property a^b * a^c == a^(b+c) does not hold. For example,

```  ordCalc> 3 ^(w^w + w + 1) * 3^(w^w) == 3 ^ (w^w + w + 1 + w^w)
FALSE
```

This calculator didn't seem to run QuickCeck style automatic testing, although it does have hundreds (or maybe more than a thousand) tests cases but some of them even causes segmentation faults depending on the machine I built this ordCalc.

Synopsis

# Types

newtype Ordinal Source

Constructors

 O [Ordinal]

Instances

 Enum Ordinal Eq Ordinal Integral Ordinal Num Ordinal Ord Ordinal Real Ordinal Show Ordinal

# Operators

Exponentiation. Defined a new operator since neither `^` nor `^^` will work. Note, `(w o)` is same as `(w 1 :^ o)` for any oridnal `o`.

There are more operators such as `+` (addition), `*` (multiplication), `-`, (left addtion) defined in the `Num` class instance declaration for `Ordinal`. Although ordinals are not really `Num` we decided to make it as a `Num` instance for convenience; We can use functions such as `sum` and `product` over list of ordinals and they behave well. We also plan to implement division and remainder operations in the `Integral` class instance for similar reason. For further information on class instances see the source code.

# Auxiliary functions

convenience function that takes an argument as the power of omega (the first limit ordinal).

well formedness of ordinals

# Auxiliary operators

These operators can manipulate the `Ordinal` newtype data structure internally. Use with care since it can break the well-formedness (`wf`) of ordinal representation.