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.