Lemma Speculation

One way of removing the accumulating and nested term structure is to propose a wave rule which moves this difference to the top of the term leaving the skeleton unchanged. We hope either that it will then cancel against wave-fronts on the other side of the equality or that it will disappear in the process of being moved. For the theorem, after generalization (which is discussed in the next section) the divergence pattern suggests a rule of the form, where is a second order variable which we need to instantiate. Instantiating is ultimately a difficult synthesis problem so we can only hope to have heuristics that will work some of the time. Two of the heuristics used by the divergence critic to instantiate are cancellation and petering out.

The cancellation heuristic uses difference matching to identify term structure accumulating on the opposite side of the sequence which would allow cancellation to occur. Failing that, the cancellation heuristic looks for suitable term structure to cancel against in a new sequence (the original sequence is usually a divergence pattern of a step case, whilst the new sequence is usually a divergence pattern of a base case). In the example, successor functions accumulate at the top of the left hand side of the diverging equations,

This divergence pattern suggests that should be instantiated to to enable immediate cancellation. Thus, as required, the cancellation heuristic suggests the rule,

The other heuristic used to instantiate the right hand side of speculated lemmas is petering out. In moving the differences up to the top of the term, they may disappear altogether. Consider, for example, the theorem, where isort is insertion sort and is true iff a list is sorted into order. These are defined by the conditional rewrite rules,

where , which inserts the element into the list in order, and are defined by the rewrite rules,

Divergence analysis of SPIKE's attempt to prove this theorem suggests the need for a rule of the form, The petering out heuristic instantiates to the identity function . This gives the rule, This rule allows the proof to go through without divergence.

As a more complex example, consider the theorem, where is defined by the rewrite rules,

SPIKE's diverging attempt to prove this theorem generates the equations,

Divergence analysis identifies term structure accumulating in two different places,

This is the unique maximal difference match. This divergence pattern suggests the need for a rewrite rule of the form, The petering out heuristic instantiates to the identity function giving the rule, This rule allows the proof to go through without divergence.

Since the erasure of the wave rule must be properly typed, sort information can be used to prune inappropriate instantiations for . All speculated lemmas are therefore filtered through a type checker. Speculated lemmas are also filtered through a conjecture disprover. When a confluent set of rewrite rules exists for ground terms, exhaustive normalization of some representative set of ground instances of the equations is used to filter out non-theorems. Alternatively, the prover itself could be used to filter out non-theorems. Unlike many other induction theorem provers, SPIKE can refute conjectures since its inference rules are refutationally complete for conditional theories in which the axioms are ground convergent and defined functions are completely defined over free constructors [6]. Other techniques for disproving conjectures are described by Protzen (1992).

The critic's lemma speculation is summarized in Figure 2 (using the same variable names as the preconditions).

This specification again uses second order variables in a limited manner. First order difference matching is merely required to construct lemmas. As with the preconditions, the specification of the postconditions can be easily extended to deal with multiple and nested wave-fronts (as in the example). Since the rules proposed by the critic move the wave-fronts to top of the term, they usually only introduce fresh divergence in the rare cases that cancellation or fertilization fails. This is unlikely since the cancellation and petering out heuristics attempt to ensure precisely that cancellation or fertilization can take place.