		Search-engine friendly clone of the ACL2 documentation.

Alphorder

Total order on atoms

Alphorder is a non-strict total order, a ``less than or equal,'' on atoms. By ``non-strict total order'' we mean a function that always returns t or nil and satisfies the following properties.

Antisymmetry: XrY & YrX -> X=Y
Transitivity: XrY & YrZ -> XrZ
Trichotomy: XrY v YrX

Also see lexorder, which extends alphorder to all objects.

(Alphorder x y) has a guard of (and (atom x) (atom y)).

Within a single type: rationals are compared arithmetically, complex rationals are compared lexicographically, characters are compared via their char-codes, and strings and symbols are compared with alphabetic ordering. Across types, rationals come before complexes, complexes come before characters, characters before strings, and strings before symbols. We also allow for ``bad atoms,'' i.e., atoms that are not legal Lisp objects but make sense in the ACL2 logic; these come at the end, after symbols.

Function: alphorder

(defun alphorder (x y)
       (declare (xargs :guard (and (atom x) (atom y))))
       (cond ((real/rationalp x)
              (cond ((real/rationalp y) (<= x y))
                    (t t)))
             ((real/rationalp y) nil)
             ((complex/complex-rationalp x)
              (cond ((complex/complex-rationalp y)
                     (or (< (realpart x) (realpart y))
                         (and (= (realpart x) (realpart y))
                              (<= (imagpart x) (imagpart y)))))
                    (t t)))
             ((complex/complex-rationalp y) nil)
             ((characterp x)
              (cond ((characterp y)
                     (<= (char-code x) (char-code y)))
                    (t t)))
             ((characterp y) nil)
             ((stringp x)
              (cond ((stringp y) (and (string<= x y) t))
                    (t t)))
             ((stringp y) nil)
             (t (cond ((symbolp x)
                       (cond ((symbolp y) (not (symbol< y x)))
                             (t t)))
                      ((symbolp y) nil)
                      (t (bad-atom<= x y))))))

Subtopics

Fast-alphorder: Probably faster alternative to alphorder.
Hons-alphorder-merge: Merge two already-alphordered lists of atoms.