Narrowing

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.^{1} Let
CSU_{E∪Ax}(u = u′) provide^{2}
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^{3}
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

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:

- 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:

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.

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^{4}
∃X_{1},…,X_{k} s →^{*}t completeness means that for each possible substitution ρ that binds some variables
of X_{1},…,X_{k} in such a way that ρ(s) →_{R,E∪Ax}^{*}ρ(t), and for all the substitutions σ_{1},…,σ_{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
^{5}; - 3.
- for right-linear theories and linear reachability goals
^{6}; 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.

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.

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.

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.

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

rl [buy-a] : < M $ > => < M a q > .

eq [change] : q q q q = $ [variant] .

endm

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

rl [buy-a] : < M $ > => < M a q > .

eq [change] : q q q q = $ [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> (search [1] in NARROWING-VENDING-MACHINE :

< M:Money > ~>* < a c > .)

Solution 1

M:Money --> $ q q q

No more solutions.

< M:Money > ~>* < a c > .)

Solution 1

M:Money --> $ q q q

No more solutions.

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.

Maude> (search [,5] in NARROWING-VENDING-MACHINE :

< M:Money > ~>* < a c > .)

Solution 1

M:Money --> $ q q q

No more solutions.

< M:Money > ~>* < a c > .)

Solution 1

M:Money --> $ q q q

No more solutions.

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.

Maude> (search [,5] in NARROWING-VENDING-MACHINE :

< M:Money > ~>! < a c > .)

No more solutions.

< M:Money > ~>! < a c > .)

No more solutions.

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

Maude> (search [,5] in NARROWING-VENDING-MACHINE :

< C1:Coin C2:Coin C3:Coin C4:Coin > ~>! < M:Money a c > .)

Solution 1

C1:Coin --> $ ; C2:Coin --> q ; C3:Coin --> q ; C4:Coin --> q ; M:Money --> empty

Solution 2

C1:Coin --> q ; C2:Coin --> $ ; C3:Coin --> q ; C4:Coin --> q ; M:Money --> empty

Solution 3

C1:Coin --> q ; C2:Coin --> q ; C3:Coin --> $ ; C4:Coin --> q ; M:Money --> empty

Solution 4

C1:Coin --> q ; C2:Coin --> q ; C3:Coin --> q ; C4:Coin --> $ ; M:Money --> empty

No more solutions.

< C1:Coin C2:Coin C3:Coin C4:Coin > ~>! < M:Money a c > .)

Solution 1

C1:Coin --> $ ; C2:Coin --> q ; C3:Coin --> q ; C4:Coin --> q ; M:Money --> empty

Solution 2

C1:Coin --> q ; C2:Coin --> $ ; C3:Coin --> q ; C4:Coin --> q ; M:Money --> empty

Solution 3

C1:Coin --> q ; C2:Coin --> q ; C3:Coin --> $ ; C4:Coin --> q ; M:Money --> empty

Solution 4

C1:Coin --> q ; C2:Coin --> q ; C3:Coin --> q ; C4:Coin --> $ ; 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 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^{7} ,
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:

(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 .

rl append(N : XS, YS) => N : append(XS, YS) .

op last : NatList -> [Nat] .

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

op _>>_ : [Success] [Nat] -> [Nat] [frozen (2) strat (1 0)] .

eq success >> X:[Nat] = X:[Nat] .

op _=:=_ : Nat Nat -> [Success] [comm] .

rl N =:= N => success .

op _=:=_ : NatList NatList -> [Success] [comm] .

rl XS =:= XS => success .

endm)

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 .

rl append(N : XS, YS) => N : append(XS, YS) .

op last : NatList -> [Nat] .

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

op _>>_ : [Success] [Nat] -> [Nat] [frozen (2) strat (1 0)] .

eq success >> X:[Nat] = X:[Nat] .

op _=:=_ : Nat Nat -> [Success] [comm] .

rl N =:= N => success .

op _=:=_ : NatList NatList -> [Success] [comm] .

rl XS =:= XS => success .

endm)

In the rule

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

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 [58]. The following reachability problem is solved
by narrowing but cannot be solved by rewriting due to the extra variable in the last
rule.^{8}

Maude> (search [1] in LAST-APPEND : last(0 : s(0) : nil) ~>! Z:Nat .)

Solution 1

