Implementing Natural Rewriting and Narrowing Efficiently

Abstract

Outermost-needed rewriting/narrowing is a sound and complete optimal demand-driven strategy for the class of inductively sequential constructor systems. Its parallel extension, known as weakly, deals with non-inductively sequential constructor systems. Recently, refinements of (weakly) outermost-needed rewriting and narrowing have been obtained. These new strategies are called natural rewriting and natural narrowing, respectively, and incorporate a better treatment of demandedness. In this paper, we address the problem of how to implement natural rewriting and narrowing efficiently by using a refinement of the notion of definitional tree, which we call matching definitional tree. We also show how to compile natural rewriting and narrowing to Prolog and provide some promising experimental results. © Springer-Verlag 2004.