		Search-engine friendly clone of the ACL2 documentation.

Tau-system

Bounders

Intervals, bounder functions, and bounder correctness

Bounder Forms 1 and 2: 
(implies (and (tau-intervalp i1) 
              ... 
              (or (equal (tau-interval-dom i1) 'dom1-1) 
                  ...) 
              ... 
              (in-tau-intervalp x1 i1) 
              ...) 
         (and (tau-intervalp (bounder-fn i1 ...)) 
              (in-tau-intervalp target 
                                (bounder-fn i1 ...))))

where target is either (fn x1 ... y1 ...) or (mv-nth 'n (fn x1 ... y1 ...)), depending on whether we are in the Form 1 or Form 2 case, respectively. However, the shape above is meant just as a reminder. Details are given below.

This topic first explains the basic shape of Bounder Form 1. Then it illustrates Bounder Form 2. Finally, it deals briefly with proving bounder correctness theorems. The community book tau-bounders/elementary-bounders contains bounders for various elementary functions including +, *, /, floor, mod, logand, lognot, logior, logorc1, logeqv, logxor, and ash. You might look at or include this book to see more example theorems, to see how proofs of such theorems are managed, and to experiment with their effects on proving theorems involving arithmetic over finite or half-finite intervals.

A bounder correctness theorem establishes that bounder-fn is a ``bounder'' for the function fn. That means that when trying to compute a tau for a call of fn (or, in the case of Form 2, for the nth component of the multiple-value vector returned by a call of fn) the tau system can call bounder-fn on the intervals containing certain arguments of fn.

Let us start with an example. Let fn be the addition function, + (actually, binary-+). Consider the target term (+ x y) and contemplate the question: if you know intervals containing x and y, say intx and inty respectively, what is an interval containing their sum? The answer is pretty easy to state in English: the domain of the answer interval is the less restrictive of the domains of intx and inty. The lower bound of the answer interval is the sum of the lower bounds of intx and inty, and the lower relation is the stronger of the lower relations of intx and inty. Analogous comments define the upper bound and relation of the answer interval. So for example, if x is an INTEGERP such that 0 <= x <= 10 and y is a RATIONALP such that 0 < y <= 20, then (+ x y) is a RATIONALP such that 0 < (+ x y) <= 30.

Defining this precisely is more tedious than describing it in English because one must make precise the notions of ``less restrictive'' domains, ``weaker'' relations, and the possibility that either or both of the bounds could be ``infinite.'' But we can easily imagine defining the function bounder-for-+ that returns the answer interval described, given intx and inty.

Then the following Bounder Form 1 formula establishes the correctness of bounder-for-+ and allows the tau system to use it to produce bounds in the tau computed for +-expressions:

(implies (and (tau-intervalp intx)
              (tau-intervalp inty)
              (in-tau-intervalp x intx)
              (in-tau-intervalp y inty))
         (and (tau-intervalp (bounder-for-+ intx inty))
              (in-tau-intervalp (+ x y)
                                (bounder-for-+ intx inty))))

For example, suppose we have a formula with the following hypotheses

(and (integerp a)
     (<= 0 a)
     (<= a 10)
     (rationalp b)
     (< 0 b)
     (<= b 20))

and suppose the tau system encounters the term (+ a b). When the term is encountered, the tau for a would include an INTEGERP interval such that 0 <= a <= 10 and the tau for b would include a RATIONALP interval such that 0 < b <= 20. In its most primitive configuration, the tau system would only know that the tau for (+ a b) includes the recognizer RATIONALP (and all that it is known to imply). But after the bounder theorem above is proved and available as a :tau-system rule the tau system would infer that (+ a b) was in the RATIONALP interval such that 0 < (+ a b) <= 30.

Thus, by defining bounder functions and proving them correct the user can give the tau system the ability to compute the bounds on function calls as a function of the known bounds on their actuals.

It is sometimes useful to restrict the domains of the intervals to be considered. For example, in bounding *-expressions it is simplifying to restrict one's attention to intervals over the integers or rationals (and thus exclude the complex rationals so one need not think about the getting negative bounds by multiplying two ``positive'' complex rationals or how to ``round up'' from complex bounds to the rationals required by our intervals).

If we were to define bounder-for-* so that it works correctly to bound *-expressions, but only for integer or rational arguments, its correctness theorem would be:

(implies (and (tau-intervalp intx)                             ; (a)
              (tau-intervalp inty)
              (or (equal (tau-interval-dom intx) 'INTEGERP)    ; (b)
                  (equal (tau-interval-dom intx) 'RATIONALP))
              (or (equal (tau-interval-dom inty) 'INTEGERP)
                  (equal (tau-interval-dom inty) 'RATIONALP))
              (in-tau-intervalp x intx)                        ; (c)
              (in-tau-intervalp y inty))
         (and (tau-intervalp (bounder-for-* intx inty))       ; (d)
              (in-tau-intervalp (* x y)                        ; (e)
                                (bounder-for-* intx inty))))

In this case, bounder-for-* would be applied to the intervals for x and y only if those intervals were over the integers or the rationals.

The above theorem for bounder-for-* begins to suggest the general form of a bounder theorem and we will use it to explain the general form.

The hypotheses of a bounder theorem must be a conjunction and the conjuncts must be partitionable into three parts, (a), (b), and (c). The conclusion, must be a conjunction, must contain at least two conjuncts, (d) and (e), and is allowed to contain others that are simply ignored for purposes of bounders. (See the note below about why we allow but ignore additional conjuncts in the conclusion.)

Part (a) introduces some distinct ``interval variables,'' here called ``ivars,'' that are known to denote intervals; for the example above, the ivars are intx and inty. Each hypothesis in part (a) is of the form (TAU-INTERVALP ivar).

Part (b) allows us to restrict the domains of some of the intervals. Each hypothesis in part (b) must be a disjunction and each of the disjuncts must be of the form (EQUAL (TAU-INTERVAL-DOM ivar) 'dom), where ivar is one of the interval variables and dom is one of INTEGERP, RATIONALP, ACL2-NUMBERP, or NIL. It is not necessary to restrict every interval variable. Indeed, part (b) may be empty, as in the theorem for bounder-for-+ above.

Part (c) consists of a set of (IN-TAU-INTERVALP avar ivar) hypotheses where each avar is a variable and no two hypotheses in part (c) use the same avar or ivar. We call the set of all such avar the ``actual variables'' or ``avars.'' The avars and ivars must be distinct. Part (c) sets up a correspondence between the avars and the ivars, each avar is in an interval denoted by one ivar.

Part (d) introduces the name of the bounder function, here bounder-for-*, and the order of its ivar arguments. We see that bounder-for-* takes two arguments and they correspond, in order, to the intervals containing x and y. Part (d) also establishes that the bounder function always returns an interval under hypotheses (a), (b), and (c). Note that it is sometimes useful to return the ``universal interval'' (one that contains everything) if you don't want to compute a better interval for some case; see tau-intervalp or in-tau-intervalp.

Part (e) introduces the name of the function being bounded, here *, and the order of its arguments. It establishes that the function being bounded really is bounded by the interval computed by the bounder function. In general, the function being bounded may take additional arguments. It is possible that the function being bounded takes some arguments that do not affect the bounds of its output.

Thus, parts (c) and (e) together establish a mapping between the actuals of a call of the function being bounded and the intervals to be supplied to the bounder.

The parts identified above may be presented in any order and the literals constituting those parts may be mingled. Thus, for example, here is another version of the theorem above that generates the same bounding information for the tau system. In this version, the hypotheses and conclusions are rearranged, bounder-for-* takes its arguments in the opposite order, and the theorem includes an additional conclusion.

(implies (and (tau-intervalp intx)                             ; (a)
              (or (equal (tau-interval-dom intx) 'INTEGERP)    ; (b)
                  (equal (tau-interval-dom intx) 'RATIONALP))
              (in-tau-intervalp x intx)                        ; (c)

              (tau-intervalp inty)                             ; (a)
              (or (equal (tau-interval-dom inty) 'INTEGERP)    ; (b)
                  (equal (tau-interval-dom inty) 'RATIONALP))
              (in-tau-intervalp y inty))
         (and (in-tau-intervalp (* x y)                        ; (e)
                                (bounder-for-* inty intx))
              (tau-intervalp (bounder-for-* inty intx))        ; (d)))

              (or (equal (tau-interval-dom (bounder-for-* inty intx))
                         'INTEGERP)
                  (equal (tau-interval-dom (bounder-for-* inty intx))
                         'RATIONALP))

Note on why bounder forms allow additional conjuncts in the conclusion: It is often the case that one creates bounders by composing other bounders. To prove compositional bounds correct one must often prove more than the mere correctness of the components. For example, one might need to prove that the domain of the new bounding interval is INTEGERP or otherwise restricted. We allow such ``unnecessary'' conclusions simply to save the user the burden of stating multiple theorems.

An Illustration of Bounder Form 2: Suppose (quad i) is defined so that truncates the integer i to the largest multiple of 4 weakly below i and, additionally, returns the remainder. For example, (quad 26) returns (mv 24 2). Then here are bounders for each of its return values:

(defun quad-bounds-0 (i)
  (cond ((and (tau-interval-lo i)
              (<= 0 (tau-interval-lo i)))
         (make-tau-interval 'integerp nil 0 nil (tau-interval-hi i)))
        (t (make-tau-interval nil nil nil nil nil))))

(defun quad-bounds-1 (i)
  (cond ((and (tau-interval-lo i)
              (<= 0 (tau-interval-lo i)))
         (make-tau-interval 'integerp nil 0 nil 3))
        (t (make-tau-interval nil nil nil nil nil))))

Note that the bounders assume i is an INTEGERP and return the universal interval when i is not a natural.

As noted in the discussion below about how to prove bounder correctness theorems, proving these bounders correct will require an arithmetic book, e.g.,

(include-book "arithmetic-5/top" :dir :system)

Here then are two bounder correctness theorems of Form 2:

(defthm quad-bounds-0-correct
  (implies (and (tau-intervalp i)
                (equal (tau-interval-dom i) 'INTEGERP)
                (in-tau-intervalp x i))
           (and (tau-intervalp (quad-bounds-0 i))
                (in-tau-intervalp (mv-nth 0 (quad x))
                                  (quad-bounds-0 i))))
  :rule-classes :tau-system)

(defthm quad-bounds-1-correct
  (implies (and (tau-intervalp i)
                (equal (tau-interval-dom i) 'INTEGERP)
                (in-tau-intervalp x i))
           (and (tau-intervalp (quad-bounds-1 i))
                (in-tau-intervalp (mv-nth 1 (quad x)) (quad-bounds-1 i))))
  :rule-classes :tau-system)

As noted above, if these bounders are to be used in constructing other bounders, we might include (in the first theorem) an additional concluding conjunct, such as

(equal (tau-interval-dom (quad-bounds-0 i)) 'INTEGERP)

so that we can keep quad-bounds-0 disabled to allow us to use quad-bounds-0-correct as a :rewrite or other rule and still relieve hypotheses about the domain of the interval it produces. These hypotheses would arise if some other verified bounder was called on the produced interval. In addition, as noted below, we might replace the :rule-classes above with

:rule-classes
 ((:rewrite)
  (:forward-chaining :trigger-terms ((quad-bounds-0 i))))

Since the theorem is being stored as some kind of rule and since it satisfies the Bounder Form 2 shape, it will additionally be stored as a :tau-system rule.

Note on proving bounder theorems: Proving bounder theorems is just like proving any other arithmetic theorem and you will need whatever libraries are appropriate for the problem domain you are working in. Do not expect the tau system to be of much use in proving bounder theorems. A typical bounder theorem might require you to prove a subgoal like (< (fn x y) (g (tau-interval-hi int1) int2)). But tau deals with inequalities relating terms to constants, e.g., (< ... 16). A bounder theorem is a sort of ``metatheorem'' about how to construct bounded intervals from other bounded intervals. So when you undertake to define a bounder and prove it correct, go into the project with your eyes open!

But bounder functions can be broadly divided into two classes, those defined in terms of arithmetic on the interval bounds and those defined in terms of other bounders. For example, given that

(LOGXOR x y) = (LOGNOT (LOGEQV x y))

an interval for bounding LOGXOR can be constructed by composing the constructions of intervals for LOGEQV and LOGNOT. So some bounder correctness proofs will involve direct manipulation of arithmetic inequalities and others might involve appeal to the correctness of other bounders, depending on how the new bounder is defined.

Regardless of which style of bounder we are dealing with, we have found it useful to prove the basic theorems relating the tau interval accessors to make-tau-interval, e.g.,

(equal (tau-interval-dom (make-tau-interval dom lo-rel lo hi-rel hi)) dom)

and then disable those functions to avoid seeing excessive cars and cdrs.

When dealing with bounders defined in the direct, arithmetic style, we tend to keep tau-intervalp and in-tau-intervalp enabled so they unfold and expose the algebra.

When dealing with bounders defined compositionally in terms of other verified bounders, we tend to keep tau-intervalp and in-tau-intervalp disabled so we can rely on the previously proved bounder theorems as rewrite and forward chaining rules.

Note that this last remark means that when you prove bounder correctness theorems you should include corollaries that are useful :rewrite and possibly :forward-chaining rules if you anticipate using that bounder in more complex ones. We tend to trigger the forward chaining with the bounder expression itself, rather than one of the hypotheses. For example in the rule above for bounder-for-* we would include (:forward-chaining :trigger-terms ((tau-bounder-expt2 int2))) and let the in-tau-intervalp hypotheses select the free variables x and y.