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
(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) ...)))
(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))) ...))
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
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).
(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)))
(defthm o-p-of-two-nats-measure (equal (o-p (two-nats-measure a b)) t))