Directed Narrowing: An Optimization That More Often Terminates

We present a refinement of the narrowing directed by a graph of terms, which is complete for confluent and terminating rewrite systems, and show that it terminates more often than basic narrowing and lazy narrowing. Then, we give a second refinement by adding LSE narrowing tests in directed narrowing, which is complete under the same conditions. We show that it terminates more often than LSE narrowing and that it is minimal, i.e. no solution is computed twice. Contents 1 Introduction 3 2 Preliminaries 4 3 The graph of terms 6 3.1 The construction of the graph : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 6 3.1.1 Examples : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 6 3.1.2 The algorithm : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 7 3.2 Properties of the graph of terms : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 8 4 The directed narrowing 11 4.1 The procedure : : : : : : : : : : : : : : ..