Chapter 16
Narrowing

with Santiago Escobar

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 [54] and then generalized to solve the more general problem of symbolic reachability [86]. The narrowing mechanism has a number of important applications including automated proofs of termination [6], execution of functional-logic programming languages [58, 30, 61, 95, 79], partial evaluation [4], verification of cryptographic protocols [86], and equational unification [65], 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 = (Σ,Ax,R) be an order-sorted rewrite theory where R is a set of unconditional rewrite rules specified with the rl keyword and Ax is a set of commonly occurring axioms (declared in Maude as equational attributes, see Section 4.4.1), such that an Ax-unification procedure is available in Maude (only unification for order-sorted signatures with free, C, or AC function symbols is available at this moment, see Chapter 12). Let CSU_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,Ax-narrowing relation on _Σ() is defined as t_σ,p,R,Ax t′ (or _σ when p,R,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_Ax(t|_p = l) such that t′ = (t[r]_p)σ. We denote by t ↝_σ,R,Ax⁺t′ (resp. t ↝_σ,R,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:

Given an order-sorted rewrite theory (Σ,Ax,R), a reachability problem is of the form ∃X₁,…,X_k s.t. s →^*t, where X₁,…,X_k are all the variables of s and t. Such a reachability problem can be solved by narrowing modulo Ax, yielding a (possibly infinite) set of substitutions σ₁,…,σ_n,… that bind some variables of X₁,…,X_k in such a way that σ_i(s) →_R,Ax^*σ_i(t) for each i.

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 above Maude module, narrowing computes the solution {Xs(Y)} for the reachability problem ∃X,∃Y s.t. 0 + X →^*s(Y) and it terminates with no more solutions. Instead, for the reachability problem ∃X,∃Z s.t. 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 s.t. X + s(0) →^*0 does not have a solution, again because of the above infinite narrowing sequence using ind.

We have implemented a version of narrowing with simplification, which is slightly different from the one formally defined above. Let = (Σ,E ∪ Ax,R) be an order-sorted rewrite theory where R and Ax are defined as above and E are the remaining equations specified with the eq or ceq keywords. Each narrowing step of the form t_σ,p,R,Ax t′ is followed by simplification using the relation →_E,Ax^!, i.e., the combined relation (_σ,p,R,Ax;→_E,Ax^!) is defined as t_σ,p,R,Ax;→_E,Ax^!t′′ iff t_σ,p,R,Ax t′, t′→_E,Ax^*t′′, and t′′ is E,Ax-irreducible. Note that this combined relation (_σ,p,R,Ax;→_E,Ax^!) may be incomplete, i.e., given a reachability problem of the form t →^*t′ and a solution σ (i.e., σ(t) →_R,E∪Ax^*σ(t′)), the relation _σ,p,R,Ax;→_E,Ax^! may not be able to find a more general solution. The reason is that the equations E should also be executed by narrowing instead of rewriting to ensure completeness under appropriate conditions (see [86] and Section 16.2). However, the combination of narrowing using rules and axioms with simplification using equations and axioms 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.

16.2 Completeness of narrowing

Note that for any narrowing sequence t ↝_σ,R,Ax^*s, we have a corresponding rewrite sequence σ(t) →_R,Ax^*s. However, only under appropriate conditions is narrowing complete as an equational unification algorithm [65, 66], or as a procedure to solve reachability problems [86]. That is, given a reachability problem³ ∃X₁,…,X_k s.t. s →^*t completeness means that for each possible substitution ρ that binds some variables of X₁,…,X_k in such a way that ρ(s) →_R,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,Ax^*θ(s), ρ(t) →_R,Ax^*θ(t), θ(s) →_R,Ax^*θ(t), and θ = _Axσ_i;τ, where σ_i;τ denotes substitution composition in diagrammatic order, i.e., (σ_i;τ)(X) = τ(σ_i(X)). Essentially, completeness holds either

1. for R,Ax-normalized substitutions ρ above [86];
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, as the equational theories in Maude functional modules with such properties restricted to unconditional equations.

16.3 Theories supported

The narrowing relation is defined on top of the order-sorted unification procedure described in Chapter 12. As described there, Maude 2.4 currently provides an order-sorted Ax-unification algorithm for all order-sorted theories (Σ,E ∪ Ax) such that:

• the signature Σ is preregular modulo Ax (see Sections 3.8 and 14.2.5);
• the axioms Ax associated to function symbols are as follows:
  • there can be arbitrary function symbols and constants with no equational attributes;
  • the iter equational attribute can be declared for some unary symbols;
  • the comm or assoc comm attributes can be declared for some binary function symbols, but then no other equational attributes must be given for such symbols.

Explicitly excluded are theories with binary function symbols having either: (i) the id:, left id:, or right id: attributes; or (ii) the assoc attribute without the comm one; or (iii) a combination of (i) and (ii) (for example, a binary symbol with only assoc and id: attributes).

Let mod (Σ,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) such that (Σ,Ax) satisfies the restrictions mentioned above and in Chapter 12, and E 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). This is not currently required for rewrite theories written in Maude because coherence is implicitly implemented within Maude. However, coherence must be explicitly introduced within the rewrite theory if we plan to use narrowing. The reason is that there is a different treatment of extension variables in rewriting and narrowing (see [103] for more details). Indeed, we require coherence rather than ground coherence, since the latter is weaker and sufficient for rewriting but insufficient for narrowing; see Section 5.3 for further details.

  For example, for Ax = AC, coherence modulo AC is easily achieved by adding to each rule in R with a top AC function symbol in its lefthand side a similar rule with an extra “extension variable” argument added to the AC function symbol, as explained in Section 4.8.

We recall again that the equations E in the system module are disregarded for narrowing purposes. However, they are applied for simplification after each narrowing step, 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, and are given the standard meaning of not allowing any narrowing step below such frozen arguments, just as in the context-sensitive narrowing of [70].

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,Ax-narrowing step are explored.

16.4 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 variant of the vending machine for buying apples (a) or cakes (c) with dollars ($) and quarters (q) used in different parts of the manual, where now the rules are explicitly coherent and the lefthand sides are non-variable terms (this theory does indeed satisfy the completeness requirements for reachability mentioned in [86] and Section 16.2 above):

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

This is done by searching for states that have a variable of sort Money instead of sort Marking at the starting term and match a corresponding pattern at the end.

Note that we must restrict the depth, because narrowing does not terminate for this reachability problem even though the above two solutions are indeed the only solutions. 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). Indeed, 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.5), the narrowing version does not provide paths to solutions.

