## Chapter 15Narrowing

### 15.1Introduction

Narrowing is a generalization of term rewriting that allows logical variables in terms (as in logic programming) and replaces pattern matching by unification in order to symbolically evaluate these terms with given rewrite rules. Narrowing is a simple, precise answer to the question:

Given a term t with variables x1,,xn, what are the most general instances of t that can be rewritten by the given rules?

For example, t can be n + m, and the rewrite rules can be 0 + y y and s(x) + y s(x + y). The term n + m cannot be rewritten because of the variable n and finding the most general instances becomes interesting; note that if + is commutative, then either n or m stop t from being rewritten.

Narrowing was originally introduced as a mechanism for solving equational unification problems . It was later generalized to solve the more general problem of symbolic reachability . The narrowing mechanism has a number of important applications, including automated proofs of termination , execution of functional-logic programming languages , partial evaluation , verification of cryptographic protocols , and equational unification , 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.1 Let CSUEAx(u = u) provide2 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,EAx 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 σ CSUEAx(t|p = l) such that t = σ(t[r]p). We denote by t σ,R,EAx+t (resp. t σ,R,EAxt) 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 usually3 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:

``` mod NAT-NARROWING is  sort Nat .  op 0 : -> Nat [ctor] .  op s : Nat -> Nat [ctor] .  op _+_ : Nat Nat -> Nat .  vars X Y : Nat .  rl [base] : 0 + Y => Y .  rl [ind] : s(X) + Y => s(X + Y) . endm
```

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: Note that, for simplicity, we show only the bindings of the unifier that affect the input term. There are infinitely many narrowing derivations starting at the input expression X + s(0) (at each step the reduced subterm is underlined):
1.
X + s(0) {X 0},bases(0)
2.
X + s(0)
 ↝{X s(#1:Nat)},inds(#1:Nat + s(0)) ↝{#1:Nat 0},bases(s(0))
3.
X + s(0)
 ↝{X s(#1:Nat)},inds(#1:Nat + s(0)) ↝{#1:Nat s(#2:Nat)},inds(s(#2:Nat + s(0))) ↝{#2:Nat 0},bases(s(s(0)))

and so on.

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

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

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  (see Section 13.5.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 14.1), 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  for symbolic reachability analysis, that is, for solving existential queries of the form xt(x) t(x) in the sense that the formula holds for iff there is a narrowing sequence t R,EAxu 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 Xtt. One can also generalize the above reachability question to questions of the form ,t φ, with φ a temporal logic formula. The papers  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 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 states4 ); 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 from each of those initial states.

### 15.3Completeness 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 {X s(Y)} for the reachability problem X,Y0 + X s(Y) and it terminates with no more solutions. Instead, for the reachability problem X,ZX + s(0) s(s(Z)), narrowing computes the solution {X s(0), Z 0} but it cannot terminate because of the above infinite narrowing sequence using ind. Moreover, narrowing cannot prove that the reachability problem XX + 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,EAxs, we have a corresponding rewrite sequence σ(t) R∕EAxs, where, by definition, the rewrite relation R∕EAx is the relation composition: R∕EAx = def (= EAx);R;(= EAx), i.e., the transition relation between states in the given rewrite theory = (Σ,E Ax,R). However, only under appropriate conditions is narrowing complete as an equational unification algorithm , or as a procedure to solve reachability problems . That is, given a reachability problem5 x1,,xk : s t, completeness of narrowing for reachability analysis means that for each possible substitution ρ such that ρ(s) R∕EAxρ(t), and for all the substitutions σ1,n,, provided by narrowing from s, there is an index i and a term ui such that, if s σ1,R,EAxu1 ui1 σi,R,EAxui, then there is a E Ax-unifier τ of the equation ui = t, and therefore there is a rewrite sequence τ(σ(s)) R∕EAxτ(ui), showing that a instance of s reaches an instance of t modulo the equations E Ax. Essentially, completeness holds under the following conditions:

1.
for (R,E Ax)-normalized substitutions ρ above  (a stronger condition is (R E,Ax)-normalized substitutions);
2.
for topmost rewrite theories6 ;
3.
for right-linear theories and linear reachability goals7 ;
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.

### 15.4Narrowing with simplification

As pointed out in Footnote 1, given a rewrite theory = (Σ,E G Ax,R), where Ax are the axioms, and E G the equations orientable as rewrite rules, if only the equations E have the variant attribute, Maude will not perform narrowing with R modulo E G Ax, but only modulo E Ax. This gives Maude users more flexibility, since the equations G may play a useful, auxiliary role in the applications they have in mind. In particular, a concrete, practical reason for using the decomposition E G is that E Ax may be FVP, but G may not be, so that variant E Ax-unification is finitary, whereas variant E G Ax-unification will be infinitary and undecidable. Note that the standard case of narrowing with R modulo E G Ax is just the special case G = , which may be particularly attractive if E Ax is FVP. The basic intuition is that, in the most general version of narrowing supported by Maude that we now explain, we narrow with R modulo E Ax, and we normalize with oriented equations E G modulo Ax.

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,EAx t is followed by simplification using the relation GE,Ax!, i.e., the combined relation ( σ,p,R,EAx;GE,Ax!) is defined as t σ,p,R,EAx;GE,Ax!t′′ iff t σ,p,R,EAx t, t′→GE,Axt′′, and t′′ is G E,Ax-irreducible. Note that this combined relation ( σ,p,R,EAx;GE,Ax!) may be incomplete, i.e., given a reachability problem of the form t t and a solution σ (i.e., σ(t) R,GEAxσ(t)), the relation σ,p,R,EAx;GE,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  and Section 15.3). 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.

### 15.5Theories supported for narrowing reachability

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

Let mod,GE Ax,RH) endm be an order-sorted system module where R is a set of rewrite rules specified with the rl keyword and the attribute narrowing, H are the remaining rewrite rules specified with the rl or crl keywords but without the attribute narrowing, 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 14.7, and G are the remaining equations specified with the eq or ceq keywords but without the attribute variant. Furthermore, the rules R must satisfy the following extra conditions:

• R cannot contain conditional rules specified with the crl keyword.
• The lefthand side of a rule in R 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 in R must be explicitly Ax-coherent (see Section 5.3). If they are not, the coherence completion algorithm of Section 21.5 should be used.

We recall again that the rules H are disregarded for narrowing modulo E Ax, and the oriented equations G are disregarded for folding variant narrowing modulo Ax in the associated task of variant unification. However, the equations G are applied for simplification after each narrowing step (see Section 15.4), 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 .

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.

### 15.6The vu-narrow command

Given a system module ModId, the user can give to Maude a narrowing-based search command of the form (the prefix vu denotes that uses variant-based unification at each step):

``` vu-narrow [ n, m ] 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 module ModId where the search takes place can be omitted;
• Term-1 is the starting term, which typically will contain variables;
• Term-2 is the pattern that has to be reached, which may share variables with the starting term (note that terms in the narrowing sequence will be unified with this target pattern, in contrast to the search command of Section 5.4.3);
• SearchArrow is an arrow indicating the form of the rewriting proof from Term-1 until Term-2:
• =>1 means a rewriting proof consisting of exactly one step,
• =>+ means a rewriting proof consisting of one or more steps,
• =>* means a proof consisting of none, one, or more steps, and
• =>! indicates that only narrowing sequences ending in terms describing sets of final states are allowed. Such terms describing sets of final states are called strongly irreducible in the sense that they cannot be further narrowed; note that this is stronger than requiring states that cannot be rewritten as in the search command of Section 5.4.3.

The one step arrow =>1 is an abbreviation of 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 14.3 is the addition of the narrowing attribute to the rules.

``` mod NARROWING-VENDING-MACHINE is  sorts Coin Item Marking Money State .  subsort Coin < Money .  op empty : -> Money .  op __ : Money Money -> Money [assoc comm id: empty] .  subsort Money Item < Marking .  op __ : Marking Marking -> Marking [assoc comm id: empty] .  op <_> : Marking -> State .  ops \$ q : -> Coin .  ops a c : -> Item .  var M : Marking .  rl [buy-c] : < M \$ > => < M c > [narrowing] .  rl [buy-a] : < M \$ > => < M a q > [narrowing] .  eq [change] : q q q q M = \$ M [variant] . endm
```

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

Is there any combination of one or more coins that returns exactly an apple and a cake?

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

``` Maude> vu-narrow  in NARROWING-VENDING-MACHINE : < M:Money > =>* < a c > .  Solution 1 state: < a c #1:Money > accumulated substitution: M:Money --> \$ q q q #1:Money variant unifier: #1:Money --> empty
```

The narrowing-based search returns the substitution accumulated along the narrowing sequence and the variant unifier resulting from the unification of the target term and the last expression in the narrowing sequence. Indeed both unifiers must be combined by hand in order to have an actual solution to the symbolic reachability problem, as shown for the previous example.

``` Solution 1 state: < a c > accumulated substitution: M:Money --> \$ q q q
```

Note that __ is an ACU symbol and that such an ACU symbol appears in the equation change, disallowing the basic narrowing strategy  to be used for equational unification and requiring the folding variant narrowing  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 there are no more solutions than the one shown before.

``` Maude> vu-narrow [,5] in NARROWING-VENDING-MACHINE : < M:Money > =>* < a c > .  Solution 1 state: < a c #1:Money > accumulated substitution: M:Money --> \$ q q q #1:Money variant unifier: #1:Money --> empty
```

The narrowing-based search version does not provide paths to solutions but there is a metalevel command, described in Section 17.6.11, that does provide paths.

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.

``` Maude> vu-narrow [,5] in NARROWING-VENDING-MACHINE : < M:Money > =>! < a c > .  No solution.
```

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:

Is there any combination of four coins that returns an apple and a cake and is such that some extra money is left but that extra money cannot be used to buy anything else?

The fact that some money may be 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 =>*.

``` vu-narrow [,10] in NARROWING-VENDING-MACHINE :   < C1:Coin C2:Coin C3:Coin C4:Coin > =>! < M:Money a c > .  Solution 1 state: < a c > accumulated substitution: C1:Coin --> q C2:Coin --> q C3:Coin --> q C4:Coin --> \$ variant unifier: M:Money --> empty  Solution 2 state: < a c > accumulated substitution: C1:Coin --> q C2:Coin --> q C3:Coin --> \$ C4:Coin --> q variant unifier: M:Money --> empty  Solution 3 state: < a c > accumulated substitution: C1:Coin --> q C2:Coin --> \$ C3:Coin --> q C4:Coin --> q variant unifier: M:Money --> empty  Solution 4 state: < a c > accumulated substitution: C1:Coin --> \$ C2:Coin --> q C3:Coin --> q C4:Coin --> q variant unifier: M:Money --> empty  No more solutions.
```

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 13. 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  and it is summarized by saying that a new version of a rule, equation or axiom is always generated before being used for unification or narrowing by renaming variables according to the counter, which is incremented afterwards. This method makes the result of a computation independent of the choice of variable names.

### 15.7The fvu-narrow command

We have motivated in the previous sections how narrowing can be used for symbolic reachability analysis  using the vu-narrow command. However, narrowing builds a reachability tree rather than a reachability graph, as the search command of Section 5.4.3 does for rewriting with rules. We have endowed Maude with a different narrowing command, the fvu-narrow command, that does fold some branches of the narrowing reachability tree in order to create a graph, with the difference that the search command identifies states in the rewriting-based reachability tree that are equal modulo axioms whereas the fvu-narrow command identifies states in the narrowing-based reachability tree that are equal modulo axioms under instantiation8 . This is similar in nature to the folding variant narrowing strategy  of the variant generation command of Chapter 14 but using rules instead of equations. Indeed, the logical model checking of  is based on earlier versions of this fvu-narrow command.

Given a system module ModId, the user now can give to Maude a folding narrowing-based search command of the form (the prefix f denotes folding):

``` fvu-narrow [ n, m ] 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 module ModId where the search takes place can be omitted;
• Term-1 is the starting term, which typically will contain variables;
• Term-2 is the pattern that has to be reached, which may share variables with the starting term;
• SearchArrow is an arrow indicating the form of the rewriting proof from Term-1 until Term-2:
• =>1 means a rewriting proof consisting of exactly one step,
• =>+ means a rewriting proof consisting of one or more steps,
• =>* means a proof consisting of none, one, or more steps, and
• =>! indicates that only terms describing sets of canonical final states are allowed (see Section 15.6).

Consider again the NARROWING-VENDING-MACHINE module and the following question, both in Section 15.6.

Is there any combination of one or more coins that returns exactly an apple and a cake?

We can repeat, with the same result, the vu-narrow command but now with the f at the beginning.

``` Maude> fvu-narrow  in NARROWING-VENDING-MACHINE : < M:Money > =>* < a c > .  Solution 1 state: < a c #1:Money > accumulated substitution: M:Money --> \$ q q q #1:Money variant unifier: #1:Money --> empty
```

However, producing a reachability graph instead of a reachability tree may improve the chances of having a finite search space. If we repeat the same command but without asking for the first solution, Maude reports the unique solution but gets into a loop, since the fvu-narrow command cannot produce a finite search graph. However, the reason is that we are giving a logical variable of sort Money and any new state containing an apple or a cake cannot be an instance of the initial state. Therefore, we can use a variable of sort Marking instead of Money and the infinite narrowing-based reachability tree is folded into a finite narrowing-based reachability graph.

``` Maude> fvu-narrow in NARROWING-VENDING-MACHINE : < M:Marking > =>* < a c > .  Solution 1 state: < #1:Marking > accumulated substitution: M:Marking --> #1:Marking variant unifier: #1:Marking --> a c  No more solutions.
```

But this is not the expected solution, since it is simply instantiating variable M:Marking to the apple and the cake. The graph is finite, as we wanted, but there is only one state, the initial one, and every other state is folded into it, since they are obviously instances of it.

What is actually happening is that this specification of the vending machine is not well suited for taking advantage of this folding narrowing technique. Consider the following new version of the vending machine. The reader can check that the only difference with the NARROWING-VENDING-MACHINE module in Section 15.6 is that apples and cakes are not deposited in the bag but consumed.

``` mod FOLDING-NARROWING-VENDING-MACHINE is  sorts Coin Item Marking Money State .  subsort Coin < Money .  op empty : -> Money .  op __ : Money Money -> Money [assoc comm id: empty] .  subsort Money Item < Marking .  op __ : Marking Marking -> Marking [assoc comm id: empty] .  op <_> : Marking -> State .  ops \$ q : -> Coin .  ops a c : -> Item .  var M : Marking .  rl [buy-c] : < M \$ c > => < M > [narrowing] .  rl [buy-a] : < M \$ a > => < M q > [narrowing] .  eq [change] : q q q q M = \$ M [variant] . endm
```

We can repeat the same command and now we get the expected result while having a finite narrowing-based reachability graph.

``` Maude> fvu-narrow in FOLDING-NARROWING-VENDING-MACHINE : < M:Marking a c > =>* < empty > .  Solution 1 state: < #1:Marking > accumulated substitution: M:Marking --> \$ q q q #1:Marking variant unifier: #1:Marking --> empty  No more solutions.
```

The graph is finite, as we wanted, since, after two narrowing steps, a state of the form < #1:Marking > is generated and, therefore, any other further state is folded into it. Note that a similar vu-narrow command does not stop. Note also that if we use a variable of sort Money, then the narrowing-based reachability tree is finite, since no more coins can be introduced, and both the vu-narrow and fvu-narrow commands stop.

``` Maude> vu-narrow in FOLDING-NARROWING-VENDING-MACHINE : < M:Money a c > =>* < empty > .  Solution 1 state: < #1:Money > accumulated substitution: M:Money --> \$ q q q #1:Money variant unifier: #1:Money --> empty  No more solutions.
```

### 15.8Narrowing with extra variables in righthand sides of rules

Although rewriting does not allow extra variables in the righthand side of rules9 , 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 with the narrowing attribute, 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 . For further details on how to write funcional-logic programs in Maude using symbolic reachability, see . Let us motivate this feature with an example. Consider the following program defining the concatenation of two lists and the function last:

``` mod LAST-APPEND is  sort Success .  op success : -> Success .  sort Nat .  op 0 : -> Nat .  op s : Nat -> Nat .  sort NatList .  op nil : -> NatList .  op _:_ : Nat NatList -> NatList .   vars XS YS : NatList .  vars N M X Y : Nat .   op append : NatList NatList -> [NatList] .  rl append(nil, YS) => YS [narrowing] .  rl append(N : XS, YS) => N : append(XS, YS) [narrowing] .   op last : NatList -> [Nat] .  rl last(XS) => append(YS, N : nil) =:= XS >> N [nonexec narrowing] .   op _>>_ : [Success] [Nat] -> [Nat] [frozen (2) strat (1 0)] .  eq success >> X:[Nat] = X:[Nat] .   op _=:=_ : Nat Nat -> [Success] [comm] .  rl N =:= N => success [narrowing] .   op _=:=_ : NatList NatList -> [Success] [comm] .  rl XS =:= XS => success [narrowing] . endm
```

In the rule

```  rl last(XS) => append(YS, N : nil) =:= XS >> N [nonexec narrowing] .
```

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

``` append(YS, N : nil) =:= XS
```

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 . The following reachability problem is solved by narrowing but cannot be solved by rewriting due to the extra variable in the last rule.10

``` Maude> vu-narrow  in LAST-APPEND : last(0 : s(0) : nil) =>! Z:Nat .  Solution 1 state: s(0) accumulated substitution: variant unifier: Z:Nat --> s(0)
```

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

``` mod MEMBERSHIP is  protecting LAST-APPEND .  vars XS YS ZS : NatList .  vars N M X Y : Nat .  op member : Nat NatList -> [Success] .  rl member(N, XS) => append(YS, N : ZS) =:= XS [nonexec narrowing] . endm
```

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.

``` Maude> vu-narrow  in MEMBERSHIP : member(s(0), 0 : s(0) : nil) =>! success .  Solution 1 state: success accumulated substitution: variant unifier:
```

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

``` Maude> vu-narrow [,5] in MEMBERSHIP : member(N, 0 : s(0) : nil) =>! success .  Solution 1 state: success accumulated substitution: N --> 0 variant unifier:  Solution 2 state: success accumulated substitution: N --> s(0) variant unifier:  No more solutions.
```

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.