January 22, 2013

Defining and Proving Interval Bounds for Arithmetic Functions

J Moore

Abstract:

Consider (+ x y) and suppose we know that the inputs, x
and y, are contained in two intervals, int1 and int2.
We wish to compute from int1 and int2 an interval
containing (+ x y).  For example, if x is known to be
an INTEGERP such that 1 <= x <= 16 and y is a RATIONALP
such that 0 < y (with no known upper bound), then (+ x
y) is known to be in the RATIONALP interval such that 1
< (+ x y) (with no known upper bound).  I call the
function that takes two intervals containing x and y
respectively and returns an interval containing (fn x
y) a ``bounder'' for fn.

I have developed a book that defines bounders for +, *,
/, FLOOR, MOD, LOGAND, LOGNOT, LOGIOR, LOGORC1, LOGEQV,
LOGXOR, EXPT2, and ASH.  The book proves the
correctness of each bounder.  In future work I hope to
extend ACL2 so that users can define and verify
bounders to improve the tau system.  The present work
is an exploration of the shape and content of such
bounder theorems.  Ideally, the present book would just
become part of an arithmetic package and not be built
into ACL2.

I will discuss some of the bounders defined, their
correctness theorems, two of the basic proofs
illustrating two different styles of bounder
definitions and proofs, and some of the issues
confronted in finding accurate bounds.