LINEAR

make some arithmetic inequality rules 
Major Section:  RULE-CLASSES

See rule-classes for a general discussion of rule classes and how they are used to build rules from formulas. An example :corollary formula from which a :linear rule might be built is: 

Example:
(implies (and (eqlablep e)           if inequality reasoning begins to
              (true-listp x))        consider how (length (member a b))
         (>= (length x)              compares to any other term, add to
             (length (member e x)))) set of known inequalities the fact
                                     that it is no larger than (length b),
                                     provided (eqlablep a) and (true-listp b)
                                     rewrite to t


General Form:
(and ...
     (implies (and ...hi...)
              (implies (and ...hk...)
                       (and ...
                            (rel lhs rhs)
                            ...)))
     ...)
Note: One :linear rule class object might create many linear arithmetic rules from the :corollary formula. To create the rules, we first flatten the and and implies structure of the formula, transforming it into a conjunction of formulas, each of the form 
(implies (and h1 ... hn) (rel lhs rhs))
where no hypothesis is a conjunction and rel is one of the inequality relations <, <=, =, >, or >=. If necessary, the hypothesis of such a conjunct may be vacuous.

We create a :linear rule for each such conjunct, if possible, and otherwise cause an error. Each rule has one or more ``trigger terms'' which may be specified by the user using the :trigger-terms field of the rule class or which may be defaulted to values chosen by the system. We discuss the determination of trigger terms after discussing how linear rules are used.

:linear rules are used by a linear arithmetic decision procedure during rewriting. We describe the procedure very roughly here. Fundamental to the procedure is the notion of a linear polynomial inequality. A ``linear polynomial'' is a sum of terms, each of which is the product of a rational constant and an ``unknown.'' The ``unknown'' is permitted to be 1 simply to allow a term in the sum to be constant. Thus, an example linear polynomial is 3*x + 7*a + 2; here x and a are the (interesting) unknowns. In our case, the unknowns need not be variable symbols. For example, (length x) might be used as an unknown in a linear polynomial. Thus, another linear polynomial is 3*(length x) + 7*a. A ``linear polynomial inequality'' is an inequality (either < or <=) relation between two linear polynomials. Certain linear polynomial inequalities can be combined by cross-multiplication and addition to permit the deduction of a third linear inequality polynomial with fewer unknowns. If this deduced inequality is manifestly false, a contradiction has been deduced from the assumed inequalities.

For example, suppose we have three assumptions: 

p1:  3*x + 7*a <  4 
p2:          3 <  2*x
p3:          0 <= a.
By cross-multiplying and adding the first two (that is, multiplying p1 by 2, p2 by 3 and adding the respective sides), we deduce the intermediate result 
p4:  6*x + 14*a + 9 < 8 + 6*x
which, after cancellation, is 
p4:        14*a + 1 <  0.
If we then cross-multiply and add p3 to p4, we get 
p5:               1 <= 0,
a contradiction. Thus, we have proved that p1 and p2 imply the negation of p3.

All of the unknowns of a polynomial must be eliminated by cancellation in order to produce a constant inequality. We can choose to eliminate the unknowns in any order. We eliminate them in term-order, largest unknowns first. (See term-order.) Now suppose that this procedure does not produce a contradiction but instead yields a set of nontrivial inequalities. A contradiction might still be deduced if we could add to the set some additional inequalities allowing additional cancellation. That is where :linear lemmas come in. When the set of inequalities has stabilized under cross-multiplication and addition and no contradiction is produced, we search the data base of :linear rules for rules about the unknowns that are candidates for cancellation (i.e., are the largest unknowns in their respective inequalities).

If the trigger term of some :linear rule can be instantiated to yield a candidate for cancellation, we so instantiate that rule, attempt to relieve the hypotheses with general-purpose rewriting, and, if successful, convert the concluding inequality into a polynomial inequality and add it to the set. This may let cancellation continue. See the discussion of ``Linear Arithmetic Rules'' pp 242 of A Computational Logic Handbook for more details.

We now describe how the trigger terms are determined. Most of the time, the trigger terms are not specified by the user and are instead selected by the system. However, the user may specify the terms by including an explicit :trigger-terms field in the rule class, e.g., 

General Form of a Linear Rule Class:
(:LINEAR :COROLLARY formula
         :TRIGGER-TERMS (term1 ... termk))
Each termi must be a term and must not be a variable, quoted constant, lambda application, let-expression or if-expression. In addition, each termi must be such that if all the variables in the term are instantiated and then the hypotheses of the corollary formula are relieved (possibly instantiating additional free variables), then all the variables in the concluding inequality are instantiated. We generate a linear rule for each conjuctive branch through the corollary and store each rule under each of the specified triggers. Thus, if the corollary formula contains several conjuncts, the variable restrictions on the termi must hold for each conjunct.

Note: Problems may arise if you explicitly store a linear lemma under a trigger term that, when instantiated, is not the largest unknown in the instantiated concluding inequality. Suppose for example you store the linear rule (<= (fn i j) (/ i (* j j))) under the trigger term (fn i j). Then when the system ``needs'' an inequality about (fn a b), i.e., because (fn a b) is the largest unknown in some inequality in the set of assumed inequalities, it will appeal to the rule and deduce (<= (fn a b) (/ a (* b b))). However, the largest unknown in this inequality is (/ a (* b b)) and hence this inequality will not be used until that term is eliminated by cancellation with some other inequality. It is generally best to specify as a trigger term one of the ``maximal'' terms of the polynomial, as described below.

If :trigger-terms is omitted the system computes a set of trigger terms. Each conjunct of the corollary formula may be given a unique set of triggers depending on the variables that occur in the conjunct and the addends that occur in the concluding inequality. In particular, the trigger terms for a conjunct is the list of all ``maximal addends'' in the concluding inequality.

The ``addends'' of (+ x y) and (- x y) are the union of the addends of x and y. The addends of (- x) and (* n x), where n is a numeric constant, is in all cases just {x}. The addends of an inequality are the union of the addends of the left- and right-hand sides. The addends of any other term, x, is {x}.

A term is maximal for a conjunct (implies hyps concl) of the corollary if (a) the term is a non-variable, non-quote, non-lambda application, non-let and non-if expression, (b) the term contains enough variables so that when they are instantiated and the hypotheses are relieved then all the variables in concl are instantiated, and (c) any instantiation of the term is always at least as ``large'' (see term-order for a description of the order used) as the corresponding instantiations of any other addend in concl.