We can formulate a more complex question for our vending machine:

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 can be bought is characterized by using the ~>! arrow instead of ~>*.

There are a couple of issues related to this reachability problem:

1. Solutions more general than those would be expected but are not generated, such as the following solution which is more general than solution 1:
     M:Money --> $ $ #1:Money ; MO’:Money --> q #1:Money

   The reason is that any state term enclosed by the <_> operator and containing a variable of sort Marking or Money does have a narrowing step from it and, thus, the state < q a c #1:Money > would not be strongly irreducible for narrowing.

2. Solutions containing several coins q would also be expected and are not generated, such as
     M:Money --> $ $ q q ; MO’:Money --> q q q

   Now the reason is that there is no rule that introduces symbols q by unification, so the substitution M:Money --> $ $ q q cannot be computed. This does not mean that narrowing is incomplete (it is indeed complete for this theory). This solution is indeed a substitution instance of the solution mentioned in (1) above.

The reason why we do not obtain these solutions is our restriction to strongly irreducible final states. But if we give the very same command but using the ~>* arrow instead of ~>!, we do obtain the substitution

described above. The somewhat subtle point is that the narrowing sequence

Another point of interest is the appearance of variables of the form #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.

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 (see [61]). 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 the kind [Nat] and the value error in order to describe what a successful solution is. The following reachability problem is solved by narrowing but cannot be solved by rewriting due to the extra variable in the last rule.⁷

16.5 Unification with identities: The id-unify command

As described in Chapter 12 and also recalled in Section 16.3, Maude 2.4 currently provides an order-sorted Ax-unification algorithm for all order-sorted theories (Σ,E ∪ Ax) such that Σ is preregular and Ax can include any combination of equational axioms for a function symbol except the id:, left id:, right id:, and assoc without comm.

As explained in Section 12.6.1, if a theory (Σ,E ∪ Ax) satisfies the coherence, confluence, and termination modulo Ax requirements, we can systematically reduce E ∪Ax-unification problems into narrowing problems as follows:

1. we define the signature by adding a fresh new sort Truth to Σ with a constant tt;
2. we define the set of rules by transforming each equation in E into a rule in ;
3. for each top sort of each connected component of sorts we add to a binary predicate eq of sort Truth and add to the rule eq(x,x) → tt, where x has such a top sort;
4. we define the rewrite theory (,Ax, ∪);
5. we then reduce an E∪Ax-unification problem tt′ to the narrowing reachability problem eq(t,t′) →^*tt modulo Ax in the rewrite theory (,Ax,).

That is, we search for all narrowing paths modulo Ax from eq(t,t′) to tt. Each such path then gives us a unifier of the equation tt′, just by composing the unifiers of each narrowing step in the narrowing path.

Therefore, if a theory (Σ,Ax) contains the id:, left id:, or right id: attributes in Ax (but not assoc without comm), we can perform unification modulo Ax as follows:

1. we decompose Ax into a disjoint union Ax = ∪ Ids, where does not contain any id:, left id:, or right id: attribute, and Ids is the set of such extra attributes;
2. we define the rewrite theory (Σ,,) where contains the obvious rules for each of the equational identity attributes, that is:
   • if f has an id: attribute in Ax and [s] is the top sort of f (which we can identify with the kind), we add rules f(x,e) → x and f(e,x) → x into , where x is a variable of sort [s] and e is the identity symbol (if f has also the comm attribute, only one such rule is needed);
   • likewise, for f with the left id: (resp. right id:) attribute, we add the rule f(e,x) → x (resp. f(x,e) → x) into ;
