Major Section: TAU-SYSTEM

whereBounder 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-intervalptarget(bounder-fn i1 ...))))

`(fn x1 ... y1 ...)`

or
`(mv-nth 'n (fn x1 ... y1 ...))`

, depending on whether we are in the
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 `n`

th
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
enountered, 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

`: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

`car`

s and `cdr`

s.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`

.