Major Section: ACL2-BUILT-INS
Using the nonnegative integers and lists we can represent the ordinals up to
epsilon-0. The ordinal representation used in ACL2 has changed as
of Version_2.8 from that of Nqthm-1992, courtesy of Pete Manolios and Daron
Vroon; additional discussion may be found in ``Ordinal Arithmetic in ACL2'',
proceedings of ACL2 Workshop 2003,
http://www.cs.utexas.edu/users/moore/acl2/workshop-2003/. Previously,
ACL2's notion of ordinal was very similar to the development given in ``New
Version of the Consistency Proof for Elementary Number Theory'' in The
Collected Papers of Gerhard Gentzen, ed. M.E. Szabo, North-Holland
Publishing Company, Amsterdam, 1969, pp 132-213.
The following essay is intended to provide intuition about ordinals.
The truth, of course, lies simply in the ACL2 definitions of
o-p and o<.
Very intuitively, think of each non-zero natural number as by being denoted by a series of the appropriate number of strokes, i.e.,
0 0 1 | 2 || 3 ||| 4 |||| ... ...Then ``
omega,'' here written as w, is the ordinal that might be
written as
w |||||...,i.e., an infinite number of strokes. Addition here is just concatenation. Observe that adding one to the front of
w in the
picture above produces w again, which gives rise to a standard
definition of w: w is the least ordinal such that adding another
stroke at the beginning does not change the ordinal.We denote by w+w or w*2 the ``doubly infinite'' sequence that we
might write as follows.
w*2 |||||... |||||...One way to think of
w*2 is that it is obtained by replacing each
stroke in 2 (||) by w. Thus, one can imagine w*3, w*4, etc., which
leads ultimately to the idea of ``w*w,'' the ordinal obtained by
replacing each stroke in w by w. This is also written as ``omega
squared'' or w^2, or:
2 w |||||... |||||... |||||... |||||... |||||... ...We can analogously construct
w^3 by replacing each stroke in w by
w^2 (which, it turns out, is the same as replacing each stroke in
w^2 by w). That is, we can construct w^3 as w copies of w^2,
3 2 2 2 2 w w ... w ... w ... w ... ...Then we can construct
w^4 as w copies of w^3, w^5 as w copies of
w^4, etc., ultimately suggesting w^w. We can then stack omegas,
i.e., (w^w)^w etc. Consider the ``limit'' of all of those stacks,
which we might display as follows.
.
.
.
w
w
w
w
w
That is epsilon-0.Below we begin listing some ordinals up to epsilon-0; the reader can
fill in the gaps at his or her leisure. We show in the left column
the conventional notation, using w as ``omega,'' and in the right
column the ACL2 object representing the corresponding ordinal.
ordinal ACL2 representation
0 0
1 1
2 2
3 3
... ...
w '((1 . 1) . 0)
w+1 '((1 . 1) . 1)
w+2 '((1 . 1) . 2)
... ...
w*2 '((1 . 2) . 0)
(w*2)+1 '((1 . 2) . 1)
... ...
w*3 '((1 . 3) . 0)
(w*3)+1 '((1 . 3) . 1)
... ...
2
w '((2 . 1) . 0)
... ...
2
w +w*4+3 '((2 . 1) (1 . 4) . 3)
... ...
3
w '((3 . 1) . 0)
... ...
w
w '((((1 . 1) . 0) . 1) . 0)
... ...
w 99
w +w +w4+3 '((((1 . 1) . 0) . 1) (99 . 1) (1 . 4) . 3)
... ...
2
w
w '((((2 . 1) . 0) . 1) . 0)
... ...
w
w
w '((((((1 . 1) . 0) . 1) . 0) . 1) . 0)
... ...
Observe that the sequence of o-ps starts with the natural
numbers (which are recognized by natp). This is convenient
because it means that if a term, such as a measure expression for
justifying a recursive function (see o<) must produce an o-p,
it suffices for it to produce a natural number.The ordinals listed above are listed in ascending order. This is
the ordering tested by o<.
The ``epsilon-0 ordinals'' of ACL2 are recognized by the recursively
defined function o-p. The base case of the recursion tells us that
natural numbers are epsilon-0 ordinals. Otherwise, an epsilon-0
ordinal is a list of cons pairs whose final cdr is a natural
number, ((a1 . x1) (a2 . x2) ... (an . xn) . p). This corresponds to
the ordinal (w^a1)x1 + (w^a2)x2 + ... + (w^an)xn + p. Each ai is an
ordinal in the ACL2 representation that is not equal to 0. The sequence of
the ai's is strictly decreasing (as defined by o<). Each xi
is a positive integer (as recognized by posp).
Note that infinite ordinals should generally be created using the ordinal
constructor, make-ord, rather than cons. The functions
o-first-expt, o-first-coeff, and o-rst are ordinals
destructors. Finally, the function o-finp and the macro o-infp
tell whether an ordinal is finite or infinite, respectively.
The function o< compares two epsilon-0 ordinals, x and y.
If both are integers, (o< x y) is just x<y. If one is an integer
and the other is a cons, the integer is the smaller. Otherwise,
o< recursively compares the o-first-expts of the ordinals to
determine which is smaller. If they are the same, the o-first-coeffs
of the ordinals are compared. If they are equal, the o-rsts of the
ordinals are recursively compared.
Fundamental to ACL2 is the fact that o< is well-founded on
epsilon-0 ordinals. That is, there is no ``infinitely descending
chain'' of such ordinals. See proof-of-well-foundedness.
To see the ACL2 definition of this function, see pf.
