The lemmas speculated so far have moved accumulating
term structure directly to the top of the term where it is
removed by cancellation or petering out. An alternative
way of removing accumulating term structure is to move
it onto another argument position where: either
it can be removed
by matching with a ``sink'', a universally quantified variable in the
induction hypothesis; or it can be moved upwards by rewriting
with the recursive definitions.
Annotated rewrite rules which preserve the skeleton and
move wave-fronts across to other argument positions are called *transverse* wave rules [9].
Theorems involving functions with accumulators
provide a rich source of examples where such rewrite rules
prevent divergence.

Consider, for example, a theorem about the correctness of tail recursive list reversal, where both and are universally quantified, is naive list reversal using append, and is tail recursive list reversal building the reversed list on the second argument position. These functions are defined by the rewrite rules,

SPIKE's attempt to prove this theorem diverges generating the following sequence of equations which the prover attempts to show by induction,

Difference matching identifies the term structure accumulating within these equations that is causing divergence,

This is the unique maximal difference match.
Rather than move
the accumulating term structure on the
right hand side of the equations to the top of the
term, it is much simpler to move the
accumulating term structure from the first
onto the second argument of the outermost append.
The critic therefore proposes a transverse wave rule,
which preserves the skeleton but moves the difference onto a different
argument position. In this example, this is a rule of the form,
In moving the difference onto another argument position,
the difference may change syntactically. The right hand side
of the lemma is therefore only partially determined. To instantiate ,
the critic uses two heuristics: *fertilization* and
*simplification*.

The fertilization heuristic
uses matching to find an instantiation for
which enables immediate fertilization. In this case,
matching against the universally quantified
variable in the induction hypothesis suggests,
Finally the critic generalizes the lemma using the
same extended primary term heuristic as before
(*i.e.*, augmenting recursive positions
with wave-hole positions). This gives the rule,
This is exactly the rule needed by SPIKE to complete the proof.
In addition, it is simple enough to be proved by itself
without divergence; this is not true of the
ungeneralized rule.

The other heuristic used to instantiate the right hand side of the speculated lemma is the simplification heuristic. The heuristic uses regular matching to find an instantiation for which will enable the wave-front to be simplified using one of the recursive definitions. Consider again the theorem from the introduction. Divergence analysis identifies successor functions accumulating on the first argument position of +. This accumulating term structure can either be moved to the top of the term tree or alternatively onto the second argument position of + using a transverse wave rule of the form, The right hand side of this transverse wave rule is instantiated by the simplification heuristic. The wave-front on the right hand side can be simplified by the rewrite rule recursively defining + if is instantiated by . That is, if we have the rule, This rule allows the proof to go through without divergence.

Speculated transverse wave rules are generalized using the
extended primary terms heuristic described in Section 5.
The divergence critic also generalizes transverse wave
rules by means of an *equality* heuristic. This heuristic attempts to
cancel equal outermost functors where possible.
For example, consider the theorem,
where addition is defined recursively on
its second argument position and
subtraction is defined by the rewrite rules,

SPIKE's attempt to prove this theorem diverges generating (amongst others) the goals,

Divergence analysis identifies accumulating term structure within these equations,

This is the unique maximal difference match. These annotations suggest the need for the transverse rule, The equality heuristic deletes the equal outermost function, . This gives the more general lemma,

All speculated lemmas are filtered through a type checker to ensure that their erasure is well typed. Speculated lemmas are also filtered through a conjecture disprover to guard against over-generalization.

The actions of the critic are summarized in Figure 3.

The specification of preconditions and postconditions again uses second order variables but in a limited manner. The implementation merely requires second order matching and first order difference matching. The preconditions and postconditions can be easily generalised to include multiple and nested annotations. We could also speculate hybrid wave rules which ripple part of the wave-front across and part of it up the term tree. However, such rules appear to be rare. In addition, such hybrid wave rules can often be decomposed into a pair of wave rules, one of which moves some of the wave-fronts up the term tree, and another which moves the wave-fronts across.

Fri Apr 12 12:14:22 BST 1996