Planning and Patching Proof - Artificial Intelligence and Symbolic Computation - page 32

invented 'rippling-sideways', 'rippling-in', etc and so generalized the combined
technique to 'rippling'.

3.2 Relation to Standard Rewriting Techniques

Are Wave-Rules Just the Step Cases of Recursive Definitions? No.
Many lemmas and other axioms can also be annotated as wave-rules. Exam-
ples include: associative laws; distributive laws; replacement axioms for equal-
ity; many logical axioms; etc. Equations that 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. Lots of example
wave-rules can be found in [Bundy

et al , 2005].

How Does Rippling Differ from the Standard Application of Rewrite
Rules? 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 & Green, 1996].

Since Rippling Is Terminating, Is It Restricted to Terminating Sets
of Rewrite Rules? 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. Exam-
ples are provided by the many rewrite rules that can be annotated as wave-rules
in both directions, and may even both be used in the same proof, without loss
of termination.

Couldn't We Simply Perform Rippling Using a Suitable Order, e.g.
Recursive Path Ordering, Without the Need for Annotations? No,
each skeleton gives (in essence) a different termination ordering which guides
the proof towards fertilization with that skeleton. Different annotations on the
same term can result in completely different rewritings.

Is Rippling Restricted to First-Order, Equational Rewriting? No, there
are at least two approaches to higher-order rippling. One is based on view-
ing wave annotation as representing an embedding of the given in the goal
[Smaill & Green, 1996]. The other is based on a general theory of colouring
λ

calculus terms in different ways [Hutter & Kohlhase, 1997].