The initial problem is recognizing when the proof is diverging. Various properties of rewrite rules have been identified which cause divergence like, for example, forwards and backwards crossed systems [12]. However, these properties fail to capture all diverging rewrite systems since the problem is, in general, undecidable. The divergence critic instead studies the proof attempt looking for patterns of divergence; no attempt is made to analyse the rewrite rules themselves for structures which give rise to divergence. The advantage of this approach is that the critic need not know the details of the rewrite rules applied, nor the type of induction being performed, nor the control structure used by the prover. The critic can thus recognise divergence patterns arising from complex mutual or multiple inductions with little more difficulty than divergence patterns arising from simple straightforward inductions. The disadvantage of this approach is that the critic can identify a ``divergence'' pattern when none exists. Fortunately, such cases appear to be rare, and even when they occur, the critic usually suggests a lemma or generalization which gives a shorter and more elegant proof (see Section 8 for an example).
To illustrate the ideas behind the critic's divergence
analysis, consider again the theorem from the introduction,
The divergence critic first partitions the sequence of equations which the prover attempts to prove by induction. This is necessary since several diverging sequences may be interleaved in the prover's output. Several heuristics can be used to reduce the number of partitions considered. The most useful heuristic is parentage in which the sequence is partitioned so that each equation is derived from the previous one. That is, the equations lie on a single branch of the proof tree. In particular, the base case and step case of an induction are partitioned into different sequences. Other heuristics which can be used include: the function and constant symbols which occur in one equation occur in the next equation in the partition, and the weights of the equations in a partition form a simple arithmetic progression. In this case, there is just a single open branch in the proof tree,
The critic then attempts to find the accumulating and nested term structure in each sequence which is causing divergence. In this case, successor functions are accumulating on the first argument of +. To identify this accumulating term structure, the critic uses difference matching. Difference matching successive equations gives the annotated sequence,
This is the unique maximal difference match.
The critic then tries to speculate a lemma which can be
used as a rewrite rule to move
the accumulating and nested term structure out of the way.
In this case, the critic speculates
a rule for moving a successor function off the first argument of +.
That is, the rule,
With this rule, SPIKE is able to prove the
theorem
without divergence. In addition, this rule is sufficiently
simple that it can be proved without assistance.
The heuristics used by the critic to perform this
lemma speculation are
described in more detail in the next two sections.
The divergence analysis performed by the critic is
summarised in Figure 1.
In analysing the divergence, we consider
all the equations which the prover attempts to prove by induction.
This includes those equation where the induction proof succeeds as
these can often suggest useful patterns.
By ``non-trivial'' I wish to
exclude , the identity
substitution.
is thus the accumulating and nested term structure
that appears to be causing divergence.
For the
example,
is
,
is
, and
is
.
Although
and
are second order variables, the second order nature of
the divergence analysis is limited. Indeed, the implementation
of the critic merely requires first order difference matching which is
polynomial. For simplicity,
the preconditions ignore the orientation of equations.
In addition, the preconditions can be easily generalised
to include multiple and nested annotations.
This allows the critic to recognise multiple sources of divergence
in the same equation.
Techniques
which identify accumulating term structure by most
specific generalization [11]
cannot cope with divergence patterns that give
rise to nested annotations (see Section 9 for
more details).
The specification of the preconditions has left the length of sequence undefined. If the sequence is of length 2, then the critic is preemptive. That is, it will propose a lemma just before another induction is attempted and divergence begins. Such a short sequence risks identifying divergence when none exists. On the other hand using a long sequence is expensive to test and allows the prover to waste time on diverging proof attempts. Empirically, a good compromise appears to be to look for sequences of length 3. This is both cheap to test and reliable. To identify accumulating term structure, it appears to be sufficient to use ground difference matching with alpha conversion of variable names. There exists a fast polynomial algorithm to perform such difference matching based upon the ground difference matching algorithm using dynamic programming [3]. Since the skeleton must be well typed (along with the erasure), the algorithm is extended to use sort information to prune potential difference matches.