The Termination of Rippling and Unblocking

Research output: Working paper

Abstract

Rippling is a heuristic technique for guiding rewriting of a goal with
respect to one or more givens. Rewriting is restricted so that the similarities
between goal and given are preserved and the movement of differences is directed
and terminating. Unblocking is a technique for changing the differences to enable
a subsequent ripple.
The standard definition of rippling currently prevents certain, otherwise desirable,
unblocking steps. In particular, some desirable unblocking steps increase the well-founded measure on which the termination proof of rippling is based. We propose
an alternative family of well-founded measures under which the combination of
rippling and unblocking is terminating. These new measures extend the power of
rippling.
Original languageEnglish
Publication statusUnpublished - 1998

Publication series

NameDAI Research Paper 880

Fingerprint Dive into the research topics of 'The Termination of Rippling and Unblocking'. Together they form a unique fingerprint.

Cite this