		Search-engine friendly clone of the ACL2 documentation.

Macro-libraries

Def-partial-measure

Introduce measure and termination predicates for a partial function definition

Introduction By Way of an Example

We begin with a motivating example. Suppose we want to admit factorial without the need to prove termination, as follows.

(fact x)
=
(if (equal x 0)
    1
  (* x (fact (1- x))))

Of course, this ``definition'' is non-terminating on negative number inputs. But with def-partial-measure, or defpm for short, we can admit a suitable definition for this partial function as follows. First, we define a function to represent the termination test and another function to represent the actual parameter of the recursive call.

(defun fact-test (x)
  (equal x 0))
(defun fact-step (x)
  (1- x))

Now we can execute our utility: we provide it with the names of the two functions above, and it generates a measure, a termination predicate, and a potentially helpful theory, respectively.

(defpm fact-test fact-step
  fact-measure fact-terminates fact-theory)

Here are the events exported by the defpm call above.

; The first three lemmas can be useful for reasoning about the termination
; predicate, FACT-TERMINATES.

(DEFTHM FACT-TERMINATES-BASE
  (IMPLIES (FACT-TEST X)
           (FACT-TERMINATES X)))

(DEFTHM FACT-TERMINATES-STEP
  (IMPLIES (NOT (FACT-TEST X))
           (EQUAL (FACT-TERMINATES (FACT-STEP X))
                  (FACT-TERMINATES X))))

(DEFTHMD FACT-TERMINATES-STEP-COMMUTED
  (IMPLIES (AND (SYNTAXP (SYMBOLP X))
                (NOT (FACT-TEST X)))
           (EQUAL (FACT-TERMINATES X)
                  (FACT-TERMINATES (FACT-STEP X)))))

(THEORY-INVARIANT (INCOMPATIBLE (:REWRITE FACT-TERMINATES-STEP)
                                (:REWRITE FACT-TERMINATES-STEP-COMMUTED)))

; The next two lemmas can be useful for defining functions whose termination
; is ensured by the measure just introduced.

(DEFTHM FACT-MEASURE-TYPE
  (O-P (FACT-MEASURE X)))

(DEFTHM FACT-MEASURE-DECREASES
  (IMPLIES (AND (FACT-TERMINATES X)
                (NOT (FACT-TEST X)))
           (O< (FACT-MEASURE (FACT-STEP X))
               (FACT-MEASURE X))))

; Finally, the four enabled rewrite rules above are collected into a theory.

(DEFTHEORY FACT-THEORY
  '(FACT-TERMINATES-BASE FACT-TERMINATES-STEP
    FACT-MEASURE-TYPE FACT-MEASURE-DECREASES))

With the events above, we can introduce the following definition, which in effect guards the body with the termination predicate. (Perhaps at some point we will extend defpm to create this definition automatically.) The :in-theory hint below was carefully crafted to allow the proof to succeed very quickly.