3. we define the theory (,, ∪) as above and then reduce an Ax-unification problem tt′ to the narrowing reachability problem eq(t,t′) →^*tt modulo in the rewrite theory (,, ∪).

However, solving such reachability problems for ACU-unification using full AC-narrowing can easily lead to an infinite search space and therefore to undecidability, since it is well-known that narrowing modulo AC “almost never terminates” and, furthermore, that narrowing strategies facilitating termination such as basic narrowing are incomplete [27, 103]. However, based on the idea of “variants” in [27], a complete, yet quite efficient in terms of its search space, narrowing strategy modulo Ax, called variant narrowing, has been proposed in [53]. Such unification procedure can be used for ACU-unification in an equational theory (Σ,Ax) containing the id:, left id:, or right id: attributes in Ax but not assoc without comm. We proceed as follows (see [53] for further details):

1. we take the rewrite theory (Σ,,) as defined above;
2. for the unification problem tt′, we compute the variants of t and the variants of t′ using (Σ,,) and perform -unification pairwise among all the variants of t and t′.

The unification procedure using variants is implemented through the command id-unify explained below.

Given a functional module, system module, or theory ⟨ModId⟩ having a set Ax of equational axioms for the signature Σ such that Σ does not include symbols with assoc without comm attributes in Ax, the user can give to Full Maude a unification command for Ax-unification of the form:

where only one unification problem is admitted (in contrast to the unify command described in Section 12.4) and such that no limit to the number of unifiers can be specified. The theories supported must satisfy the following requirements:

• the signature Σ is preregular modulo Ax (see Sections 3.8 and 14.2.5);
• the equational axioms Ax associated to function symbols are as follows:
  • there can be arbitrary function symbols and constants with no equational attributes;
  • the iter equational attribute can be declared for some unary symbols;
  • the id:, left id:, right id:, comm, comm id:, assoc comm, and assoc comm id: attributes can be declared for some binary function symbols, but any assoc attribute must also be accompanied by comm.

Consider, for example, the following simple definition of multisets with identity:

We can use the id-unify command to solve the following three unification problems:

For the following substitutions computed for the last unification problem: σ₁ = {X:MSet(a Y:MSet)} and σ₂ = {X:MSeta,Y:MSete}, the reader might believe that σ₂ is subsumed by σ₁, because the substitution ρ = {Y:MSete} can be built in such a way that σ₁;ρ can be normalized into σ₂. However, they are incomparable modulo AC, since both computed substitutions are valid only for ,-normalized substitutions. Indeed, our equational unification procedure modulo identity can compute only ,-normalized unifiers which are valid only for ,-normalized instance substitutions. That is, given Ax = ∪ Ids, a unification problem tt′, and a Ax-unifier σ,

1. σ is assumed to be ,-normalized (if not, we can normalize it and the normalized version will still be a valid Ax-unifier);
2. there will be a computed Ax-unifier θ and an extra substitution ρ such that σ = θ;ρ and both θ and ρ are also assumed to be ,-normalized.

Let us illustrate also the use of left-id and right-id attributes. Consider the following variation of the previous example where we remove associativity and commutativity, but still keep the identity operator as a left identity:

Then the following two unification problems have a different and peculiar meaning, where we have swapped the position of the variables.

Let us now consider the case of a right identity:

Then the very same unification problems above have a different behavior

16.6 Reachability at the metalevel: metaNarrowSearch

Narrowing-based reachability analysis is also available at the metalevel by using the function metaNarrowSearch. The functional module providing the necessary infrastructure is called META-NARROWING-SEARCH and the function metaNarrowSearch has the following declaration:

If a non-identity substitution is provided in the fourth argument, 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.4.6). For the bounds, the first bound is the maximum length of the narrowing sequences, i.e., the depth of the narrowing tree, and the second bound is the number of computed solutions.

For the NARROWING-VENDING-MACHINE system module in Section 16.4, the following search command considered in that section

can be specified at the metalevel as follows, where ’<_>[’M:Money] is the metarepresentation of the state < M:Money > and ’<_>[’__[’a.Item,’c.Item]] is the metarepresentation of the state < a c >:

Note that we obtain the very same two solutions, where the output contains two terms of type ResultTriple, each one containing the actual output term, its type, and the computed substitution, and

is the metarepresentation of the substitution M:Money --> $ q q q, whereas

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

16.7 Unification with identities at the metalevel:
metaACUUnify

The procedure for equational Ax-unification where Ax can contain any equational attribute except assoc without comm is available at the metalevel by using the metaACUUnify function. The functional module providing the necessary infrastructure is called META-E-UNIFICATION and the metaACUUnify function has the following declaration:

For the ID-UNIFICATION-EXAMPLE system module in Section 16.5, the following id-unify command considered in that section

can be specified at the metalevel as follows, where ’__[’a.Elem, ’X:MSet] metarepresents the term a X:MSet and ’__[’__[’a.Elem, ’a.Elem], ’Y:MSet] metarepresents the term a a Y:MSet:

Note that, as expected, the very same two solutions are returned, i.e., the metarepresentations of the two substitutions X:MSet --> a Y:MSet and X:MSet --> a ; Y:MSet --> e.