Chapter 16
Narrowing

16.1 Introduction

Narrowing is a generalization of term rewriting that allows free variables in terms (as in logic programming) and replaces pattern matching by unification in order to (non-deterministically) reduce these terms. Narrowing was originally introduced as a mechanism for solving equational unification problems [67]. It was later generalized to solve the more general problem of symbolic reachability [100]. The narrowing mechanism has a number of important applications, including automated proofs of termination [6], execution of functional-logic programming languages [71, 35, 74, 110, 92], partial evaluation [4], verification of cryptographic protocols [100], and equational unification [78], to mention just a few.

At each rewriting step one must choose which subterm of the subject term and which rule of the specification are going to be considered. Similarly, at each narrowing step one must choose which subterm of the subject term, which rule of the specification, and which instantiation on the variables of the subject term and the rule’s lefthand side are going to be considered. The narrowing relation is formally defined as follows. Let = (Σ,E ∪Ax,R) be an order-sorted rewrite theory where R is a set of unconditional rewrite rules specified with the rl keyword, E is a set of unconditional equations specified with the eq keyword, and Ax is a set of commonly occurring axioms declared in Maude as equational attributes (see Section 4.4.1) such that an E ∪ Ax-unification procedure is available in Maude.¹ Let CSU_E∪Ax(u = u′) provide² a finitary and complete set of unifiers for any pair of terms u,u′ with the same top sort. The R,E ∪Ax-narrowing relation on T_Σ(X) is defined as t_{σ,p,R,E∪Ax} t′ (or _σ when p,R,E ∪Ax are understood) if there is a non-variable position p of t, a (possibly renamed) rule l → r in R, and a unifier σ ∈ CSU_E∪Ax(t|_p = l) such that t′ = σ(t[r]_p). We denote by t ↝_σ,R,E∪Ax⁺t′ (resp. t ↝_σ,R,E∪Ax^*t′) the transitive (resp. reflexive-transitive) closure of the narrowing relation, where σ is obtained as the composition of the substitutions for each narrowing step in the sequence.

The difference between a rewriting step and a narrowing step is that in both cases we use a rewrite rule l → r to rewrite t at a position p in t, but narrowing unifies the lefthand side l and the chosen subject term t|_p before actually performing the rewriting step. Also, narrowing is usually³ restricted to non-variable positions of t, whereas rewriting does not require such a restriction.

Consider the following system module defining the addition function _+_ on natural numbers built from 0 and s:

Consider the term X + s(0) and the two rules base and ind. Narrowing will instantiate variable X with 0 and s(X’) respectively in order to be able to apply each of these rules, i.e., the following two narrowing steps are generated:

1.

X + s(0) ↝_{X0},base s(0)

2.

X + s(0)

