Major Section: MISCELLANEOUS
Using the nonnegative integers and lists we can represent the
ordinals up to
epsilon-0. The ACL2 notion of
ordinal is the same as
that found in
nqthm-1992 and both are 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
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
win the picture above produces
wagain, which gives rise to a standard definition of
wis the least ordinal such that adding another stroke at the beginning does not change the ordinal.
We denote by
w*2 the ``
doubly infinite'' sequence that we
might write as follows.
w*2 |||||... |||||...One way to think of
w*2is that it is obtained by replacing each stroke in
w. Thus, one can imagine
w*4, etc., which leads ultimately to the idea of ``
w*w,'' the ordinal obtained by replacing each stroke in
w. This is also written as ``
2 w |||||... |||||... |||||... |||||... |||||... ...We can analogously construct
w^3by replacing each stroke in
w^2(which, it turns out, is the same as replacing each stroke in
w). That is, we can construct
3 2 2 2 2 w w ... w ... w ... w ... ...Then we can construct
w^4, etc., ultimately suggesting
w^w. We can then stack
(w^w)^wetc. 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 representationObserve that the sequence of
0 0 1 1 2 2 3 3 ... ... w '(1 . 0) w+1 '(1 . 1) w+2 '(1 . 2) ... ... w*2 '(1 1 . 0) (w*2)+1 '(1 1 . 1) ... ... w*3 '(1 1 1 . 0) (w*3)+1 '(1 1 1 . 1) ... ...
2 w '(2 . 0) ... ...
2 w +w*4+3 '(2 1 1 1 1 . 3) ... ...
3 w '(3 . 0) ... ...
w w '((1 . 0) . 0) ... ...
w 99 w +w +4w+3 '((1 . 0) 99 1 1 1 1 . 3) ... ...
2 w w '((2 . 0) . 0)
w w w '(((1 . 0) . 0) . 0) ... ...
e0-ordinalps starts with the nonnegative integers. This is convenient because it means that if a term, such as a measure expression for justifying a recursive function (see e0-ord-<) must produce an
e0-ordinalpit suffices for it to produce a nonnegative integer.
The ordinals listed above are listed in ascending order. This is
the ordering tested by
epsilon-0 ordinals'' of ACL2 are recognized by the recursively
e0-ordinalp. The base case of the recursion tells
us that nonnegative integers are
epsilon-0 ordinals. Otherwise, an
epsilon-0 ordinal is a
(o1 . o2), where
o1 is a non-
o2 is an
epsilon-0 ordinal, and if
o2 is not an
integer then its
car (which, by the foregoing, must be an
ordinal) is no greater than
o1. Thus, if you think of a
epsilon-0 ordinal as a list, each element is an non-
epsilon-0 ordinal, the ordinals are listed in weakly descending
order, and the final
cdr of the list is an integer.
e0-ord-< compares two
both are integers,
e0-ord-< is just
x<y. If one is an integer and
the other is a
cons, the integer is the smaller. Otherwise, the
ordinals in their
cars are compared recursively and determines which
is smaller unless the
cars are equal, in which case the ordinals in
cdrs are compared.
Fundamental to ACL2 is the fact that
e0-ord-< is well-founded on
epsilon-0 ordinals. That is, there is no ``infinitely descending
chain'' of such ordinals. See proof-of-well-foundedness.