Rippling is a powerful heuristic developed at Edinburgh for proving theorems involving explicit induction [9] and is implemented in the CLAM theorem prover [10]. In the step case of an inductive proof, the induction conclusion typically differs from the induction hypothesis by the addition of some constructors or destructors. Rippling uses annotations to mark these differences and applies annotated rewrite rules to remove them.

As a simple example, consider again the theorem discussed in the
introduction.
In the step case, the induction hypothesis is,
And the induction conclusion is,
If we ``difference match''
the induction conclusion against the
induction hypothesis [2],
we obtain the following annotated induction
conclusion,
An annotation consists of a *wave-front*, a box with a *wave-hole*, an
underlined term.
Wave-fronts
are always one functor thick
[4]. That is, every
wave-front has one immediate subterm that is annotated with
a wave-hole. To make presentation simpler, we
display adjacent wave-fronts merged. Thus,
is just syntactic sugar for
the annotated term, .
Wave-fronts can also include up and down arrows
to indicate whether they are moving towards the
top of the term tree or down towards the leaves.
This extension can, however, be safely ignored here.

The *skeleton* of an annotated
term is formed by deleting everything that
appears in the wave-front but not in the wave-hole.
The *erasure* of an annotated terms is formed by deleting
the annotations but not the terms they contain. In this case,
the skeleton of the annotated induction conclusion is identical to
the induction hypothesis, and
the erasure of the annotated induction conclusion is
the unannotated induction conclusion.
Difference matching guarantees this; that is,
difference matching the induction conclusion with
the induction hypothesis
annotates the induction conclusion so that its skeleton
matches the induction hypothesis.

Formally, is a *difference
match* of with with substitution iff
and
where and build the skeleton and erasure of
the annotated term .
Difference matching is not unitary. That is,
two terms can have more than one difference match.
For example, both and
are difference matches of
with . The number of difference matches
can be reduced if we compute just the
*maximal* difference match in which wave-fronts
are as high as possible in the term tree. A formal
definition of such a well founded ordering on annotated
terms has been given by Basin and Walsh (1994).

The aim of rippling is to rewrite the annotated induction conclusion so that
the skeleton, the induction hypothesis, is preserved and
the differences, the wave-fronts are moved to harmless
places (for example, to the top of the term). If
this rewriting succeeds, we will then be able to appeal to the
induction hypothesis.
To rewrite the annotated induction conclusion, we use
the following annotated rewrite rules, or *wave rules*:

The first two of these annotated rewrite rules are derived from the recursive definitions of and + whilst the second is derived from the lemma proposed at the end of the introduction. Each of these annotated rewrite rules preserves the skeleton of the term being rewritten, and moves the wave-fronts higher up the term tree. Wave rules guarantee this: a wave rule is an annotated rewrite rule with an identical skeleton on left and right hand sides that moves wave-fronts in a well founded direction like, for instance, to the top of the term tree [4].

Rippling on the left hand side of the annotated induction conclusion using (1) yields, Then rippling on the right hand side with (2) gives, Finally rippling with (3) on the right hand side yields, As the wave-fronts are at the top of each term, we have successfully rippled both sides of the equality. We can now appeal to the induction hypothesis on the left hand side giving, This is a simple identity and the proof is complete. Note that to complete the proof, we needed to rewrite with a lemma, (3). The aim of the divergence critic described in this paper is to propose such lemmas.

Rippling has several desirable properties. It is highly goal directed, manipulating just the differences between the induction hypothesis and the induction conclusion. As the annotations restrict the application of the rewrite rules, rippling also involves little or no search. Difference matching and rippling have proved useful in domains outside of explicit induction. For example, they have been used to sum series [20] and to prove limit theorems [21]. In the rest of the paper, I show that difference matching and rippling are also useful in identifying and correcting divergence in a prover that neither uses explicit rules of induction nor uses annotations to control rewriting.

Fri Apr 12 12:14:22 BST 1996