Basic Narrowing Revisited

Abstract

In this paper we study basic narrowing as a method for solving equations in the initial algebra specified by a ground confluent and terminating term rewriting system. Since we are interested in equation solving, we don’t study basic narrowing as a reduction relation on terms but consider immediately its reformulation as an equation solving rule. This reformulation leads to a technically simpler presentation and reveals that the essence of basic narrowing can be captured without recourse to term unification. We present an equation solving calculus that features three classes of rules. Resolution rules, whose application is don’t care nondeterministic, are the basic rules and suffice for a complete solution procedure. Failure rules detect inconsistent parts of the search space. Simplification rules, whose application is don’t care nondeterministic, enhance the power of the failure rules and reduce the number of necessary don’t know steps. Three of the presented simplification rules are new. The rewriting rule allows for don’t care nondeterministic rewriting and thus yields a marriage of basic and normalizing narrowing. The safe blocking rule is specific to basic narrowing and is particulary useful in conjunction with the rewriting rule. Finally, the unfolding rule allows for a variety of search strategies that reduce the number of don’t know alternatives that need to be explored.