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 `omega`

s,
i.e., `(w^w)^w`

etc. Consider the ``limit'' of all of those stacks,
which we might display as follows.
. . . w w w w wThat 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-p`

s 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-expt`

s of the ordinals to
determine which is smaller. If they are the same, the `o-first-coeff`

s
of the ordinals are compared. If they are equal, the `o-rst`

s 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.