		Search-engine friendly clone of the ACL2 documentation.

Two-nats-measure

An ordinal measure for admitting functions: lexicographic ordering of two natural numbers.

(two-nats-measure a b) constructs an ordinal that can be used to prove that recursive functions terminate. It essentially provides a lexicographic order where a is more significant than b. More precisely, its correctness is understood through the theorem:

Theorem: o<-of-two-nats-measure

(defthm o<-of-two-nats-measure
  (equal (o< (two-nats-measure a b)
             (two-nats-measure c d))
         (or (< (nfix a) (nfix c))
             (and (equal (nfix a) (nfix c))
                  (< (nfix b) (nfix d))))))

This is often useful for admitting mutually recursive functions where one function inspects its argument and then immediately calls another. For instance, suppose you want to admit:

(mutual-recursion
  (defun f (x) ...)
  (defun g (x) (if (special-p x) (f x) ...)))

Then since g calls f on the same argument, you can't just use ACL2-count, or for that matter any other measure that only considers the argument x) to show that the call of (f x) has made progress. However, it's easy to use two-nats-measure to ``rank'' the functions so that f is always considered smaller than g:

(mutual-recursion

  (defun f (x)
    (declare (xargs :measure (two-nats-measure (acl2-count x) 0)))
    ...)

  (defun g (x)
    (declare (xargs :measure (two-nats-measure (acl2-count x) 1)))
    ...))

More generally two-nats-measure may be useful whenever you want to admit an algorithm that makes different kinds of progress.

Example. Suppose you have a pile of red socks and a pile of blue socks to put away. Every time you put away a red sock, I add a bunch of blue socks to your pile, but when you put a blue sock away, I don't get to add any more socks. You will eventually finish since the pile never gets any new red socks. You can admit a function like this with (two-nats-measure num-red num-blue).

See also nat-list-measure for a generalization of this to a lexicographic ordering of a list of natural numbers (of any length instead of just two numbers).

Definitions and Theorems

Function: two-nats-measure

(defun two-nats-measure (a b)
  (declare (xargs :guard (and (natp a) (natp b))))
  (make-ord 2 (+ 1 (nfix a))
            (make-ord 1 (+ 1 (nfix b)) 0)))

Theorem: o-p-of-two-nats-measure

(defthm o-p-of-two-nats-measure
  (equal (o-p (two-nats-measure a b)) t))

Theorem: o<-of-two-nats-measure

(defthm o<-of-two-nats-measure
  (equal (o< (two-nats-measure a b)
             (two-nats-measure c d))
         (or (< (nfix a) (nfix c))
             (and (equal (nfix a) (nfix c))
                  (< (nfix b) (nfix d))))))