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.

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.

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