Natural Narrowing as a General Unified Mechanism for Programming and Proving

Although originally introduced as a theorem proving method to solve equational unification problems, narrowing was soon recognized as a key mechanism to unify functional and logic programming. In fact, in a declarative setting where programming and proving can be seamlessly integrated, narrowing serves as a unified mechanism for both evaluation and deduction. For narrowing to be an efficient evaluation mechanism, several lazy narrowing strategies have been proposed, although typically for the restricted case of left-linear constructor-based rewrite systems. These assumptions, while reasonable for functional programming applications, are too restrictive for a much broader range of applications to which narrowing can be fruitfully applied. In this paper, we propose an efficient lazy narrowing strategy called natural narrowing which can be applied to a larger class of rewrite systems without the above assumptions. This strategy is more efficient than all previously know strategies when applied to the class of left-linear constructor-based rewrite systems. An important consequence of this generalization is the wide range of applications that can now be efficiently supported by narrowing. We highlight a few such applications including symbolic model checking, theorem proving, and partial evaluation. What thus emerges is a general and efficient unified mechanism based on narrowing, that seamlessly integrates a very wide range of applications in programming and proving