Chapter 15
Narrowing

15.1 Introduction

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 $x_1,\dots ,x_n$, 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\to y$ and $s(x)+y\to 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 [64]. 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 [67, 32, 70, 109, 92], partial evaluation [3], verification of cryptographic protocols [100], and equational unification [74], 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 $R=(\mathrm{\Sigma },E\cup 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\cup Ax$-unification procedure is available in Maude.¹ Let ${\mathit{\text{CSU}}}_{E\cup Ax}(u=u^{\prime })$ provide² a finitary and complete set of unifiers for any pair of terms $u,u^{\prime }$ with the same top sort. The $R,E\cup Ax$-narrowing relation on $T_{\mathrm{\Sigma }}(X)$ is defined as $t{\stackrel{}{\rightsquigarrow }}_{\sigma ,p,R,E\cup Ax}{t}^{\prime }$ (or ${\stackrel{}{\rightsquigarrow }}_{\sigma }$ when $p,R,E\cup Ax$ are understood) if there is a non-variable position $p$ of $t$, a (possibly renamed) rule $l\to r$ in $R$, and a unifier $\sigma \in {\mathit{\text{CSU}}}_{E\cup Ax}(t{|}_p=l)$ such that $t^{\prime }=\sigma (t{[r]}_p)$. We denote by $t{\rightsquigarrow }_{\sigma ,R,E\cup Ax}^{+}{t}^{\prime }$ (resp. $t{\rightsquigarrow }_{\sigma ,R,E\cup Ax}^{\ast }{t}^{\prime }$) the transitive (resp. reflexive-transitive) closure of the narrowing relation, where $\sigma$ 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\to 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:

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: $$\begin{array}{c}X+s(0){\rightsquigarrow }_{\{X\mapsto 0\},base}s(0)\hfill \\ \\ X+s(0){\rightsquigarrow }_{\{X\mapsto s(\#1:Nat)\},ind}s(\#1:Nat+s(0))\hfill \end{array}$$

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.

$\underline{X+s(0)}{\rightsquigarrow }_{\{X\mapsto 0\},base}s(0)$

2.

$\underline{X+s(0)}\begin{array}{c}{\rightsquigarrow }_{\{X\mapsto s(\#1:Nat)\},ind}s(\underline{\#1:Nat+s(0)})\hfill \\ {\rightsquigarrow }_{\{\#1:Nat\mapsto 0\},base}s(s(0))\hfill \end{array}$

3.

$\underline{X+s(0)}\begin{array}{c}{\rightsquigarrow }_{\{X\mapsto s(\#1:Nat)\},ind}s(\underline{\#1:Nat+s(0)})\hfill \\ {\rightsquigarrow }_{\{\#1:Nat\mapsto s(\#2:Nat)\},ind}s(s(\underline{\#2:Nat+s(0)}))\hfill \\ {\rightsquigarrow }_{\{\#2:Nat\mapsto 0\},base}s(s(s(0)))\hfill \end{array}$

and so on.

The following infinite narrowing derivation resulting from applying rule ind infinitely many times can also be shown: $$\underline{X+s(0)}\begin{array}{c}{\rightsquigarrow }_{\{X\mapsto s(\#1:Nat)\},ind}s(\underline{\#1:Nat+s(0)})\hfill \\ {\rightsquigarrow }_{\{\#1:Nat\mapsto s(\#2:Nat)\},ind}s(s(\underline{\#2:Nat+s(0)}))\hfill \\ {\rightsquigarrow }_{\{\#2:Nat\mapsto s(\#3:Nat)\},ind}s(s(s(\underline{\#3:Nat+s(0)})))\hfill \\ \dots \hfill \end{array}$$

15.2 Applications

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

Instead, when the rules $R$ are understood as transition rules, a completely different application of $R,E\cup Ax$-narrowing is that of symbolic reachability analysis [100]. Specifically, we will consider the case of transition systems specified by order-sorted rewrite theories of the form $R=(\mathrm{\Sigma },E\cup Ax,R)$ where: (i) $E\cup Ax$ has a finite and complete $E\cup Ax$-unification algorithm (see the requirements of Section 14.1), and (ii) the transition rules $R$ are $E\cup 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 $\exists <!--FUNCTION\; APPLICATION-->\overline{x}t(\overline{x}){\to }^{\ast }{t}^{\prime }(\overline{x})$ in the sense that the formula holds for $R$ iff there is a narrowing sequence $t{\rightsquigarrow }_{R,E\cup Ax}^{\ast }u$ such that $u$ and $t^{\prime }$ have an $E\cup Ax$-unifier.

Furthermore, in symbolic reachability analysis we may be interested in verifying properties more general than existential questions of the form $\exists <!--FUNCTION\; APPLICATION-->Xt{\to }^{\ast }{t}^{\prime }$. One can also generalize the above reachability question to questions of the form $R,t\vDash \phi$, with $\phi$ a temporal logic formula. The papers [59, 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 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 from each of those initial states.

15.3 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 $\{\mathtt{\text{X}}\mapsto \mathtt{\text{s(Y)}}\}$ for the reachability problem $\exists <!--FUNCTION\; APPLICATION-->\mathtt{\text{X}},\mathtt{\text{Y}}\mathtt{\text{0 + X}}{\to }^{\ast }\mathtt{\text{s(Y)}}$ and it terminates with no more solutions. Instead, for the reachability problem $\exists <!--FUNCTION\; APPLICATION-->\mathtt{\text{X}},\mathtt{\text{Z}}\mathtt{\text{X + s(0)}}{\to }^{\ast }\mathtt{\text{s(s(Z))}}$, narrowing computes the solution $\{\mathtt{\text{X}}\mapsto \mathtt{\text{s(0)}}, \mathtt{\text{Z}}\mapsto \mathtt{\text{0}}\}$ but it cannot terminate because of the above infinite narrowing sequence using ind. Moreover, narrowing cannot prove that the reachability problem $\exists <!--FUNCTION\; APPLICATION-->\mathtt{\text{X}}\mathtt{\text{X + s(0)}}{\to }^{\ast }\mathtt{\text{0}}$ does not have a solution, again because of the above infinite narrowing sequence using ind.

Note that for any narrowing sequence $t{\rightsquigarrow }_{\sigma ,R,E\cup Ax}^{\ast }s$, we have a corresponding rewrite sequence $\sigma (t){\to }_{R∕E\cup Ax}^{\ast }{s}^{\prime }$, where, by definition, the rewrite relation ${\to }_{R∕E\cup Ax}$ is the relation composition: ${\to }_{R∕E\cup Ax}{=}_{def}({=}_{E\cup Ax});{\to }_R;({=}_{E\cup Ax})$, i.e., the transition relation between states in the given rewrite theory $R=(\mathrm{\Sigma },E\cup Ax,R)$. However, only under appropriate conditions is narrowing complete as an equational unification algorithm [74, 75], or as a procedure to solve reachability problems [100]. That is, given a reachability problem⁵ $\exists <!--FUNCTION\; APPLICATION-->x_1,\dots ,x_k:s{\to }^{\ast }t$, completeness of narrowing for reachability analysis means that for each possible substitution $\rho$ such that $\rho (s){\to }_{R∕E\cup Ax}^{\ast }\rho (t)$, and for all the substitutions ${\sigma }_1,\dots ,{\sigma }_n,\dots$, provided by narrowing from $s$, there is an index $i$ and a term $u_i$ such that, if $s{\rightsquigarrow }_{{\sigma }_1,R,E\cup Ax}{u}_1\cdots u_{i-1}{\rightsquigarrow }_{{\sigma }_i,R,E\cup Ax}{u}_i$, then there is an $E\cup Ax$-unifier $\tau$ of the equation $u_i=t$, and therefore there is a rewrite sequence $\tau (\sigma (s)){\to }_{R∕E\cup Ax}^{\ast }\tau (u_i)$, showing that an instance of $s$ reaches an instance of $t$ modulo the equations $E\cup Ax$. Essentially, completeness holds under the following conditions:

1.

for $(R,E\cup Ax)$-normalized substitutions $\rho$ above [100] (a stronger condition is $(R\cup E,Ax)$-normalized substitutions);

2.

for topmost rewrite theories⁶ ;

3.

for right-linear theories and linear reachability goals⁷ ;

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.4 Narrowing with simplification

As pointed out in Footnote 1, given a rewrite theory $R=(\mathrm{\Sigma },E\cup G\cup Ax,R)$, where $Ax$ are the axioms, and $E\cup 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\cup G\cup Ax$, but only modulo $E\cup 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\cup G$ is that $E\cup Ax$ may be FVP, but $G$ may not be, so that variant $E\cup Ax$-unification is finitary, whereas variant $E\cup G\cup Ax$-unification will be infinitary and undecidable. Note that the standard case of narrowing with $R$ modulo $E\cup G\cup Ax$ is just the special case $G=\varnothing$, which may be particularly attractive if $E\cup 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\cup Ax$, and we normalize with oriented equations $\overrightarrow{E}\cup \overrightarrow{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{\stackrel{}{\rightsquigarrow }}_{\sigma ,p,R,E\cup Ax}{t}^{\prime }$ is followed by simplification using the relation ${\to }_{G\cup E,Ax}^{!}$, i.e., the combined relation $({\stackrel{}{\rightsquigarrow }}_{\sigma ,p,R,E\cup Ax};{\to }_{G\cup E,Ax}^{!})$ is defined as $t{\stackrel{}{\rightsquigarrow }}_{\sigma ,p,R,E\cup Ax};{\to }_{G\cup E,Ax}^{!}{t}^{<mi>″</mi>}$ iff $t{\stackrel{}{\rightsquigarrow }}_{\sigma ,p,R,E\cup Ax}{t}^{\prime }$, $t^{\prime }{\to }_{G\cup E,Ax}^{\ast }{t}^{″}$, and $t^{″}$ is $G\cup E,Ax$-irreducible. Note that this combined relation $({\stackrel{}{\rightsquigarrow }}_{\sigma ,p,R,E\cup Ax};{\to }_{G\cup E,Ax}^{!})$ may be incomplete, i.e., given a reachability problem of the form $t{\to }^{\ast }{t}^{\prime }$ and a solution $\sigma$ (i.e., $\sigma (t){\to }_{R,G\cup E\cup Ax}^{\ast }\sigma (t^{\prime })$), the relation ${\stackrel{}{\rightsquigarrow }}_{\sigma ,p,R,E\cup Ax};{\to }_{G\cup 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 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.5 Theories supported for narrowing reachability

The narrowing relation is defined on top of the order-sorted variant-based unification procedure described in Section 14.8. In order to avoid clashing of algorithms and notions, we have decided that the rules used for narrowing should be identifiable, as the equations for variant unification, and clearly distinguished from standard rules in Maude. For this purpose we have defined a new attribute for rules: the keyword narrowing.

Let mod $(\mathrm{\Sigma },G\cup E\cup Ax,R\cup H)$ 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 $(\mathrm{\Sigma },E\cup Ax)$ satisfies the restrictions mentioned in Section 14.8, 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 for system modules and [97] for coherence details).

We recall again that the rules $H$ are disregarded for narrowing modulo $E\cup 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. Note, 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. , They are given the standard meaning of not allowing any narrowing step below such frozen arguments, just as in the context-sensitive narrowing of [82].

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\cup Ax$-narrowing step are explored.

15.6 The 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 it uses variant-based unification at each step):

{fold,vfold,path} vu-narrow {filter,delay} [ $n$, $m$ ] in $⟨$ModId$⟩$ : 
  $⟨$Term-1$⟩$ $⟨$SearchArrow$⟩$ $⟨$Term-2$⟩$ .
     

where

• {fold} (or {vfold}) are optional and are explained in Section 15.6.3;

• {path} is optional and is explained in Section 15.6.5;

• {filter,delay} are optional and imply that filtered variant unification of Section 14.9 is invoked;

• $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 (Section 15.6.6 describes how to perform narrowing from a disjunction of initial terms instead of one single term);

• $⟨$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 equationally unified with this target pattern, in contrast to the search command of Section 5.4.3 that performs only matching);

• $⟨$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 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.4 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 [1] 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
     

Maude can now show the narrowing trace associated to each solution (see Section 15.6.5 below), but it is easy to see that one application of the rule buy-a happened after (or before) one application of the rule buy-c.

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 [74] to be used for equational unification and requiring the folding variant narrowing [62] to be used for equational unification.

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 (modulo the order of the two applications of buy-c and buy-a one after the other). 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 [,3] 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 command show frontier states outputs the frontier (open leaves) of the narrowing-based reachability graph. Note that this command is not available for the search command. For example, we can type this frontier command after the previous vu-narrow command to see the leaves for depth $3$; unfortunately, state identifiers are not shown.

Maude> show frontier states . 
< c c c @1:Money > \/ 
< q a c c @1:Money > \/ 
< q a c c @1:Money > \/ 
< a c c #1:Money > \/ 
< q q a a c @1:Money > \/ 
< q a a c #1:Money > \/ 
< q a c c @1:Money > \/ 
< a c c #1:Money > \/ 
< q q a a c @1:Money > \/ 
< q a a c #1:Money > \/ 
< a c c @1:Money > \/ 
< q a a c @1:Money > \/ 
< q q a a c @1:Money > \/ 
< a a c #1:Money > \/ 
< q q q a a a @1:Money > \/ 
< q a a a #1:Money > \/ 
< q a a c @1:Money > \/ 
< a a c %1:Money > \/ 
< q q a a a @1:Money > \/ 
< q a a a %1:Money >
     

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 [,3] in NARROWING-VENDING-MACHINE : < M:Money > =>! < a c > . 
 
No solution.
     

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 =>*.

Maude> vu-narrow 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.
     

Indeed, the show frontier states command shows that there are no open leaves because the narrowing tree is terminating.

Maude> show frontier states . 
*** frontier is empty ***
     

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 [5] 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.6.1 Variant unification options

Sections 13.4 and 14.9 provide a command for computing minimal sets of, respectively, unifiers modulo axioms or modulo a convergent equational theory. Narrowing with rules modulo an equational theory has also been extended to use a minimal set of unifiers. The filter flag indicates that filtering is activated but it can be done either during equational unification (the delay flag is not included) or after all equational unifiers have been computed (the delay flag is included); the latter being the method used in the filtered variant unify command of Section 14.9.

For instance, we can use the narrowing search command to answer the question:

Can I get an apple and a cake starting with the exact money?

The answer should be an obvious yes but the symbolic reachability question gets into too many paths.

Maude> vu-narrow [, 2] in NARROWING-VENDING-MACHINE : 
       < $ q q q M1:Money > =>* < a c M2:Money > . 
 
Solution 1 
state: < $ a c %1:Money > 
accumulated substitution: 
M1:Money --> $ %1:Money 
variant unifier: 
M2:Money --> $ @1:Money 
%1:Money --> @1:Money 
 
... 
 
Solution 9 
state: < $ a c #1:Money > 
accumulated substitution: 
M1:Money --> q q q q #1:Money 
variant unifier: 
M2:Money --> $ @1:Money 
#1:Money --> @1:Money 
 
No more solutions. 
rewrites: 34 in 9ms cpu (10ms real) (3664 rewrites/second)
     

We can ask Maude to filter unifiers at each narrowing step, and the branching is, obviously, smaller.

Maude> vu-narrow {filter} [, 2] in NARROWING-VENDING-MACHINE : 
       < $ q q q M1:Money > =>* < a c M2:Money > . 
 
Solution 1 
state: < $ a c %1:Money > 
accumulated substitution: 
M1:Money --> $ %1:Money 
variant unifier: 
M2:Money --> $ @1:Money 
%1:Money --> @1:Money 
 
Solution 2 
state: < q a c #1:Money > 
accumulated substitution: 
M1:Money --> q #1:Money 
variant unifier: 
M2:Money --> q @1:Money 
#1:Money --> @1:Money 
 
Solution 3 
state: < a c %1:Money > 
accumulated substitution: 
M1:Money --> %1:Money 
variant unifier: 
M2:Money --> @1:Money 
%1:Money --> @1:Money 
 
No more solutions.
     

But the first solution is actually redundant, i.e., we can ask Maude to filter unifiers only after all have been generated, which is more expensive but ensures the minimal set of most general variant unifiers.

Maude> vu-narrow {filter,delay} [, 2] in NARROWING-VENDING-MACHINE : 
       < $ q q q M1:Money > =>* < a c M2:Money > . 
 
Solution 1 
state: < q a c #1:Money > 
accumulated substitution: 
M1:Money --> q #1:Money 
variant unifier: 
M2:Money --> q @1:Money 
#1:Money --> @1:Money 
 
Solution 2 
state: < a c %1:Money > 
accumulated substitution: 
M1:Money --> %1:Money 
variant unifier: 
M2:Money --> @1:Money 
%1:Money --> @1:Money 
 
No more solutions.
     

Note that the simplest path is the second solution, since all the necessary money was given.

15.6.2 Filtered vs. unfiltered symbolic reachability analysis

The vu-narrow {filter,delay} command can achieve dramatic state space reductions over the previous vu-narrow command by filtering $E\cup B$-unifiers. This is illustrated in this section by a simple rewrite theory describing a cryptographic protocol inspired by the strand space model [63], which is the basis for the Maude-NPA protocol analyzer [57, 58]. The protocol appeared in [54, 60]. The cryptographic function’s equational properties are those of the following exclusive-or FVP theory:

fmod EXCLUSIVE-OR is 
 sort XOR . 
 op mt : -> XOR . 
 op _*_ : XOR XOR -> XOR [assoc comm] . 
 vars X Y Z U V : [XOR] . 
 eq [nilp] :    X * X = mt   [variant] . 
 eq [nilp-Coh] : X * X * Z = Z [variant] . 
 eq [id] :      X * mt = X   [variant] . 
endfm
   

The strand space syntax is given in a general form.

mod PROTOCOL-SYNTAX is 
 sorts Name Nonce Fresh Msg . 
 subsort Name Nonce < Msg . 
 
 ops a b i : -> Name . --- Alice Bob Intruder 
 op n : Name Fresh -> Nonce . --- Nonces 
 ops r1 r2 r3 : -> Fresh . 
 op pk : Name Msg -> Msg . --- Public encryption 
 
 sort SMsg . 
 ops + - : Msg -> SMsg . 
 
 sort SMsgList . subsort SMsg < SMsgList . 
 op nil : -> SMsgList . 
 op _,_ : SMsgList SMsgList -> SMsgList [assoc] . 
 
 sort Strand . 
 op [_|_] : SMsgList SMsgList -> Strand . 
 
 sort StrandSet . 
 subsort Strand < StrandSet . 
 op mt : -> StrandSet . 
 op _&_ : StrandSet StrandSet -> StrandSet [assoc comm id: mt] . 
 
 sort IKnowledge . 
 op mt : -> IKnowledge . 
 op inI : Msg -> IKnowledge . --- Intruder knows 
 op nI : Msg -> IKnowledge . --- Intruder doesn’t know 
 op _,_ : IKnowledge IKnowledge -> IKnowledge [assoc comm id: mt] . 
 
 sort State . 
 op {_{_}} : StrandSet IKnowledge -> State . 
endm
   

The exclusive-or protocol example is defined in the following module, where nonces are combined using exclusive-or.

mod PROTOCOL-XOR is 
 extending EXCLUSIVE-OR . 
 extending PROTOCOL-SYNTAX . 
 subsort Nonce < XOR < Msg . 
 var IK : IKnowledge .  var SS : StrandSet . 
 var M : Msg .        vars L1 L2 : SMsgList . 
 
 --- Intruder knows receiving message of a strand 
 rl [recv] : { (SS & [ ( L1 , -(M)) | L2 ])  { (inI(M) , IK) } } => 
           { (SS & [ L1 | (-(M) , L2) ])  { (inI(M) , IK) } } [narrowing] . 
 --- Intruder learns a sending message of a strand 
 rl [snd] : { (SS & [ (L1 , +(M)) | L2 ])  { (inI(M) , IK) } } => 
           { (SS & [ L1 | (+(M) , L2) ])  { (nI(M) , IK) } } [narrowing] . 
endm
   

Actually, due to this general strand syntax, the protocol itself is given as a term. And, due to the fact that the rewrite rules are given in a reversed way, the initial term contains the protocol with the vertical bars on the rightmost position, denoting a finished strand, and the intruder knowledge with inI operators, denoting terms learned by the intruder, whereas the target term contains the protocol with the vertical bars on the leftmost position, denoting a non-started strand, and the intruder knowledge with nI operators, denoting terms not yet learned by the intruder. The initial term of the narrowing-based reachability command is

{ 
 [ nil, -(pk(a, X)), +(pk(b, n(a, r2))), -(X * n(a, r2)) | nil] & 
 [ nil, +(pk(a, n(b, r1))), -(pk(b, Y )), +(Y * n(b, r1)) | nil] 
 { inI(X * n(a, r2)), inI(pk(b, Y )), inI(pk(a, X)) } 
}
     

{ 
 [ nil | -(pk(a, X)), +(pk(b, n(a, r2))), -(X * n(a, r2)), nil] & 
 [ nil | +(pk(a, n(b, r1))), -(pk(b, Y )), +(Y * n(b, r1)), nil] 
 { nI(X * n(a, r2)), nI(pk(b, Y )), nI(pk(a, X)) } 
}
     

Note that there are variables X and Y only for the unknown parts of receiving messages of Alice and Bob. This reduces the search space considerably: it becomes a finite symbolic search space with depth $6$, so we can focus only on the difference between filtered and unfiltered variant unification. The unfiltered symbolic reachability search command without folding is as follows:

Maude> vu-narrow 
         { 
           [ nil, -(pk(a, X:Msg)), +(pk(b, n(a, r2))), -(X:Msg * n(a, r2)) | nil] & 
           [ nil, +(pk(a, n(b, r1))), -(pk(b, Y:Msg)), +(Y:Msg * n(b, r1)) | nil] 
           { inI(X:Msg * n(a, r2)), inI(pk(b, Y:Msg)), inI(pk(a, X:Msg)) } 
         } 
      =>* { 
           [ nil | -(pk(a, X:Msg)), +(pk(b, n(a, r2))), -(X:Msg * n(a, r2)), nil] & 
           [ nil | +(pk(a, n(b, r1))), -(pk(b, Y:Msg)), +(Y:Msg * n(b, r1)), nil] 
           { nI(X:Msg * n(a, r2)), nI(pk(b, Y:Msg)), nI(pk(a, X:Msg)) } 
         } . 
 
Solution 1 
rewrites: 26528 in 1937ms cpu (2163ms real) (13694 rewrites/second) 
state: {[nil | +(pk(a, n(b, r1))),-(pk(b, n(a, r2))),+(n(a, r2) * n(b, r1)),nil] & 
 [nil | -(pk(a, n(b, r1))),+(pk(b, n(a, r2))),-(n(a, r2) * n(b, r1)),nil]{nI(n(a, 
 r2) * n(b, r1)),nI(pk(a, n(b, r1))),nI(pk(b, n(a, r2)))}} 
accumulated substitution: 
Y:Msg --> mt * n(a, r2) 
X:Msg --> mt * n(b, r1) 
variant unifier: 
 
Solution 2 
rewrites: 26533 in 1938ms cpu (2164ms real) (13689 rewrites/second) 
state: {[nil | +(pk(a, n(b, r1))),-(pk(b, n(a, r2))),+(n(a, r2) * n(b, r1)),nil] & 
 [nil | -(pk(a, n(b, r1))),+(pk(b, n(a, r2))),-(n(a, r2) * n(b, r1)),nil]{nI(n(a, 
 r2) * n(b, r1)),nI(pk(a, n(b, r1))),nI(pk(b, n(a, r2)))}} 
accumulated substitution: 
Y:Msg --> n(a, r2) * n(a, r2) * n(a, r2) 
X:Msg --> n(a, r2) * n(a, r2) * n(b, r1) 
variant unifier: 
 
... 
 
Solution 84 
rewrites: 26937 in 2015ms cpu (2243ms real) (13364 rewrites/second) 
state: {[nil | +(pk(a, n(b, r1))),-(pk(b, n(a, r2))),+(n(a, r2) * n(b, r1)),nil] & 
 [nil | -(pk(a, n(b, r1))),+(pk(b, n(a, r2))),-(n(a, r2) * n(b, r1)),nil]{nI(n(a, 
 r2) * n(b, r1)),nI(pk(a, n(b, r1))),nI(pk(b, n(a, r2)))}} 
accumulated substitution: 
Y:Msg --> n(a, r2) * n(b, r1) * n(b, r1) 
X:Msg --> n(a, r2) * n(a, r2) * n(b, r1) 
variant unifier: 
 
No more solutions.