Abstract / Description of output
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.
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 language | English |
|---|---|
| Publication status | Unpublished - 1998 |
Publication series
| Name | DAI Research Paper 880 |
|---|