Edinburgh Research Explorer

The Termination of Rippling and Unblocking

Research output: Working paper

Related Edinburgh Organisations

Documents

Original languageEnglish
StateUnpublished - 1998

Publication series

NameDAI Research Paper 880

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.

Download statistics

No data available

ID: 639686