The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

Research Paper #880

Title:The Termination of Rippling and Unblocking
Date:Jan 1998
Presented:submitted to CADE-15
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.

[Search These Pages] [DAI Home Page] [Comment]