Z:Nat --> s(0)

No more solutions.

Solution 1

Z:Nat --> s(0)

No more solutions.

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] .

endm)

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] .

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> (search [1] in MEMBERSHIP :

member(s(0), 0 : s(0) : nil) ~>! success .)

Solution 1

empty substitution

No more solutions.

member(s(0), 0 : s(0) : nil) ~>! success .)

Solution 1

empty substitution

No more solutions.

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

Maude> (search [,5] in MEMBERSHIP :

member(N:Nat, 0 : s(0) : nil) ~>! success .)

Solution 1

N:Nat --> 0

Solution 2

N:Nat --> s(0)

No more solutions.

member(N:Nat, 0 : s(0) : nil) ~>! success .)

Solution 1

N:Nat --> 0

Solution 2

N:Nat --> s(0)

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.

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:

op metaNarrowSearch :

Module Term Term Substitution Qid Bound Bound Bound -> ResultTripleSet .

Module Term Term Substitution Qid Bound Bound Bound -> ResultTripleSet .

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

op {_,_,_} : Term Type Substitution -> ResultTriple .

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

sort ResultTripleSet .

subsort ResultTriple < ResultTripleSet .

op empty : -> ResultTripleSet [ctor] .

op _|_ : ResultTripleSet ResultTripleSet -> ResultTripleSet

[ctor assoc comm id: empty prec 65 format (d d n d)] .

eq X:ResultTriple | X:ResultTriple = X:ResultTriple .

subsort ResultTriple < ResultTripleSet .

op empty : -> ResultTripleSet [ctor] .

op _|_ : ResultTripleSet ResultTripleSet -> ResultTripleSet

[ctor assoc comm id: empty prec 65 format (d d n d)] .

eq X:ResultTriple | X:ResultTriple = X:ResultTriple .

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

Maude> (search [1] in NARROWING-VENDING-MACHINE :

< M:Money > ~>* < a c > .)

< M:Money > ~>* < a c > .)

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.

Maude> reduce in FULL-MAUDE :

metaNarrowSearch(

axCohComplete(

upModule(’NARROWING-VENDING-MACHINE, false)),

’<_>[’M:Money],

’<_>[’__[’a.Item, ’c.Item]],

none, ’*, unbounded, 1, unbounded) .

result ResultTriple:

{ ’<_>[’__[’a.Item,’c.Item,’empty.Money]],

’State,

’#1:Marking <- ’__[’q.Coin,’q.Coin,’q.Coin,’empty.Money] ;

’#4:Marking <- ’__[’a.Item,’empty.Money] ;

’#6:Money <- ’empty.Money ;

’%3:Money <- ’__[’q.Coin,’q.Coin,’q.Coin,’empty.Money] ;

’M:Money <- ’__[’$.Coin,’__[’q.Coin,’q.Coin,’q.Coin,’empty.Money]] }

metaNarrowSearch(

axCohComplete(

upModule(’NARROWING-VENDING-MACHINE, false)),

’<_>[’M:Money],

’<_>[’__[’a.Item, ’c.Item]],

none, ’*, unbounded, 1, unbounded) .

result ResultTriple:

{ ’<_>[’__[’a.Item,’c.Item,’empty.Money]],

’State,

’#1:Marking <- ’__[’q.Coin,’q.Coin,’q.Coin,’empty.Money] ;

’#4:Marking <- ’__[’a.Item,’empty.Money] ;

’#6:Money <- ’empty.Money ;

’%3:Money <- ’__[’q.Coin,’q.Coin,’q.Coin,’empty.Money] ;

’M:Money <- ’__[’$.Coin,’__[’q.Coin,’q.Coin,’q.Coin,’empty.Money]] }

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

’M:Money <- ’__[’$.Coin, ’__[’q.Coin, ’q.Coin, ’q.Coin]]

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:

op metaNarrowSearchPath :

Module Term Term Substitution Qid Bound Bound

Bound -> TraceNarrowSet .

Module Term Term Substitution Qid Bound Bound

Bound -> TraceNarrowSet .

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:

Maude> reduce in FULL-MAUDE :

metaNarrowSearchPath(

axCohComplete(upModule(’NARROWING-VENDING-MACHINE, false)),

’<_>[’M:Money],

’<_>[’__[’a.Item, ’c.Item]],

none, ’*, unbounded, 1, unbounded) .