(defun fact (x)
  (declare (xargs :measure (fact-measure x)
                  :hints (("Goal"
                           :in-theory
                           (union-theories (theory 'fact-theory)
                                           (theory 'minimal-theory))))))
  (if (fact-terminates x)
      (if (fact-test x)
          1
        (* x (fact (fact-step x))))
    1 ; don't-care
    ))

With the events above (not necessarily including the definition of fact), we can prove that fact terminates on natural number inputs. A second macro, defthm-domain, automates much of that task:

(defthm-domain fact-terminates-holds-on-natp
  (implies (natp x)
           (fact-terminates x))
  :measure (nfix x))

See defthm-domain.

Detailed Documentation

General form:

(defpm ; or equivalently, def-partial-measure ; ;
  TEST STEP
  MEASURE TERMINATES THEORY
  :formals FORMALS ; default is (x)
  :verbose VERBOSE ; default is nil
  )

where there is no output unless VERBOSE is non-nil. The remaining arguments are as follows.

First consider the case that FORMALS is the default, (x). The arguments TEST and STEP are conceptually ``inputs'': they should name existing functions on the indicated value for formals (which by default is (x)). Then defpm will attempt to generate a measure and termination predicate on those formals, with the indicated names (MEASURE and TERMINATES, respectively). These theorems are suitable for admitting a function of the following form, where capitalized names refer to those in the defpm call above, and where additional code may appear as indicated with ``...''.

(defun foo (x)
  (declare (xargs :measure (MEASURE x)
                  :hints (("Goal"
                           :in-theory
                           (union-theories (theory 'THEORY)
                                           (theory 'minimal-theory))))))
  (if (TERMINATES x)
      (if (TEST x)
          ...
        (... (fact (STEP x)) ...)
    ...))

The generated THEORY names the four rules generated by the defpm call, as in the example above.

(defthm TERMINATES-base
  (implies (TEST x)
           (TERMINATES x)))
(defthm TERMINATES-step
  (implies (not (TEST x))
           (equal (TERMINATES (STEP x))
                  (TERMINATES x))))
(defthmd TERMINATES-step-commuted
  (implies (AND (syntaxp (symbolp x))
                (not (TEST x)))
           (equal (TERMINATES x)
                  (TERMINATES (STEP x)))))
(theory-invariant (incompatible (:rewrite TERMINATES-step)
                                (:rewrite TERMINATES-step-commuted)))
(defthm MEASURE-type
  (o-p (MEASURE x)))
(defthm MEASURE-decreases
  (implies (and (TERMINATES x)
                (not (TEST x)))
           (o< (MEASURE (STEP x))
               (MEASURE x))))
(deftheory THEORY
  '(TERMINATES-base TERMINATES-step MEASURE-type MEASURE-decreases))

For arbitrary formals the situation is similar, except that there is one step function per formal, obtained by adding the formal name as a suffix to the specified STEP separated by a hyphen. Thus we have the following events when FORMALS is (y1 ... yk).

(defthm TERMINATES-base
  (implies (TEST y1 ... yk)
           (TERMINATES y1 ... yk)))
(defthm TERMINATES-step
  (implies (not (TEST y1 ... yk))
           (equal (TERMINATES (STEP-y1 y1 ... yk)
                              ...
                              (STEP-yk y1 ... yk))
                  (TERMINATES y1 ... yk))))
(defthm TERMINATES-step-commuted
  (implies (AND (syntaxp (symbolp y1)) ... (syntaxp (symbolp yk))
                (not (TEST y1 ... yk)))
           (equal (TERMINATES (STEP-y1 y1 ... yk)
                              ...
                              (STEP-yk y1 ... yk))
                  (TERMINATES y1 ... yk))))
(theory-invariant (incompatible (:rewrite TERMINATES-step)
                                (:rewrite TERMINATES-step-commuted)))
(defthm MEASURE-type
  (o-p (MEASURE y1 ... yk)))
(defthm MEASURE-decreases
  (implies (and (TERMINATES y1 ... yk)
                (not (TEST y1 ... yk)))
           (o< (MEASURE (STEP-y1 y1 ... yk)
                        ...
                        (STEP-yk y1 ... yk))
               (MEASURE y1 ... yk))))
(deftheory THEORY
  '(TERMINATES-base TERMINATES-step MEASURE-type MEASURE-decreases))

Implementation

The implementation of defpm (i.e., def-partial-measure has been designed to make proofs efficient. It should be completely unnecessary to know anything about the implementation in order to use defpm effectively. If however you are interested, you can execute :trans1 on your defpm call to see the events that it generates.

More Information

The community book misc/defpm.lisp illustrates how to use defpm and defthm-domain to define ``partial'' functions. Search for calls of my-test in that book to see examples.

Related work of Dave Greve, in particular his utility def::ung, may be found in community books directory books/coi/defung/. Our utilities def-partial-measure and defthm-domain were developed independently using an approach that seems considerably simpler than Greve's development. However, his utility is much more powerful in that it generates a termination test, rather than requiring the user to provide it, and also it handles reflexive functions — definitions with recursive calls like (mc91 (mc91 (+ n 11))) — while ours were not designed to do so.