Skip to main content

Module ordinal

Module ordinal 

Source
Expand description

Ordinals below ε₀ in Cantor normal form — the stage counter of transfinite execution.

Every ordinal α < ε₀ is uniquely ω^{β₁}·c₁ + ω^{β₂}·c₂ + … + ω^{βₖ}·cₖ with exponents β₁ > β₂ > … > βₖ (themselves ordinals below ε₀, in the same form) and positive natural coefficients. An Ordinal stores exactly that list, so equality is structural and the order is lexicographic on (exponent, coefficient) pairs, a longer list winning a common prefix.

The arithmetic is the ordinal arithmetic, not the arithmetic of naturals, and its asymmetries are the point:

  • addition absorbs every term of the left summand below the right summand’s leading exponent: 1 + ω = ω, yet ω + 1 > ω;
  • multiplication distributes on the left only: α·(β + γ) = α·β + α·γ, while (1 + 1)·ω = ω ≠ ω + ω; a term ω^β·c of the right factor contributes ω^{α₁ + β}·c when β > 0 and α·c (the leading coefficient scaled, the rest kept) when β = 0;
  • exponentiation α^β = ∏ (α^{ω^{βᵢ}})^{cᵢ}, where for β ≥ 1 a finite base n ≥ 2 gives n^{ω^β} = ω^{ω^{β'}} (β = 1 + β') and an infinite base gives α^{ω^β} = ω^{α₁·ω^β} — so 2^ω = ω and (ω + 1)^ω = ω^ω.

Structs§

Ordinal
An ordinal below ε₀. See the module documentation.