result TraceNarrow:

{ ’<_>[’__[’%3:Money,’__[’q.Coin,’a.Item]]],

’#1:Marking <- ’%3:Money ;

’M:Money <- ’__[’$.Coin,’%3:Money],

’State,

rl ’<_>[’__[’$.Coin,’#1:Marking]]

=> ’<_>[’__[’#1:Marking,’__[’q.Coin,’a.Item]]]

[label(’buy-a)] . }

{ ’<_>[’__[’c.Item,’__[’a.Item,’#6:Money]]],

’#4:Marking <- ’__[’a.Item,’#6:Money] ;

’%3:Money <- ’__[’q.Coin,’q.Coin,’q.Coin,’#6:Money],

’State,

rl ’<_>[’__[’$.Coin,’#4:Marking]]

=> ’<_>[’__[’c.Item,’#4:Marking]]

[label(’buy-c)] .}

metaNarrowSearchPath(

axCohComplete(upModule(’NARROWING-VENDING-MACHINE, false)),

’<_>[’M:Money],

’<_>[’__[’a.Item, ’c.Item]],

none, ’*, unbounded, 1, unbounded) .

result TraceNarrow:

{ ’<_>[’__[’%3:Money,’__[’q.Coin,’a.Item]]],

’#1:Marking <- ’%3:Money ;

’M:Money <- ’__[’$.Coin,’%3:Money],

’State,

rl ’<_>[’__[’$.Coin,’#1:Marking]]

=> ’<_>[’__[’#1:Marking,’__[’q.Coin,’a.Item]]]

[label(’buy-a)] . }

{ ’<_>[’__[’c.Item,’__[’a.Item,’#6:Money]]],

’#4:Marking <- ’__[’a.Item,’#6:Money] ;

’%3:Money <- ’__[’q.Coin,’q.Coin,’q.Coin,’#6:Money],

’State,

rl ’<_>[’__[’$.Coin,’#4:Marking]]

=> ’<_>[’__[’c.Item,’#4:Marking]]

[label(’buy-c)] .}

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.

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:

op metaParamodulationSearch :

Module Term Term Substitution Qid Bound Bound Bound -> ResultTripleSet .

Module Term Term Substitution Qid Bound Bound Bound -> ResultTripleSet .

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

mod NARROWING-VM-NOTOP 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] .

subsort Marking < State .

ops $ q : -> Coin .

ops a c : -> Item .

var M : Marking .

rl [buy-c] : $ => c .

rl [buy-a] : $ => a q .

eq [change]: q q q q = $ [variant] .

endm

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] .

subsort Marking < State .

ops $ q : -> Coin .

ops a c : -> Item .

var M : Marking .

rl [buy-c] : $ => c .

rl [buy-a] : $ => a q .

eq [change]: q q q q = $ [variant] .

endm

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

Maude> red in FULL-MAUDE :

metaParamodulationSearch(

axCohComplete(upModule(’NARROWING-VM-NOTOP, false)),

’M:Money,

’__[’a.Item, ’c.Item],

none, ’*, unbounded, 1, unbounded) .

result ResultTriple:

{’__[’a.Item,’c.Item],

’Marking,

’#1:‘[State‘] <- ’__[’q.Coin,’q.Coin,’q.Coin] ;

’#4:‘[State‘] <- ’a.Item ;

’#6:Money <- ’empty.Money ;

’%3:Money <- ’__[’q.Coin,’q.Coin,’q.Coin] ;

’M:Money <- ’__[’$.Coin,’q.Coin,’q.Coin,’q.Coin]}

metaParamodulationSearch(

axCohComplete(upModule(’NARROWING-VM-NOTOP, false)),

’M:Money,

’__[’a.Item, ’c.Item],

none, ’*, unbounded, 1, unbounded) .

result ResultTriple:

{’__[’a.Item,’c.Item],

’Marking,

’#1:‘[State‘] <- ’__[’q.Coin,’q.Coin,’q.Coin] ;

’#4:‘[State‘] <- ’a.Item ;

’#6:Money <- ’empty.Money ;

’%3:Money <- ’__[’q.Coin,’q.Coin,’q.Coin] ;

’M:Money <- ’__[’$.Coin,’q.Coin,’q.Coin,’q.Coin]}

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