		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.