A technique for controlling term rewriting using annotations to restrict application and to ensure termination. A target expression is rippled with respect to one or more source expressions. Each source expression embeds in the target expression. Annotations in the target mark those subexpresions which correpond to bits of the source (the skeleton) and those which do not (the wave-fronts). The target is rewritten so that the embeddings are preserved, ie rewriting can only move the wave-fronts around within the skeleton - wave-fronts can change but the skeleton cannot. Furthermore, wave-fronts are given a direction (outwards or inwards) and movement can only be in that direction. Outwards wave-fronts can mutate to inwards, but not vice versa. This ensures termination. Rippling can be implemented by putting wave annotation into the rewrite rules to turn them into wave-rules. The successful application of wave-rule requires that any wave-front in the wave-rule must match a wave-front in the target. Rippling was originally developed for guiding the step cases of inductive proofs, in which the sources are the induction hypotheses and the target is the induction conclusion.
For an informal introduction to rippling with lots of examples see: Bundy, A., Stevens, A., van Harmelen, F., Ireland, A. and Smaill, A., Rippling: A Heuristic for Guiding Inductive Proofs. AI Journal, vol. 62, pp 185-253, 1993. For a more formal account see: Basin, D.A. and Walsh, T., A calculus for and termination of rippling, JAR, vol. 16, no. 1-2, pp 147-180, 1996.
No. Many lemmas and other axioms can also be annotated as wave-rules. Examples include: associative laws; distributive laws; replacement axioms for equality; many logical axioms; etc. Equations which cannot be expressed as wave-rules include commutative laws and (usually) the step cases from mutually recursive definitions. The latter can be expressed as wave-rules in an abstraction in which the mutually defined functions are regarded as indistinguishable.
Rippling differs from standard rewriting in two ways. Firstly, the wave annotation may prevent the application of a wave-rule which, viewed only as a rewrite rule, would otherwise apply. This will happen if the left-hand side of the wave-rule contains a wave-front which does not match a wave-front in the expression being rewritten. Secondly, equations can usually be oriented as wave-rules in both directions, but without loss of termination. The wave annotations prevent looping. An empirical comparison of rippling and rewriting can be found in Bundy, A. and Green, I., An experimental comparison of rippling and exhaustive rewriting., Edinburgh Technical Report, forthcoming.
No. If all the rewrite rules in a non-terminating set can be annotated as wave-rules then the additional conditions of wave annotation matching, imposed by rippling, will ensure that rippling still terminates. Examples are provided by the many rewrite rules which can be annotated as wave-rules in both directions, and may even both be used in the same proof, without loss of termination.
No, each skeleton gives (in essence) a different termination ordering which guides proof towards fertilization with that skeleton. Different annotations on the same term can result in completely different rewritings.
"Wave-rule" can be formally defined. It is a rewrite rule containing wave annotation in which the skeletons are preserved and the wave-front measure of the right-hand side is less than that of the left-hand side. Informally, the skeleton consists of those bits of the expression outside of wave-fronts or inside the wave-holes. The measure records the position of the wave-fronts in the skeleton. It decreases when outwards directed wave-fronts move out or downwards wave-fronts move in. A formal definition of skeleton and of the wave-front measure can be found in Basin, D.A. and Walsh, T., A calculus for and termination of rippling, JAR, vol. 16, no. 1-2, pp 147-180, 1996..
Wave annotation can be inserted in expressions by a family of difference unification algorithms invented by Basin and Walsh (see Basin, D.A. and Walsh, T., Difference Unification. Proc. of IJCAI-93, 1993). These algorithms are like unification but with the additional ability to hide non-matching structure in wave-fronts. Ground difference matching can be used to insert wave annotation into induction rules and ground difference unification for wave-rules. "Ground" means that no instantiation of variables occurs. "Matching" means that wave-fronts are inserted only into the induction conclusion and not the induction hypothesis. "Unification" means that wave-fronts are inserted into both sides of wave-rules. Note that the process of inserting wave annotations can be entirely automated.
Yes. Rippling has been used successfully in the verification of the Gordon microprocessor and the synthesis of a decision procedure and of the rippling tactic itself. It has also been used outwith inductive proofs for the summing of series and the Lim+ theorem. A survey of some of these successes can be found in Bundy, A., Rippling: Greatest Hits. Edinburgh technical report, forthcoming.
Yes, if there is no wave-rule available to move a wave-front. In this case we apply critics to try to patch the partial proof. For inductive proofs, for instance, these may: generalise the induction formula; revise the induction rule; introduce a case split; or introduce and prove an intermediate lemma, according to the precise circumstances of the breakdown. The fact that a failed ripple provides so much information to focus the attempt to patch the proof is one of the major advantages of rippling. More details about critics, including some hard examples which have been proven with their use, can be found in Ireland, A. and Bundy, A.Productive use of failure in inductive proof. JAR, vol. 16, no. 1-2, pp 79-111, 1996.
There is a one-level look-ahead into the rippling process to see what induction rules would permit rippling to take place. In particular, which wave-fronts placed around which induction variables would match with corresponding wave-fronts in induction rules. We call this ripple analysis. It is similar to the use of recursive definitions to suggest induction rules, as pioneered by Boyer and Moore, but differs in that all available wave-rules are used in ripple analysis, and not just recursive definitions. More detail of ripple analysis can be found in Bundy et al, A rational reconstruction and extension of recursion analysis, Procs. of IJCAI-89, Morgan Kaufmann, pp 359-365, 1989, although that paper is rather old now and is not a completely accurate description of current CLaM implementations. In particular, the term "ripple analysis" was not in use when that paper was written and it is misleadingly called "recursion analysis" there.
The boxes form hollow squares, which help to display the outwards or inwards movement of wave-fronts. Orange was used because it is one of the few transparent overhead pen colours, allowing the expression in the wave-front to show through. [Famously, Pete Madden coloured his wave-fronts red for a conference talk. The underlying expressions were made invisible, ruining his presentation. Ah Pete! -- the source for so many of Life's Little Lessons.]
Raymond Aubin coined the term "rippling-out", in his 1976 Edinburgh PhD thesis, to describe the pattern of movement of what we now call wave-fronts, during conventional rewriting with constructor style recursive definitions. In Bundy, A. The use of explicit plans to guide inductive proofs Procs. of CADE-9, Springer Verlag LNCS 310, pp 111-120, 1988. we turned this on its head by taking such a movement of wave-fronts as the definition of rippling rather than the effect of rewriting. This enabled the idea to be considerably generalised. Later we invented "rippling-sideways", "rippling-in", etc and so generalised the combined technique to "rippling".