↝{Xs(#1:Nat)},ind s(#1:Nat + s(0))

↝{#1:Nat0},base s(s(0))

3.

X + s(0)

↝{Xs(#1:Nat)},ind s(#1:Nat + s(0))

↝{#1:Nats(#2:Nat)},ind s(s(#2:Nat + s(0)))

↝{#2:Nat0},base s(s(s(0)))

and so on.

The following infinite narrowing derivation resulting from applying rule ind infinitely many times can also be shown:

16.1.1 Applications

The classical application of narrowing modulo an equational theory is to perform E ∪Ax-unification by ,Ax-narrowing when the equations E are oriented into sort-decreasing, confluent, terminating, and coherent modulo Ax rules . Indeed the variant-based equational order-sorted unification algorithm of Section 12.10 is based on an E,Ax-narrowing strategy, called folding variant narrowing [65], that terminates when E ∪ Ax has the finite variant property [32], even though full E,Ax-narrowing typically does not terminate when Ax contains AC axioms [32, 65].

Instead, when the rules R are understood as transition rules, a completely different application of R,E ∪ Ax-narrowing is that of symbolic reachability analysis [100] (see Section 12.6.2). Specifically, we will consider the case of transition systems specified by order-sorted rewrite theories of the form = (Σ,E ∪Ax,R) where: (i) E ∪Ax has a finite and complete E ∪Ax-unification algorithm (see the requirements of Section 12.9), and (ii) the transition rules R are E ∪ Ax-coherent and topmost (so that rewriting is always done at the top of the term). Then, narrowing is a complete deductive method [100] for symbolic reachability analysis, that is, for solving existential queries of the form ∃x t(x) →^*t′(x) in the sense that the formula holds for R iff there is a narrowing sequence t ↝_R,E∪Ax^*u such that u and t′ have an E ∪ Ax-unifier.

Furthermore, in symbolic reachability analysis we may be interested in verifying properties more general than existential questions of the form ∃X t-→^*t′. One can also generalize the above reachability question to questions of the form ,tφ, with φ a temporal logic formula. The papers [62, 7] show how narrowing can be used (again, both at the level of transitions with rules R and at the level of equations E) to perform logical model checking to verify such temporal logic formulas; this is a a kind of symbolic model checking not in the binary decision diagram sense of “symbolic,” which still remains finite-state, but in a much more general sense in which possibly infinite sets of states are finitely described by patterns with logical variables. Two distinctive features are: (i) the term t does not describe a single initial state, but a possibly infinite set of instances of t (i.e., a possibly infinite set of initial states); and (ii) the set of reachable states does not have to be finite. Therefore, standard model-checking techniques may not be usable, because of a possible double infinity: in the number of initial states, and in the number of states reachable for each of those initial states.

16.1.2 Completeness of narrowing

Due to nontermination, narrowing behaves as a semi-decision procedure for equational unification and for reachability analysis in a wide variety of theories. However, for some particular subject terms narrowing may terminate, providing a complete set of solutions. For instance, in the Maude module NAT-NARROWING above, narrowing computes the solution {Xs(Y)} for the reachability problem ∃X,Y 0 + X →^*s(Y) and it terminates with no more solutions. Instead, for the reachability problem ∃X,Z X + s(0) →^*s(s(Z)), narrowing computes the solution {Xs(0), Z0} but it cannot terminate because of the above infinite narrowing sequence using ind. Moreover, narrowing cannot prove that the reachability problem ∃X X + s(0) →^*0 does not have a solution, again because of the above infinite narrowing sequence using ind.

Note that for any narrowing sequence t ↝_σ,R,E∪Ax^*s, we have a corresponding rewrite sequence σ(t) →_R,E∪Ax^*s. However, only under appropriate conditions is narrowing complete as an equational unification algorithm [78, 79], or as a procedure to solve reachability problems [100]. That is, given a reachability problem⁴ ∃X₁,…,X_k s →^*t completeness means that for each possible substitution ρ that binds some variables of X₁,…,X_k in such a way that ρ(s) →_R,E∪Ax^*ρ(t), and for all the substitutions σ₁,…,σ_n,… provided by narrowing from s, there is an index i and two substitutions θ,τ such that ρ(s) →_R,E∪Ax^*θ(s), ρ(t) →_R,E∪Ax^*θ(t), θ(s) →_R,E∪Ax^*θ(t), and θ = _E∪Axσ_i;τ, where σ_i;τ denotes substitution composition in diagrammatic order, i.e., (σ_i;τ)(X) = τ(σ_i(X)). Essentially, completeness holds either

1.

for (R,E ∪ Ax)-normalized substitutions ρ above [100] (a stronger condition is (R ∪ E,Ax)-normalized substitutions);

2.

for topmost rewrite theories⁵ ;

3.

for right-linear theories and linear reachability goals⁶ ; and

4.

in particular for theories that are confluent, terminating, and coherent modulo axioms Ax, as the equational theories in Maude functional modules with such properties restricted to unconditional equations.

16.1.3 Narrowing with simplification

We have implemented a version of narrowing with simplification, which is slightly different from the one formally defined above. Let = (Σ,G ∪ E ∪ Ax,R) be an order-sorted rewrite theory where R, E, and Ax are defined as above and G are the remaining equations. Note that when an equational theory (Σ,G ∪ E ∪ Ax,R) is provided to Full Maude, each equation in E (used for variant computation) must include the variant attribute. Note that equations in G do not contain the variant attribute and do not have any restriction, i.e., they can be conditional equations, with the owise attribute, etc. Each narrowing step of the form t_{σ,p,R,E∪Ax} t′ is followed by simplification using the relation →_G∪E,Ax^!, i.e., the combined relation (_{σ,p,R,E∪Ax};→_G∪E,Ax^!) is defined as t_{σ,p,R,E∪Ax};→_G∪E,Ax^!t′′ iff t_{σ,p,R,E∪Ax} t′, t′→_G∪E,Ax^*t′′, and t′′ is G ∪ E,Ax-irreducible. Note that this combined relation (_{σ,p,R,E∪Ax};→_G∪E,Ax^!) may be incomplete, i.e., given a reachability problem of the form t →^*t′ and a solution σ (i.e., σ(t) →_R,G∪E∪Ax^*σ(t′)), the relation _{σ,p,R,E∪Ax};→_G∪E,Ax^! may not be able to find a more general solution. The reason is that the equations G should also be executed by narrowing instead of rewriting to ensure completeness under appropriate conditions (see [100] and Section 16.1.2). However, the combination of narrowing using rules, equations, and axioms with simplification using additional equations can be quite helpful to allow built-in Maude functions such as addition or multiplication, which cannot be executed by narrowing in their predefined form. It can also be useful in other applications where specific combinations of narrowing and simplification are needed.

16.2 Theories supported for narrowing reachability

The narrowing relation is defined on top of the order-sorted variant-based unification procedure described in Section 12.10.

Let mod (Σ,G ∪ E ∪ Ax,R) endm be an order-sorted system module where R is a set of rewrite rules specified with the rl or crl keywords, Ax is a set of commonly occurring axioms (declared in Maude as equational attributes, see Section 4.4.1), E is a set of equations specified with the eq keyword and the attribute variant such that (Σ,E ∪ Ax) satisfies the restrictions mentioned in Section 12.10, and G are the remaining equations specified with the eq or ceq keywords. Furthermore, the rules R must satisfy the following extra conditions:

• Conditional rules specified with the crl keyword are not taken into account, i.e., there may be conditional rewrite rules in the system module but they will not be used for narrowing.
• A rule’s lefthand side cannot be a variable. If a variable is needed, one should instead specify a new kind with an extra unary symbol grabbing the whole system’s state (which would before have been matched by a single variable lefthand side). In this way, the problem of having a variable lefthand side can often be solved.
• The rules must be explicitly Ax-coherent (see Section 5.3). Moreover, Ax-coherence of equations and rules is enforced automatically by calling the coherence completion algorithm of Section 15.5. If the rules are already Ax-coherent, no extra rules will be added.

We recall again that the equations G in the system module are disregarded for narrowing purposes. However, they are applied for simplification after each narrowing step (see Section 16.1.3), as it is performed in Maude for rewriting. Recall, again, that this combination of one narrowing step followed by equational simplification is not complete. A full treatment of rules, equations, and axioms for narrowing is outside the scope of the present implementation and is left for future work.

Furthermore, frozen arguments (see Section 4.4.9) are allowed for narrowing, as for rewriting. They are given the standard meaning of not allowing any narrowing step below such frozen arguments, just as in the context-sensitive narrowing of [83].

Finally, we do not consider any narrowing strategy at all for solving reachability problems, i.e., all positions in a term with an admissible R,E ∪ Ax-narrowing step are explored.

16.3 The narrowing search command

Given a system module ⟨ModId⟩, the user can give to Full Maude a search command of the form:

  (search  [  ] in ⟨ModId⟩ : ⟨Term-1⟩ ⟨SearchArrow⟩ ⟨Term-2⟩ .)

where:

• n is an optional argument providing a bound on the number of desired solutions;
• m is another optional argument stating the maximum depth of the search;
• the system module ⟨ModId⟩ where the search takes place can be omitted if it is the current one;
• ⟨Term-1⟩ is the starting non-variable term, which may contain variables;
• ⟨Term-2⟩ is the term specifying the pattern that has to be reached, with variables possibly shared with ⟨Term-1⟩;
• ⟨SearchArrow⟩ is an arrow indicating the form of the narrowing proof from ⟨Term-1⟩ until ⟨Term-2⟩:
  • ~>1 means a narrowing proof consisting of exactly one step,
  • ~>+ means a narrowing proof consisting of one or more steps,
  • ~>* means a narrowing proof consisting of none, one, or more steps, and
  • ~>! indicates that only strongly irreducible final states are allowed, i.e., states that cannot be further narrowed; note that this is stronger than requiring states that cannot be rewritten.

  The one step arrow ~>1 is an abbreviation for the one-or-more steps arrow ~>+ with the depth bound m set to 1.

Consider, for example, the following new version of the vending machine to buy apples (a) or cakes (c) with dollars ($) and/or quarters (q). The reader can check that the only difference with the VARIANT-VENDING-MACHINE module in Section 12.9.2 is the change equation, which is ACU-coherent in the former version but it is not in this new version, because it is made ACU-coherent internally.

We can use the narrowing search command to answer the question:

This can be done by searching for states that are reachable from a term < M:Money > and match the desired pattern at the end.

Note that __ is an ACU symbol and that such an ACU symbol appears in the equation change, disallowing the basic narrowing strategy [78] to be used for equational unification and requiring the folding variant narrowing [65] to be used for equational unification.

Note that we have restricted the previous reachability problem to just one solution. Narrowing does not terminate for this reachability problem even though the above solution is indeed the only solution. The problem is that narrowing follows a breadth-first exploration and does not stop until the whole narrowing tree demanded by the search command is created, even though this infinite search may not yield any further solutions. The very same problem happens for the standard search command (see Section 5.4.3). If we increase the depth of the narrowing tree, we can experimentally observe that no more solutions are found.

As with the search command of Full Maude (see Section 15.6), the narrowing version does not provide paths to solutions but there is a metalevel command that does provide paths, described in Section 16.3.2.

In the previous reachability problem, we can change the arrow ~>* for reachability in zero or more steps by the arrow ~>! for reachability in zero or more steps including only states that cannot be narrowed any more.

And surprisingly we do not find the previous solution. The reason is that the transition rules of the vending machine are not terminating for narrowing and for rewriting, so it is impossible to find a state that cannot be narrowed any more. However, if we replace the variable M:Money by variables of sort Coin, we are able to find appropriate solutions. That is, we formulate the following interesting question:

The fact that some money is left is characterized by including a variable of sort Money in the final state, and the fact that nothing else can be bought is characterized by using the ~>! arrow instead of ~>*.

Another point of interest is the occurrence of variables of the form #n:Sort or %n:Sort, which are called fresh and are described in Chapter 12. Unification modulo axioms usually introduces fresh variables; furthermore, narrowing introduces many fresh variables because the rule applied at each narrowing step is appropriately renamed so that no variable is shared by it and the current term. Indeed, the standard solution used in logic and functional-logic programming language implementations is to use a counter along each narrowing derivation to ensure that fresh variables have never been used previously in that narrowing derivation. This method is called standardized apart.

16.3.1 Narrowing with extra variables in righthand sides of rules

Although rewriting does not allow extra variables in the righthand side of rules⁷ , extra variables in righthand sides pose no problem for narrowing. Since rules having extra variables in the righthand side are not allowed in Maude for rewriting purposes, the attribute nonexec (see Section 4.5.3) must be added to such rules if one wants to use them for narrowing. The nonexec attribute is not taken into account by narrowing: all unconditional rules, regardless of whether or not they include the nonexec attribute, are used by narrowing. Extra variables in the righthand side are a common feature of programs using narrowing as the operational evaluation mechanism, as in logic programming or functional-logic programming [74]. For further details on how to write funcional-logic programs in Maude using symbolic reachability, see [58]. Let us motivate this feature with an example. Consider the following program defining the concatenation of two lists and the function last:

In the rule

we have used an extra variable N to denote the last element of the list and used a constraint

that narrowing will solve by instantiating N in the proper way. Furthermore, note the use of kinds and the sort Success in order to describe what a successful solution is; this follows a logic programming approach (as in Prolog) to success and failure, see [58]. The following reachability problem is solved by narrowing but cannot be solved by rewriting due to the extra variable in the last rule.⁸

Another interesting example of narrowing with extra variables is the function member:

The following reachability problem is solved by narrowing but cannot be solved by rewriting due to the extra variable in the rule defining the member function.

But the interesting application is to enumerate all the elements of a list by computing different substitutions, as in logic programming.

Note that we have to restrict the depth of the narrowing tree to five because there exists an infinite number of narrowing sequences from the term member(N:Nat,0 : s(0): nil) even if only two solutions exist.

16.3.2 Reachability at the metalevel: metaNarrowSearch and
metaNarrowSearchPath

Narrowing-based reachability analysis is also available at the metalevel by using the function metaNarrowSearch, provided in the META-NARROWING-SEARCH module with the following declaration:

Recall that the sort ResultTriple contains triples formed by a term, its type, and a substitution:

The sort ResultTripleSet contains sets of such result triples and is defined as follows:

If a non-identity substitution is provided in the fourth argument of metaNarrowSearch, then any computed substitution must be an instance of the provided one, i.e., we can restrict the computed narrowing sequences to some concrete shape. The Qid argument metarepresents the appropriate search arrow, similar to the metaSearch command (see Section 11.5.6). For the bounds, the first one is the maximum length of the narrowing sequences, the second one is the number of computed solutions, i.e., the depth of the narrowing tree, and the third one is the chosen solution (in order to provide all solutions in a sequential way, as many metalevel commands in Maude do).

For the NARROWING-VENDING-MACHINE system module introduced at the beginning of Section 16.3, the following search command considered above

can be specified at the metalevel as follows, where ’<_>[’M:Money] is the metarepresentation of the state < M:Money >, ’<_>[’__[’a.Item,’c.Item]] is the metarepresentation of the state < a c >, and we use the coherence completion of the NARROWING-VENDING-MACHINE module given above.

Note that we obtain the very same solution, where the output contains one term of type ResultTriple, which contains the actual output term, its type, and the computed substitution, and

is the metarepresentation of the substitution M:Money --> $ q q q. Moreover, the substitutions computed in this way also contain all the temporary bindings that narrowing has computed.

Moreover, we can also obtain the narrowing sequence associated to a narrowing-based reachability command with the function metaNarrowSearchPath provided in the same module META-NARROWING-SEARCH with the following declaration:

It works in exactly the same way as metaNarrowSearch but providing as a result a more detailed data structure. If we redo the previous metaNarrowSearch computation but using this time the metaNarrowSearchPath function, we obtain:

The data structure TraceNarrow, which is the basic element of TraceNarrowSet, is very similar to the data structure ResultTriple but it contains a sequence of narrowing results instead of only the final result, each one together with the rule that has been used in that narrowing step.

16.3.3 Paramodulation

The difference between a rewriting step and a narrowing step is that in both cases we use a rewrite rule l → r to rewrite t at a position p in t, but narrowing unifies the lefthand side l and the chosen subject term t|_p before actually performing the rewriting step. Rewriting does not impose any restriction on the chosen subterm t|_p nor the lefthand side l but narrowing imposes that both cannot be a variable, i.e.:

• the chosen subterm t|_p of a narrowing step cannot be a variable, and
• the lefthand side l cannot be a variable.

However, there are interesting cases where these two restrictions are not desirable, for example the paramodulation inference rule used in paramodulation-based theorem proving [101] does not require them (see [118] for an example of use of this paramodulation feature for theorem proving).

The function metaParamodulationSearch provides an extension at the metalevel of the narrowing-based search command without these two restrictions. It is declared again in the same module META-NARROWING-SEARCH and has the same parameters as metaNarrowSearch:

Let us consider yet another version of the NARROWING-VENDING-MACHINE system module where we do not use the symbol <_> for restricting rewriting:

Then we can perform the following search command that provides a variable as the starting term, without using the <_> symbol anymore:

Note that we obtain the same solution that we computed by means of metaNarrowSearch.