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 . 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.