An overview and a systematization of the main results of optimized narrowing strategies are presented in this paper, which also corrects some imprecise claims made in the literature on this topic. The paper also demonstrates how to translate a very general class of term rewriting systems (left-linear and constructor-based conditional rewriting systems) into overlapping inductively sequential ones, a format suitable for the application of an optimized narrowing strategy (inductively sequential narrowing, INS), which was developed by the author in previous work.
The transformation is sound and complete, with regard to the evaluation semantics of the original program. Since INS is a complete operational principle for the target class of programs, the combination of both results formalizes the first correct operational semantics for the wide class of left-linear constructor-based conditional term rewriting systems.
The novel contribution of this paper is not particularly technically difficult, since the method essentially combines a number of traditional transformations. For instance, the ideas of left-linearization and deconditionalization were already present in the initial reports of Babel, Curry, and so on. Nevertheless, the paper fills a gap in the literature, and its relevance is high. Indeed, INS is (essentially) the operational basis of modern functional-logic languages, and subsumes the most popular needed narrowing strategy, which is complete only for the smaller subclass of inductively sequential programs (although it enjoys stronger optimality properties).
The paper is accurate and easy to read, even if it is not completely self-contained: due to space restrictions, the definitions of some key notions are not recalled, thus a reader unfamiliar with the topic will get a sense of the state of the art, but might not be able to grasp things in depth.