Next: Divergence Analysis Up: A Divergence Critic for Previous: Introduction

Difference matching and rippling

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.

Next: Divergence Analysis Up: A Divergence Critic for Previous: Introduction
Fri Apr 12 12:14:22 BST 1996