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,