LP, the Larch Prover -- The critical-pairs command

The critical-pairs command provides a method of forward inference that produces consequences from pairs of rewrite rules. This method can be used to increase the amount of confluence in LP's rewriting system.

Syntax

<critical-pairs-command> ::= critical-pairs <names> with <names>

Examples

critical-pairs *Hyp with *

Usage

The critical-pairs command directs LP to compute critical pair equations between the rewrite rules named by the first <names> and those named by the second. LP adds any nontrivial critical pair equations (i.e., nonidentities) to its logical system. If LP reduces the current conjecture to an identity upon orienting a critical pair equation into a rewrite rule, it terminates the critical pair computation. LP performs critical pair computations in the order determined by the combined sizes of the left sides of the rewrite rules.

LP also computes critical pairs in response to the complete command. LP keeps track of which rewrite rules have had their critical pairs computed, and does not recompute critical pairs between those rules. See also the forget command.

Critical pair equations between two rewrite rules result from using them to rewrite a common term in two different ways. Suppose that R1 is the rewrite rule l1 -> r1 and R2 is l2 -> r2. Suppose also that R1 and R2 have no variables in common (LP ensures that this is the case by substituting fresh variables for those in R2). If l2 can be unified with a nonvariable subterm of l1, then both R1 and R2 can be used to rewrite some substitution instance of l1. A critical pair equation between R1 and R2 is an equation relating the results of these two rewritings.

More precisely, if s1 is a nonvariable subterm of l1 that does not contain any variables bound by outer quantifiers in l1, if sigma is a substitution that unifies l2 with s1 and that does not introduce any variables bound by outer quantifiers in l1, and if l1' is the result of substituting r2 for s2 in l1, then sigma(l1') = sigma(r1) is a critical pair equation between R1 and R2.

Examples:

    Rewrite rules                        Critical pair equations

1.  f(x) * f(y)        -> f(x * y)       b * f(y) = f(a * y)
    f(a)               -> b              f(x) * b = f(x * a)

2.  P(x) => Q(x)       -> true           true => Q(c) <=> true
    P(c)               -> true             ... which reduces to Q(c)

3.  \E x (f(x) = g(y)) -> true           \E x (f(x) = c)
    g(c)               -> c

When the principal operator of l1 or l2 is an ac operator, say *, LP generalizes the critical pair computation by computing Petersen-Stickel extensions Ri' having the form li*x -> ri*x of R1 and R2, and then by computing critical pair equations between {R1, R1'} and {R2, R2'}. Thus, i(x) * x -> e has three nontrivial critical pair equations with itself when * is ac:

i(e) * e = e, which results from unifying i(x) * x with the nonvariable subterm y * z of the left side of i(y) * y * z -> z,
e * x = i(i(x)) * e, which results from the unifier i(i(x)) * i(x) * x of i(x) * x * y and i(x') * x' * y' (via the map from x' to i(x) and y' to x), and
e * i(x) = i(x*y) * e * y, which results from the unifier i(x*y) * i(x) * x * y of the same terms (via the map from x' to x*y and y' to i(x)).