LP, the Larch Prover — Polynomial orderings

The polynomial ordering can be used to prove the termination of sets of rewrite rules involving associative-commutative operators. Because it requires considerable user input, it is generally used only to experiment with termination proofs of small sets of rewrite rules, not to orient large sets of equations into rewrite rules.

Syntax

<polynomial-constraint> ::= polynomials <operator> <polynomial>*[,]
<polynomial>            ::= <polynomial-term> ( "+" <polynomial-term> )*
<polynomial-term>       ::= <polynomial-factor> ( "*" <polynomial-factor> )*
<polynomial-factor>     ::= <polynomial-primary> [ "^" <number> ]
<polynomial-primary>    ::= <variable> | <number> | "(" <polynomial> ")"

Examples

polynomials + x + y + 1, x + 2

Usage

The polynomial ordering is based on user-supplied interpretations of operators by sequences of polynomials. The ordering extends these interpretations to terms by interpreting a variable by a sequence of identity polynomials and a compound term by the interpretation of its principal operator applied to the interpretations of its arguments. One term is less than another in the polynomial ordering if its interpretation is lexicographically less than that of the second term (one polynomial is less than another if its value is less than that of the other for all values of its variables).

The command set ordering polynomial n sets the current ordering-method to a polynomial ordering based on sequences of length n; the default value of n is 1.

The command register polynomial op p1, ..., pn assigns the sequence p1, ..., pn of polynomials as the polynomial interpretation of the operator op. If no polynomials are specified, LP prompts the user to enter them on the following lines. The polynomials are entered like standard LP terms, using the binary operators +, *, \and fq{^} (for exponentiation), the variables in the prompt, and positive integer coefficients. LP understands operator precedence for terms representing polynomials, so these terms need not be fully parenthesized..

If the sequence of polynomials associated with an operator is longer than the length of the current polynomial ordering, the extra polynomials are ignored. If it is shorter, it is extended by replicating its last element.

Each operator has a default interpretation. Suggestions for assigning polynomials: 

(1) f nullary                           I[f]   = 2
(2) f(x1,...,xn) -> t  [f not in t]     I[f]   = I[t] + 1
(3) h(f(t1,...,tn)) ->                  I[h]   = a*(x^i) with i > 1
       f(h(t1),...,h(tn))               I[f]   = x1 + ... + xn
(4) f associative                       I.1[f] = (a*x*y) + x with a > 0
    f(f(x,y),z) -> f(x,f(y,z))          I.2[f] = (a*(x^i)) + y with a, i > 0
(5) f associative                       I.1[f] = (a*x*y) + y with a > 0
    f(x,f(y,z)) -> f(f(x,y),z)          I.2[f] = x + (a*(y^i)) with a, i > 0
(6) f associative-commutative           I[f]   = (a*x*y) + (b*(x+y)) + c
                                                 with ac + b - b^2 = 0
(7) f, g associative-commutative        I[f]   = a*x*y with a > 0
    g distributive over f               I[g]   = x + y
                                    or  I[f]     as in (6) with a > 0
                                        I[g]   = x+y+d     with d = b/a
(8) f should be rewritten to g          degree(I.1[f]) > degree(I.1[g])