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
-, (left addtion)
defined in the
Num class instance declaration for
Although ordinals are not really
Num we decided to make it
Num instance for convenience; We can use functions such
product over list of ordinals and they behave well.
We also plan to implement division and remainder operations
Integral class instance for similar reason. For further
information on class instances see the source code.
convenience function that takes an argument as the power of omega (the first limit ordinal).