Narrowing is a computation.
The environment of the computation is a rewrite system.
The subject of the computation is a term.
For example, a rewrite system that models the addition operation on natural numbers is:
add(zero,Y) -> Y add(succ(X),Y) -> succ(add(X,Y))Each line is a rewrite rule. The meaning should be intuitive. Identifiers add, zero, and succ are symbols, whereas X and Y are variables.A term, e.g., add(succ(zero),succ(zero)), is rewritten using the rewrites rules as follows:
add(succ(zero),succ(zero)) -> succ(add(zero,succ(zero))) -> succ(succ(zero))The first step makes use of the second rewrite rule where X stands for zero and Y stands for succ(zero). The second step makes use of the first rewrite rule.Narrowing generalizes rewriting by "guessing" instantiations of variables, if any, occurring in the term subject of the computation. Often, more than one guess is possible. For example, the term add(U,succ(zero)) is narrowed as follows:
add(U,succ(zero)) -> succ(add(V,succ(zero))) -> succ(succ(zero))The first step makes use of the second rewrite rule as before after guessing that variable U stands for succ(V), where V is a new variable. The second step makes use of the first rewrite rule as before after guessing that variable V stands for zero.Variables in the term subject of the computation represent unknown or incomplete information. Guessing instantiations of these variables without some purpose or guidance is in general meaningless.
Narrowing can be used to solve equations.
Continuing the previous example, narrowing the equation:add(U,succ(zero)) = succ(succ(zero))would determine that U=succ(zero) is a solution.Solving equations occasionally comes up when problems are coded into program. However, a much greater advantage is to use narrowing to ease design, development and maintenance of software.
For example, consider an abstraction such as that provided by the class String in the Java lang package. The abstraction contains groups of interdependent methods such as concat, to concatenate strings, and startsWith, lastChar, substring, etc. with the expected meaning. Coding all these methods is expensive. Maintaining the abstraction is also error prone. When a method in a group changes, other dependent methods in the group usually must change accordingly. However, since neither the groups of methods in a class nor the dependencies between these methods are explicit in the code, the potential for introducing errors is high.
Narrowing promotes a coding style where most dependent methods are either unnecessary or are code in a way unaffected by changes. For example:
startsWith(X,Y) -> concat(X,Z) = Ywhich reads as string Y starts with string X if there exists a string Z such that the concatenation of X and Z is equal to Y. Narrowing makes coding method startsWith a trivial task. Since the relation between startsWith and concat becomes explicit, changing the latter does not affect the former. For example, consider changing the representation of concatenated strings from a linear sequence of characters obtained by copying the arguments of concat in a new location to creating a pair containing the references to such arguments.Methods lastChar and substring are coded likewise:
lastChar(C, X) -> concat(Y,string(C)) = X substring(X,Y) -> concat(concat(U,X),V) = Ystring converts is argument, a character, to a string.
Narrowing in itself is a simple operation. Narrowing computations are executed step-wise until the term subject of a computation can no longer be narrowed. In general, many narrowing steps are possible in a term. The difficulty is in deciding which step(s) to execute.A narrowing step consists of a substitution, the guess of the values of some variables, and a reduction, the replacement of an instance of a rewrite rule left-hand side with the corresponding right-hand side.
Determining which steps are useful for a computation is the task of a strategy. Different strategies have been proposed for different classes of rewrite systems. Good strategies are sound, complete and efficient. These concepts are best understood when the term subject of a narrowing computation is an equation. Soundness means that narrowing computes only solutions of the equation. Completeness means that narrowing computes all the solutions of the equation. Efficiency is more elusive. It means that steps are not unnecessarily computed, where the notion of "necessary" step depends on the class of rewrite systems.
A narrowing strategy computes a set of narrowing steps of a term.A narrowing step of a term t is identified by a triple (p,l->r,s) where p is a position of t, l->r is a rewrite rule, and s is an idempotent substitution that unifies the subterm of t at p with l.
A narrowing step (p,l->r,s) of a term t is executed as follows. Every time a rule is used in a step, its variables are considered new. First, the substitution s is applied to the term t. The subterm of s(t) at position p is an instance of l, the left-hand side of the step's rewrite rule. Then, this subterm is replaced by the corresponding instance of r.
Continuing the previous example, a narrowing step of add(U,succ(zero)) is as follow. The position is empty, i.e., the subterm to replace is the entire term. The rule is add(succ(V),W)->succ(add(V,W). The substitution is {U=succ(V)}.
Narrowing steps are computed by a narrowing strategy. Different rewrite systems call for different strategies. However, the strategies that compute steps for many interesting subclasses of the constructor-based rewrite systems use definitional trees.A definitional tree is a hierarchical structure of the left-hand sides of the rewrite rules defining an operation. Definitional trees are used as finite state automata to compute narrowing steps. For example, the following operations compute the concatenation of two lists and the a prefix of a given length of a list. Natural numbers are in Peano notation and lists are in Prolog notation.
concat([],Z) -> Z concat([Y|Ys],Z) -> [Y|concat(Ys,Z)] take(zero,K) -> [] take(succ(N),[]) -> [] take(succ(N),[L|Ls]) -> [L|take(N,Ls)]The definitional tree of these operations are:take(M,K) concat(X,Z) / \ / \ / take(succ(N),K) / \ take(zero,K) / \ concat([],Z) concat([Y|Ys],Z) / \ take(succ(N),[]) take(succ(N),[L|Ls])The leaves of a tree are (variants) of the rewrite rules left-hand sides. The bold variable of a branch is called inductive variable.Suppose that the term t to narrow is take(V,concat([1],[2])) where V is an uninstantiated variable. Term t unifies with two maximal elements of the definitional tree of take, namely take(zero,K) and take(succ(N),K), with unifiers {V=zero} and {V=succ(N),K=concat([1],[2])}, respectively. The first element, take(zero,K), is a leaf, hence the substitution of the step is {V=zero} and the instantiated t is reduced to []. The second element, take(succ(N),[L|Ls]), is a branch, hence to compute a step of t it is necessary to compute a step of the subterm of t matching the inductive variable of the branch, namely concat([1],[2]). This step is computed using the definitional tree of operation concat and composing its substitution with {V=succ(N),K=concat([1],[2])}. The step of concat([1],[2]) has the identity substitution and [1|concat([],[2]) as reduct.