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.