Next: Transverse Wave Rules Up: A Divergence Critic for Previous: Lemma Speculation


A major cause of divergence is the need to generalize. Most of the lemmas proposed by the critic fix divergence, but attempting to prove the lemmas themselves can cause fresh divergence. In addition, several speculated lemmas can sometimes be replaced by a single generalization. Generalized lemmas also can lead to shorter, more elegant and natural proofs. The critic therefore attempts to generalize the lemma speculated, using the conjecture disprover to guard against over-generalization.

The main heuristic used for generalization is an extension of the primary term heuristic [1]. The primary terms are those terms encountered as a term is explored from the root to the leaves ignoring non-recursive argument positions to functions. The same notion of recursive argument position is used by the critic as defined by Bouhoula and Rusinowitch (1995a) and as used by SPIKE for performing inductions. Consider, for example, the theorem, where + is again defined recursively on its second argument, and and are defined by means of the rewrite rules,

This problem is taken from the CLAM library corpus [10]. SPIKE's attempt to prove this theorem diverges. One of the sequences of equations generated is,

Difference matching identifies the term structure causing divergence,

This is the unique maximal difference match. These annotations suggest the need for the wave rule, A set of candidate terms for generalization is constructed by computing the intersection of the primary terms of the two sides of this rule. In this case, the primary terms of the left hand side are the set , and the primary terms of the right hand side are the set . The intersection of the primary terms is thus the set . The critic picks members of the intersection to generalize to new variables. Picking justs gives an equivalent lemma up to renaming of variables. Picking gives the generalization,

The reason for considering just primary terms is that the recursive definitions typically provide wave rules for removing term structure which accumulates at these positions. In addition to primary terms, the divergence critic therefore also considers the positions of the wave-holes (but not wave-fronts) in the skeleton of the lemma being speculated. The motivation for this extension is that the speculated lemma will allow accumulating term structure to be moved from the wave-hole positions; such positions are therefore also candidates for generalization. Positions of the wave-fronts are not included since we want to speculate a lemma that will move the term structure at such positions.

For instance, because of the wave-hole on the first argument of + in the last example, is also included in the intersection set of candidate terms for generalization. Picking to generalize gives, The speculated lemma is now as general as is possible. This rule allows the proof to go through without divergence.

The critic also has a heuristic for merging speculated lemmas. For instance, with the theorem , the critic speculates several rules including,

As is a cover set for the natural numbers, these two rules can be merged to give,


Fri Apr 12 12:14:22 BST 1996