|
|
|---|
|
|
|
|---|
Recursion and Induction: The Ordinals
The ordinals are an extension of the naturals that captures an essential notion of ordering. They were invented by Georg Cantor in the late nineteen century. While controversial during Cantor's lifetime, ordinals are among the richest and deepest mines of mathematics. We only scratch the surface here.
Think of each natural number as denoted by a sequence of strokes, i.e.,
0 0 1 ∣ 2 ∣ ∣ 3 ∣ ∣ ∣ 4 ∣ ∣ ∣ ∣ … … ω ∣ ∣ ∣ ∣ ∣ …
The limit of that progression is the ordinal ω, an infinite sequence of strokes.
Ordinal addition is just concatenation. Observe that adding one to the front of ω produces ω again, which gives rise to a standard definition of ω: the least ordinal such that adding another stroke at the beginning does not change the ordinal.
We denote by ω + ω or ω×2 the “doubly infinite” sequence that we might write as follows.
ω × 2 ∣ ∣ ∣ ∣ ∣ … ∣ ∣ ∣ ∣ ∣ …
One way to think of ω×2 is that it is obtained by replacing each stroke in 2 (| |) by ω. Thus, one can imagine ω×3, ω×4, etc., which leads ultimately to the idea of ω×ω, the ordinal obtained by replacing each stroke in ω by ω. This is also written as ω^2.
ω^2 ∣ ∣ ∣ ∣ ∣ … ∣ ∣ ∣ ∣ ∣ … ∣ ∣ ∣ ∣ ∣ … ∣ ∣ ∣ ∣ ∣ … ∣ ∣ ∣ ∣ ∣ … …
We can analogously construct ω^3 by replacing each stroke in ω by ω^2 (which, it turns out, is the same as replacing each stroke in ω^2 by ω). That is, we can construct ω^3 as ω copies of ω^2, and so on. This ultimately suggests ω^ω. We can then stack ωs, i.e., ω^(ω^ω), etc. Consider the limit of all of those stacks,
ω^(ω^(ω^(ω^(ω^(ω^(ω^ … )))))).
That limit is ε_0. (As the subscript suggests, there are lots more ordinals! But ACL2 stops with ε_0.)
Despite the plethora of ordinals, we can represent all the ones below ε_0 in ACL2, using lists. Below we begin listing some ordinals up to ε_0; the reader can fill in the gaps at his or her leisure. We show in the left column the conventional notation and in the right column the ACL2 object representing the corresponding ordinal.
| ordinal | ACL2 representation | |
| 0 | 0 | |
| 1 | 1 | |
| 2 | 2 | |
| 3 | 3 | |
| … | … | |
| ω | ((1 . 1) . 0) | |
| ω + 1 | ((1 . 1) . 1) | |
| ω + 2 | ((1 . 1) . 2) | |
| … | … | |
| ω×2 | ((1 . 2) . 0) | |
| (ω×2) + 1 | ((1 . 2) . 1) | |
| … | … | |
| ω×3 | ((1 . 3) . 0) | |
| (ω×3) + 1 | ((1 . 3) . 1) | |
| … | … | |
| ω^2 | ((2 . 1) . 0) | |
| … | … | |
| ω^2 + ω×4 + 3 | ((2 . 1) (1 . 4) . 3) | |
| … | … | |
| ω^3 | ((3 . 1) . 0) | |
| … | … | |
| ω^ω | ((((1 . 1) . 0) . 1) . 0) | |
| … | … | |
| ω^ω + ω^99 + ω×4 + 3 | ((((1 . 1) . 0) . 1) (99 . 1) (1 . 4) . 3) | |
| … | … | |
| ω^(ω^2) | ((((2 . 1) . 0) . 1) . 0) | |
| … | … | |
| ω^(ω^ω) | ((((((1 . 1) . 0) . 1) . 0) . 1) . 0) | |
| … | … |
We say an ordinal is “finite” if it is not a cons and we define (o-finp x) to recognize finite ordinals. Of course, if x is an ordinal and finite, it is a natural number. But by defining o-finp this way we ensure that if an ordinal is not finite we can recur into it with cdr.
To manipulate ordinals we define functions that access the first exponent, the first coefficient, and the rest of the ordinal:
(defun o-first-expt (x) (if (o-finp x) 0 (car (car x)))) (defun o-first-coeff (x) (if (o-finp x) x (cdr (car x)))) (defun o-rst (x) (cdr x))
For example, if x is the representation of ω^e×c + r then (o-first-expt x) is e, (o-first-coeff x) is c and (o-rst x) is r.
Here is the definition of o-p, the function that recognizes ordinals.
(defun o-p (x)
(if (o-finp x)
(natp x)
(and (consp (car x))
(o-p (o-first-expt x))
(not (equal 0 (o-first-expt x)))
(natp (o-first-coeff x))
(< 0 (o-first-coeff x))
(o-p (o-rst x))
(o< (o-first-expt (o-rst x))
(o-first-expt x)))))
(The ACL2 definition is syntactically different but equivalent.)
The function o< is the “less than” relation on ordinals. We show its definition below. But study the definition of o-p first. It says that an ordinal is a list of pairs, terminated by a natural number. Each pair (e . c) consists of an exponent e and a coefficient c and represents (ω^e)×c. The exponents are themselves ordinals and the coefficients are non-0 naturals. Importantly, the exponents are listed in strictly descending order. The list represents the ordinal sum of its elements plus the final natural number. Thus, ordinals can be viewed as polynomials.
By insisting on the ordering of exponents we can readily compare two ordinals, using o< below, in much the same way we can compare polynomials.
(defun o< (x y)
(if (o-finp x)
(or (not (o-finp y))
(< x y))
(if (o-finp y)
nil
(if (equal (o-first-expt x)
(o-first-expt y))
(if (equal (o-first-coeff x)
(o-first-coeff y))
(o< (o-rst x)
(o-rst y))
(< (o-first-coeff x)
(o-first-coeff y)))
(o< (o-first-expt x)
(o-first-expt y))))))
(The ACL2 definition is syntactically different but equivalent.)
Problem 90.
Which is smaller, ordinal a or ordinal b?
Problem 91.
The o< operation can be reduced to lexicographic comparison.
Define m2 so that it constructs “lexicographic ordinals”
from two arbitrary natural numbers. Specifically, show that
the following is a theorem:
(implies (and (natp i1)
(natp j1)
(natp i2)
(natp j2))
(and (o-p (m2 i1 j1))
(iff (o< (m2 i1 j1)
(m2 i2 j2))
(if (equal i1 i2)
(< j1 j2)
(< i1 i2)))))
The crucial property of o< is that it is well-founded on the ordinals. That is, there is no infinite sequence of ordinals, x_i such that … x_3 o< x_2 o< x_1 o< x_0.
Problem 92.
What is the longest decreasing chain of ordinals starting from the ordinal
10? What is the longest decreasing chain of ordinals starting
from the ordinal ((1 . 1) . 0)?
Problem 93.
Construct an infinitely descending o< chain of objects. Note that
by the well-foundedness of o< on the ordinals, your chain will not
consist entirely of ordinals!
Problem 94.
Prove that o< is well-founded on our ordinals, i.e., those
recognized by o-p.
Caution: Using the logical machinery we have developed here, it is not possible to state that o< is well-founded on the ordinals: that requires an existential quantifier and infinite sequences. However, it can be done in a traditional set theoretic setting. That is, the theorem that o< is well-founded is a “meta-theorem”, it can be proved about our system but it cannot be proved within our system.
Our definitional and induction principles are built on the assumption that o< is well-founded on the ordinals recognized by o-p. Thus, if some ordinal measure of the arguments of a recursive function decreases according to o< in every recursive call, the recursion cannot go on forever.
The representation of ordinals described here is a version of Cantor's
Normal Form. See
Next: