Cantor Normal Form #
The Cantor normal form of an ordinal is generally defined as its base
ω expansion, with its
non-zero exponents in decreasing order. Here, we more generally define a base
Ordinal.CNF in this manner, which is well-behaved for any
b ≥ 2.
Implementation notes #
Ordinal.CNF as an association list, where keys are exponents and values are
coefficients. This is because this structure intrinsically reflects two key properties of the Cantor
- It is ordered.
- It has finitely many entries.
- Add API for the coefficients of the Cantor normal form.
- Prove the basic results relating the CNF to the arithmetic operations on ordinals.
Inducts on the base
b expansion of an ordinal.
The Cantor normal form of an ordinal
o is the list of coefficients and exponents in the
b expansion of
CNF b (b ^ u₁ * v₁ + b ^ u₂ * v₂) = [(u₁, v₁), (u₂, v₂)]