Division of Informatics
Forrest Hill & 80 South Bridge
Research Paper #880 | |
|---|---|
| Title: | The Termination of Rippling and Unblocking |
| Authors: | Bundy,A |
| Date: | Jan 1998 |
| Presented: | submitted to CADE-15 |
| Keywords: | |
| 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: | POSTSCRIPT COPY |
![[Search These Pages]](http://www.dai.ed.ac.uk/icons/dai_search.gif){kind=icon}
![[DAI Home Page]](http://www.dai.ed.ac.uk/icons/dai_home.gif){kind=icon}
![[Comment]](http://www.dai.ed.ac.uk/icons/dai_comment.gif){kind=icon}