ORDINALS

ordinals in ACL2 
Major Section:  MISCELLANEOUS

Ordinals are used in ACL2 for proving termination in the admission of recursive function definitions. For a proof that the ACL2 ordinals are well-founded, see proof-of-well-foundedness.

The representation of ordinals changed in ACL2 Version_2.8, and is due to Pete Manolios and Daron Vroon. They have also defined algorithms for ordinal arithmetic, created a library of theorems to reason about ordinal arithmetic, and written the rest of this documentation in order to explain this change. We thank them for their efforts. Although they have provided the implementation and even modified the community books as needed, we have looked over their work and are maintaining it (and this documentation); if there are any bugs, they should be considered ours (Matt Kaufmann and J Moore).

A book is included for compatibility with the representation before Version_2.8. For books that contain events relying on the previous ordinal implementation, insert the following lines before the first such event: 

(include-book "ordinals/e0-ordinal" :dir :system)
(set-well-founded-relation e0-ord-<)

The new ordinal representation is based on a slightly different version of Cantor Normal Form than that used by the old ordinals. An advantage of the new representation is that it is exponentially more succinct than the old representation.

While pre-Version_2.8 ACL2 versions provided built-in functions for checking if an object is an ordinal and for comparing two ordinals, they did not provide support for reasoning about and constructing ordinals. The community books directory books/ordinals provides such support. First, it provides efficient algorithms for ordinal arithmetic (including addition, subtraction, multiplication, and exponentiation). The algorithms and their complexity are described in the following paper. 

Manolios, Panagiotis & Vroon, Daron. 
Algorithms for ordinal arithmetic.
Baader, Franz (ed),
19th International Conference on Automated Deduction--CADE-19.
Pages 243-257 of LNAI, vol. 2741.  Springer-Verlag.
Second, the algorithms are mechanically verified and libraries of theorems which can be used to automate reasoning involving the ordinals are provided. For details, see the following paper. 
Manolios, Panagiotis & Vroon, Daron.
Ordinal arithmetic in ACL2.
Kaufmann, Matt, & Moore, J Strother (eds). 
Fourth International Workshop on the ACL2 Theorem
Prover and Its Applications (ACL2-2003),
July, 2003.
See http://www.cs.utexas.edu/users/moore/acl2/workshop-2003/.
We now describe aspects of the above mentioned books in more detail.

The new ordering function is o< and the new ordinal recognizer is o-p. See also natp, posp, o<=, o>, o>=, o-first-expt, o-first-coeff, o-rst, make-ord, o-finp, and o-infp.

The old ordinals were based on the following formulation of Cantor Normal Form:

For any ordinal, a < epsilon-0, there exist natural numbers p and n, and ordinals a1 >= a2 >= ... >= an > 0 such that a > a1 and a = w^(a1) + w^(a2) + ... + w^(an) + p.

Thus, a predicate recognizing ACL2's old ordinals is given by the following definition. 

(defun e0-ordinalp (x)
  (if (consp x)
      (and (e0-ordinalp (car x))
           (not (equal (car x) 0))
           (e0-ordinalp (cdr x))
           (or (atom (cdr x))
               (not (e0-ord-< (car x) (cadr x)))))
    (and (integerp x)
         (>= x 0))))
The new representation is based on a corollary to the above theorem, which we get by the left distributive property of ordinal multiplication over ordinal addition. Thus, w^a + w^a = (w^a)2, w^a + w^a + w^a = (w^a)3 and so forth. The corollary is as follows:

For any ordinal, a < epsilon-0, there exist natural numbers p and n, positive integers x1, x2, ..., xn and ordinals a1 > a2 > ... > an > 0 such that a > a1 and a = w^(a1)x1 + w^(a2)x2 + ... + w^(an)xn + p.

Instead of representing an ordinal as a list of non-increasing ordinals, we represent it as a list of exponent-coefficient pairs, such that the exponents are strictly decreasing (see o-p). Note that this representation is exponentially more efficient than the old representation.

The ordinal arithmetic functions: o+, o-, o*, and o^ are defined in the ordinals library (in the community books directory books/ordinals). To use them, include the book ordinals-without-arithmetic or ordinals, depending on whether you want the arithmetic books included or not (ordinals includes community book books/arithmetic/top-with-meta). To use the old ordinals, include the book e0-ordinal and run the command (set-well-founded-relation e0-ord-<)

The community book books/arithmetic/natp-posp is a book for reasoning about posp and natp. We recommend using this book if you have to reason about posp and natp. It is included in community book books/arithmetic/top, which is included in community book books/arithmetic/top-with-meta, which is included in community book books/ordinals/ordinals.

If you have a good reason to use the old definitions of the ordinals (e.g., because of legacy code and theorems), then we provide a convenient way to do this. The book ordinal-isomorphism proves that the new ordinals are order-isomorphic to the old ordinals and thus theorems proved in one context can be directly transferred to the other. For an example of how to do this, look at the book defmul in the community books directory books/workshops/2000/ruiz/multiset.

The ordinals books have been used to prove non-trivial theorems. For a good example, see the books in the community books directory books/workshops/2003/sustik/support, where Matyas Sustik proves Dickson's lemma.

Finally, many termination proofs can be carried out with weaker orderings than the ordinals up to epsilon-0. For example, many inductive theorem provers only know that the lexicographic ordering on natural numbers is well-founded. The book lexicographic-ordering contains a definition of such an ordering l< whose arguments are either a list of natural numbers, or a natural number. In the book we prove that l< is well-founded (that is, we prove a :well-founded-relation defthm and provide a macro llist to simplify the generation of measure functions. We also show how to use l< to prove that the famous Ackermann function terminates. Finally, since l< does something reasonable with natural numbers, it gets along with acl2-count, the default measure chosen by ACL2.