Rule rewriting is a highly nondeterministic process: at every step, many rules could be applied at various positions. A finer control on rule application is sometimes desirable, and even required, when rules are not terminating or not convergent. Maude programmers already had resources to restrain rewriting, from adding more information to the data representation to applying rules explicitly at the metalevel, as described in Section 17.7. However, these methods make specifications harder to understand and programming at the metalevel is a cumbersome task for novice users. For these reasons, a strategy language has been proposed [98, 61, 100] as a specification layer above those of equations and rules. This provides a cleaner way to control the rewriting process respecting the separation of concerns principle. That is, the rewrite theory is not modified in any way: strategies provide an additional specification level above that of rules, so that the same system module may be executed according to different strategy specifications. The design of Maude’s strategy language has been influenced, among others, by ELAN [13] and Stratego [18].
Of course, the most basic action of the strategy language is rule application, which is invoked by mentioning the rule label. More complex strategies, involving several, or unboundedly many, rule applications, can be built by means of various strategy combinators. The language is described in detail in Section 10.1. Moreover, strategy expressions can be given a name to be later invoked with arguments, even recursively. Strategy modules, the modular way in which strategies are declared, are explained in Section 10.2. Like functional and system modules, strategy modules can be parameterized, with specific features that are described in Section 10.3. A discussion about the strategy search commands follows in Section 10.4. Some other aspects are covered in specific chapters, like the metarepresentation of strategies in Section 17.3 and how strategy executions can be traced and debugged in Section 20.
Let us start with a simple example. The HANOI module below specifies the Tower of Hanoi puzzle, invented by the French mathematician Éduard Lucas in 1883 [93]. His story tells about an Asian temple where there are three diamond posts. The first one is surrounded by sixtyfour golden disks of increasing size from the top to the bottom. The monks are committed to move them from one post to another respecting two rules: only a disk can be moved at a time, and they can only be laid either on a bigger disk or on the floor. Their objective is to move all of them to the third post, and then the world will end.
mod HANOI is
protecting NATLIST .
sorts Post Hanoi Game .
subsort Post < Hanoi .
op (_) [_] : Nat NatList > Post [ctor] .
op empty : > Hanoi [ctor] .
op __ : Hanoi Hanoi > Hanoi [ctor assoc comm id: empty] .
vars S T D1 D2 N : Nat .
vars L1 L2 : NatList .
vars H H’ : Hanoi .
crl [move] : (S) [L1 D1] (T) [L2 D2] => (S) [L1] (T) [L2 D2 D1] if D2 > D1 .
rl [move] : (S) [L1 D1] (T) [nil] => (S) [L1] (T) [D1] .
endm
It rewrites the term according to the given strategy expression and prints all the results. Since strategies need not be deterministic, many results may be obtained. Like in the standard rewriting commands, we can optionally specify the module where to rewrite after in, and a bound n on the number of solutions to be shown just after the command keyword, which can be shortened to srew. For example,
Maude> srew [3] in HANOI : (0)[3 2 1] (1)[nil] (2)[nil] using move .
Solution 1
rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second)
result Hanoi: (0)[3 2] (1)[1] (2)[nil]
Solution 2
rewrites: 2 in 0ms cpu (1ms real) (~ rewrites/second)
result Hanoi: (0)[3 2] (1)[nil] (2)[1]
No more solutions.
rewrites: 2 in 0ms cpu (1ms real) (~ rewrites/second)
As we have anticipated, rule application is the essential building block of the strategy language. Besides the rule label, further restrictions can be imposed. Its most general syntax has the form:
Between square brackets, we can optionally set an initial ground substitution for the variables X_{1},…,X_{n} appearing in the rule. And when invoking a conditional rule with rewriting conditions we must provide between curly brackets the strategies α_{1},…,α_{m} to control rewriting each of them. Only rules with exactly m condition fragments will be tried, so all rewriting fragments must be given a strategy. For example, we can select to which Hanoi tower the disk is moved by giving the command:
Maude> srew (0)[3 2 1] (1)[nil] (2)[nil] using move[T < 2] .
Solution 1
rewrites: 1
result Hanoi: (0)[3 2] (1)[nil] (2)[1]
No more solutions.
rewrites: 1
An additional combinator all triggers a single rewriting step with all rules available in the module, even those which are not given a label, but excluding those marked with nonexec, external objects and implicit rules. Rewriting condition fragments are executed like in the usual rewriting engine, without any restriction. To illustrate all and how strategies can control rule conditions, the following module HANOICOUNT introduces a pair operator of Game for keeping track of the number of moves used to reach a solution.
mod HANOICOUNT is
protecting HANOI .
op <_,_> : Hanoi Nat > Game [ctor] .
vars H H’ : Hanoi .
var N : Nat .
crl [step] : < H, N > => < H’, s N > if H => H’ .
rl [cancel] : N => 0 [nonexec] .
rl [inc] : N => s N [nonexec] .
endm
Maude> srew < (0)[3 2 1] (1)[nil] (2)[nil], 0 > using step{all} .
Solution 1
result Game: < (0)[3 2] (1)[1] (2)[nil],1 >
Solution 2
result Game: < (0)[3 2] (1)[nil] (2)[1],1 >
No more solutions
By default, rule applications are tried anywhere within the subject term. However, they can be limited to the topmost position using the top restriction. For example, if we apply the cancel rule, which rewrites any natural number^{1} to zero, we obtain multiple solutions:
Maude> srew 1 using cancel .
Solution 1
result Zero: 0
Solution 2
result NzNat: 1
No more solutions.
The other basic component of the language are the tests. They can be used for testing a condition on the subject term. Their syntax has the form:
where P is a pattern and C is an equational condition, as described in Section 4.3. Their syntax and behavior are similar to those of the match commands in Section 4.9: the suchthat clause can be omitted if no condition is imposed, and the starting keyword indicates where the matching is done: on top (match), on any fragment of the flattened top modulo axioms (xmatch), or anywhere within the subject term (amatch). The condition may refer to variables in the pattern, whose value will be obtained from the matching. On a successful match and condition check, the result is the initial term. Otherwise, the test does not provide any solution. For example, we can check whether the towers of Hanoi puzzle is solved with tests:
Maude> srew (0)[nil] (1)[nil] (2)[3 2 1] using match (N)[3 2 1] H s.t. N =/= 0 .
Solution 1
result Hanoi: (0)[nil] (1)[nil] (2)[3 2 1]
No more solutions.
Maude> srew (0)[nil] (1)[nil] (2)[3 2 1] using xmatch (0)[nil] (2)[3 2 1] .
Solution 1
result Hanoi: (0)[nil] (1)[nil] (2)[3 2 1]
No more solutions.
Maude> srew in HANOI : (0)[nil] (1)[nil] (2)[3 2 1] using amatch 3 L1 1 .
Solution 1
result Hanoi: (0)[nil] (1)[nil] (2)[3 2 1]
No more solutions.
Strategy ζ  Results ⟦ζ⟧(𝜃,t)  






idle  {t}  



fail  ∅  



rlabel[ρ]  { t′∈ T_{Σ}∣t →_{ρ(l)→ρ(r)}t′ for any l →^{rlabel}r ∈ R }  



α;β  ⋃ _{t′∈⟦α⟧(𝜃,t)}⟦β⟧(𝜃,t′)  



αβ  ⟦α⟧(𝜃,t) ∪⟦β⟧(𝜃,t)  



α*  ⋃ _{n=0}^{∞}⟦α⟧^{n}(𝜃,t)  



match P s.t. C  



α ? β : γ  









slabel(t_{1},…,t_{n})  ⋃ _{(lhs,δ,C)∈Defs} ⋃ _{σ∈matches(slabel(t1,…,tn),lhs,C,id)} ⟦δ⟧(σ,t) 
To control the flow of rule execution some combinators are defined. Let α, β and γ represent arbitrary strategy expressions.
Maude> srew (0)[3 2 1] (1)[nil] (2)[nil] using move ; move .
Solution 1
result Hanoi: (0)[3 2 1] (1)[nil] (2)[nil]
Solution 2
result Hanoi: (0)[3] (1)[1] (2)[2]
Solution 3
result Hanoi: (0)[3 2] (1)[nil] (2)[1]
Solution 4
result Hanoi: (0)[3] (1)[2] (2)[1]
Solution 5
result Hanoi: (0)[3 2] (1)[1] (2)[nil]
No more solutions.
Maude> srew (0)[3 2 1] using idle .
Solution 1
result Post: (0)[3 2 1]
No more solutions.
Maude> srew (0)[3 2 1] using fail .
No solution.
For example, we can instruct the monks to move disks to the first and second tower only if no disk can be moved to the target post. In this way, we obtain only 21 results out of 27.
In the example above, we are giving precedence to one strategy over another, so that the second is only executed if the first fails. This is a common control pattern, and so it is defined as a derived operator with its own name, along with some other usual constructions:
The orelse combinator is defined by
As shown in the example above, it executes β only if α has failed.
It fails when α succeeds, and succeeds as an idle when α fails.
applies α until it cannot be further applied.
The try strategy is defined by try(α) ≡ α ? idle : idle. It applies α, but if it fails, it returns the initial state.
The test strategy, defined by test(α) ≡not(not(α)), fails whenever α fails, but when α succeeds, it returns the initial term instead of its results.
The match and rewrite operator matchrew restricts the application of a strategy to a specific subterm of the subject term. Its syntax is
where P is a pattern with variables X_{1},…,X_{n} among others, and C is an optional equational condition. The using clauses associate variables in the pattern, which are matched by subterms of the matched term, with strategies that will be used to rewrite them. These variables must be distinct and must appear in the pattern. As in the case of tests, there are three flavors for this operator, depending on the type of matching: matchrew, xmatchrew, and amatchrew.The semantics of this operator is illustrated in Figure 10.1. All matches of the pattern in the subject term are tried, checking the condition if any. If none succeeds, the strategy fails. Otherwise, for each match of the main pattern the subterms matching each X_{i} are extracted, rewritten according to α_{i}, and their solutions are put in place of the original subterm. The rewriting of the subterms happens in parallel, in the sense that the terms evolve in a completely independent and fair way. Finally, all possible combinations of the subterm results will give rise to different reassembled solutions.
Another advantage of matchrew is that it let us obtain information about the term and use it to modify the behavior of the strategies. The scope of the variables in the pattern and the condition is extended to the substrategies α_{1},…,α_{n}, so that the values they take by matching and evaluation can be used in nested rule substitutions, strategy calls, and match and matchrew operators. Conversely, when these variables are bound by outer constructs, they keep their values and matching is done against a partially instantiated pattern. When a variable in the condition is not bound either by the outer context or by the matching, the strategy will be unusable and a warning will be shown by the interpreter.
For example, instead of using the step rule to count the moves in the Tower of Hanoi, we could have used a matchrew and the increment rule inc. This is written:
Maude> srew [1] in HANOICOUNT : < (0)[3 2 1] (1) [nil] (2)[nil], 0 >
using (matchrew < H, N > by H using move, N using top(inc)) * ;
amatch (2)[3 2 1] .
Solution 1
rewrites: 523 in 56ms cpu (56ms real) (9339 rewrites/second)
result Game: < (0)[nil] (1)[nil] (2)[3 2 1], 7 >
Maude> srew 1 using inc .
Solution 1
rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second)
result NzNat: 2
No more solutions.
rewrites: 2 in 0ms cpu (0ms real) (~ rewrites/second)
Strategies are nondeterministic due to the different possible matches of the rules and the subterm rewriting operator, disjunction, iteration, etc. The various rewriting paths that these alternatives make possible are explored almost simultaneously by the strategic search engine. Sometimes, the different options lead to the same result or, the results being different, it may not matter which of them is selected. For efficiency purposes, the one combinator is introduced to execute its argument strategy and return only one of its solutions, namely the first one found. If the strategy does not produce any solutions, neither does one.
Maude> srew (0)[3 2 1] (1)[nil] (2)[nil] using one(move * ; amatch (2)[3 2 1]) .
Solution 1
rewrites: 121
result Hanoi: (0)[nil] (1)[nil] (2)[3 2 1]
No more solutions.
rewrites: 121
Maude> srew (0)[3 2 1] (1)[nil] (2)[nil] using move * ; amatch (2)[3 2 1] .
Solution 1
rewrites: 121
result Hanoi: (0)[nil] (1)[nil] (2)[3 2 1]
No more solutions.
rewrites: 150
Maude> srew (0)[3 2 1] (1)[nil] (2)[nil] using one(move) * .
Solution 1
result Hanoi: (0)[3 2 1] (1)[nil] (2)[nil]
Solution 2
result Hanoi: (0)[3 2] (1)[1] (2)[nil]
No more solutions.
Strategies with their own name and taking parameters can be defined in strategy modules, which will be explained in Section 10.2. These named strategies can be called as a strategy expression with a typical prefix operator syntax: a strategy identifier followed by a commaseparated list of arguments between parentheses. When the strategy does not take any arguments and there is no rule with the same name, the parentheses can be omitted. Suppose we already have defined a strategy moveAll to move disks between certain posts indicated by its arguments, with its third argument being the number of disks to be moved. It can be applied to an initial state like this:
Maude> srew (0)[3 2 1] (1)[nil] (2)[nil] using moveAll(0, 2, 3) .
Solution 1
rewrites: 24 in 4ms cpu (2ms real) (6000 rewrites/second)
result Hanoi: (0)[nil] (1)[nil] (2)[3 2 1]
No more solutions.
rewrites: 24 in 4ms cpu (2ms real) (6000 rewrites/second)
Strategy modules let the user give name to strategy expressions. Named strategies facilitate the use and description of complex strategies, and they extend the expressiveness of the language by means of recursive and mutually recursive strategies. As for functional and system modules, a strategy module is declared in Maude using the keywords
A typical strategy module would import the system module it will control, declare some strategies, and define them by means of strategy definitions. All statements and declarations that were available in functional and system modules can also be included in strategy modules, but we encourage to avoid them as much as possible to emphasize a clean separation between the rewriting theory and the strategies that control it.For example, the following strategy module HANOISOLVE defines the recursive strategy moveAll that we have used in Section 10.1.4 to illustrate strategy calls and solve the puzzle.
smod HANOISOLVE is
protecting HANOI .
protecting HANOIAUX .
strat moveAll : Nat Nat Nat @ Hanoi .
vars S T C M : Nat .
sd moveAll(S, S, C) := idle .
sd moveAll(S, T, 0) := idle .
sd moveAll(S, T, s(C)) := moveAll(S, third(S, T), C) ;
move[S < S, T < T] ;
moveAll(third(S, T), T, C) .
endsm
fmod HANOIAUX is
protecting SET{Nat} .
op third : Nat Nat ~> Nat .
vars N M K : Nat .
ceq third(N, M) = K if N, M, K := 0, 1, 2 .
endfm
Strategy names can be overloaded, i.e., strategies can be defined with the same name but may have different arities and argument types. Like operators, strategies are defined at the kind level. Homonymous strategies with the same arity and such that for each argument the corresponding sorts have the same kind are considered the same. In practice, the concrete sorts of the strategy signature do not have any effect and should be considered as a declaration of intent. Repeated declarations of the exact same strategy twice (with the same name and argument kinds) will generate a warning. For example, when processing the module
the interpreter will issue the warning:
Warning: <standard input>, line 5 (smod STRATS): strategy declaration
strat repeat : Int @ Nat . conflicts with
strat repeat : Nat @ Nat . from <standard input>, line 4 (smod STRATS).
Without a corresponding definition, named strategies behave like fail. Definition statements should be provided to properly define each named strategy according to the syntax:
The lefthand side of a definition is a strategy call, as seen in the previous section, probably containing variables, which can be used in the righthand side. In fact, all variables in the strategy expression, except variables in matching patterns, must appear in the lefthand side. Like equations and rules, strategy definitions may be conditional: The condition of a strategy definition is an equational one, as described in Section 4.3, i.e., rewriting conditions t_{1} => t_{2} are not allowed. The attributes metadata, label and print (see Section 4.5) can be attached to sd and csd definitions. When a strategy is invoked, all available definitions for the name are tried, and all those whose lefthand side matches the calling arguments are executed. Moreover, conditions may generate different variable assignments, in which case the strategy will be applied with each one of them. For example, we could have given the third definition of moveAll in HANOISOLVE above as
csd moveAll(S, T, s(C)) := moveAll(S, third(S, T), C) ;
move[S < S, T < T] ;
moveAll(third(S, T), T, C) if S =/= T .
To conclude this section, let us show another example: the insertionsort algorithm implemented by means of strategies. The underlying array is represented as a set of pairs containing both a position and a value. It is assumed that there is a single entry for each position between one and the length of the array. A rule swap is defined to swap the values between two entries.
mod SWAPPING{X :: DEFAULT} is
protecting ARRAY{Nat, X} .
vars I J : Nat .
vars V W : X$Elt .
var AR : Array{Nat, X} .
rl [swap] : J > V ; I > W => J > W ; I > V .
op maxIndex : Array{Nat, X} ~> Nat .
eq maxIndex(empty) = 0 .
eq maxIndex(I > V ; AR) = if maxIndex(AR) < I then I else maxIndex(AR) fi .
endm
smod INSERTIONSORT{X :: STRICTTOTALORDER + DEFAULT} is
protecting SWAPPING{DEFAULT+}{X} * (
sort Array{Nat, DEFAULT+}{X} to NatArray{X}
) .
strat swap : Nat Nat @ NatArray{X} .
strats insert insort : Nat @ NatArray{X} .
vars X Y J I : Nat .
vars V W : X$Elt .
var AR : NatArray{X} .
sd insort(Y) := try(match AR s.t. Y <= maxIndex(AR) ;
insert(Y) ;
insort(Y + 1)) .
sd insert(1) := idle [label basecase] .
csd insert(s(X)) := try(xmatch X > V ; s(X) > W s.t. W < V ;
swap(X, s(X)) ;
insert(X))
if X > 0 [label recursivecase] .
sd swap(X, Y) := swap[J < X, I < Y] .
endsm
Then, we can sort any array using insort with the following srewrite command:
Maude> srewrite 1 > 8 ; 2 > 3 ; 3 > 15 ; 4 > 5 ; 5 > 2 using insort(2) .
Solution 1
rewrites: 116 in 0ms cpu (0ms real) (~ rewrites/second)
result NatArray{Int<0}: 1 > 2 ; 2 > 3 ; 3 > 5 ; 4 > 8 ; 5 > 15
No more solutions.
rewrites: 116 in 0ms cpu (1ms real) (~ rewrites/second)
Strategy modules can be seen as an additional layer of specification over functional and system modules, which are not allowed to import strategy modules. Instead, strategy modules can import functional, system, or strategy modules using the protecting, extending, and including modes.
The semantic requirements for each inclusion mode are described in Section 6.1 for functional and system modules. Similar requirements apply to strategies when importing strategy modules. A protecting extension M of a strategy module M′ should not alter the rewriting paths permitted by each strategy declared in M′. The declaration and definition of new strategies in the importing module does not affect the semantics of the strategies declared in the imported module, but adding new definitions for the imported strategies may change their behavior. If new rewriting paths are added to the imported strategies, but those of the imported module are preserved, the extending mode should be used. In any other case, the including mode is the right choice.
Let us illustrate the importation modes with a simple example. The following strategy module SMODIMPORTEXAMPLE declares two strategies st1 and st2. Since st1 is not given any definition, no rewriting is possible using it, and thus st1 is equivalent to fail. On the other hand, the definition of st2 describes all rewriting paths of the form q →’z for every quoted identifier q.
mod SMODIMPORTEXAMPLE0 is
protecting QID .
rl [ab] : ’a => ’b .
rl [bc] : ’b => ’c .
rl [zz] : Q:Qid => ’z .
endm
smod SMODIMPORTEXAMPLE is
protecting SMODIMPORTEXAMPLE0 .
strats st1 st2 @ Qid .
sd st2 := st1 ? bc : zz .
endsm
Maude> srew in SMODIMPORTEXAMPLE : ’a using st2 .
Solution 1
rewrites: 1
result Qid: ’z
No more solutions.
rewrites: 1
Maude> srew in SMODIMPORTEXAMPLE’’ : ’a using st2 .
Solution 1
rewrites: 2
result Qid: ’c
No more solutions.
rewrites: 2
Finally, the language of module renamings (see Section 6.2.2) is extended with strategy renamings. Like for regular operators, strat name to newName renames all strategies whose name is name to newName. To rename only a specific instance of an overloaded strategy name, its arity and subject sort can be made explicit with strat name : s_{1}…s_{n} @ s to newName.
Strategy modules can be parameterized like any other module in Maude, by means of theories and views, as explained in Section 6.3. A parameterized strategy module is a usual strategy module that takes a set of formal parameters, bound to some theories:
These theories can be functional or system theories, or also strategy theories. A strategy theory specifies the signature of the strategies that a concrete strategy module parameter must provide and the requirements that these actual strategies must satisfy. How a particular strategy module meets the requirements of a strategy theory is specified by means of a view with strategy bindings, which will be described soon, and then views are used to instantiate parameterized modules with actual parameters. Strategy theories are introduced with the syntax: and have features entirely similar to those of strategy modules. They can:import other theories in including mode,
import modules of any kind,
declare strategies,
provide strategy definitions, and
include other declarations and statements that functional and system theories admit.
The simplest strategy theory STRIV declares a single strategy without parameters:
The subject sort Elt of the strategy st is imported from the functional theory TRIV. Strategy theories can never be used to parameterize functional or system modules.Given a strategy module that meets the requirements of a strategy theory, we should specify how they are actually met by using a view. The repertoire of mappings that can appear in a view (see Section 6.3.2) has been extended with additional syntax for strategy bindings:
For example, consider the following strategy theory FOO and strategy module BAR:
sth STHEORY is
including TRIV .
protecting NAT .
strat foo : Elt @ Elt .
strat foo : Elt Nat @ Elt .
endsth
smod SMODULE is
protecting STRING .
protecting NAT .
strat bar : String @ String .
strat bar : String Nat @ String .
endsm
Finally, and as usual, modules are instantiated with views using the syntax
Let us illustrate how parameterized strategy modules are instantiated by strategy views with an example. The following parameterized strategy module BACKTRACKING is a backtracking problem solver: the generic algorithm is specified as a strategy solve depending on some formal declarations.
smod BACKTRACKING{X :: BTSTRAT} is
strat solve @ X$State .
var S : X$State .
sd solve := (match S s.t. isSolution(S)) ?
idle : (expand ; solve) .
endsm
mod QUEENS is
protecting LIST{Nat} .
protecting SET{Nat} .
op isOk : List{Nat} > Bool .
op ok : List{Nat} Nat Nat > Bool .
op isSolution : List{Nat} > Bool .
vars N M Diff : Nat .
var L : List{Nat} .
var S : Set{Nat} .
eq isOk(L N) = ok(L, N, 1) .
eq ok(nil, M, Diff) = true .
ceq ok(L N, M, Diff) = ok(L, M, Diff + 1)
if N =/= M /\ N =/= M + Diff /\ M =/= N + Diff .
eq isSolution(L) = size(L) == 8 .
crl [next] : L => L N if N, S := 1, 2, 3, 4, 5, 6, 7, 8 .
endm
smod QUEENSSTRAT is
protecting QUEENS .
strat expand @ List{Nat} .
var L : List{Nat} .
sd expand := top(next) ; match L s.t. isOk(L) .
endsm
view QueensBT from BTSTRAT to QUEENSSTRAT is
sort State to List{Nat} .
strat expand to expand .
endv
Maude> srew [2] nil using solve .
srewrite [2] in BTQUEENS : nil using solve .
Solution 1
rewrites: 285984 in 238ms cpu (238ms real) (1200211 rewrites/second)
result NeList{Nat}: 1 5 8 6 3 7 2 4
Solution 2
rewrites: 285984 in 238ms cpu (238ms real) (1200211 rewrites/second)
result NeList{Nat}: 1 6 8 3 7 4 2 5
Typically, views will be defined from a strategy theory to a strategy module or theory, but other combinations are possible. In general, strategic and nonstrategic theories and modules can be combined with freedom in views.
Otherwise, all the details about module instantiation in Section 6.3.4 are applicable to the strategy level as well. As a simple example, we can write a view from the functional theory TRIV to the strategy theory STRIV and viceversa as follows:
view StrivIdle from STRIV to TRIV is
sort Elt to Elt .
strat st to expr idle .
endv
view STRIV from TRIV to STRIV is
sort Elt to Elt .
endv
Moreover, we could have defined a view from the strategy theory BTSTRAT directly to the functional module QUEENS by binding the formal strategy expand to the actual inline definition of the expand strategy we already use in the strategy module QUEENSSTRAT. In this way, we do not need to define or use the QUEENSSTRAT strategy module.
view QueensBT2 from BTSTRAT to QUEENS is
sort State to List{Nat} .
var L : State .
strat expand to expr top(next) ; match L s.t. isOk(L) .
endv
Although strategies control and restrict rewriting, they do not make the process deterministic. A strategy may allow multiple rewriting paths, produced by alternative local decisions that may appear during its execution. The rewrite and frewrite commands eliminate this nondeterminism by each choosing a specific fixed strategy, as explained in Sections 5.4.1 and 5.4.2. Instead, the search command explores all the possible rule applications looking for a term matching a given target. The srewrite command agrees with search in the exhaustive exploration of the alternatives, looking, in this case, for strategy solutions. However, the srewrite search is not conducted on the complete rewriting tree of search, but in a subtree pruned by the effect of the strategy. How this tree is explored has implications for the command’s output and its performance.
The srewrite command explores the rewriting graph following a fair policy which ensures that all solutions reachable in a finite number of steps are eventually found, unless the interpreter runs out of memory. Without being a breadthfirst search, multiple alternative paths are explored in parallel. This can be observed in the nqueens problem presented in Section 10.3 , and in the particular example we showed:
Maude> srew [2] nil using solve .
Solution 1
rewrites: 285984 in 249ms cpu (248ms real) (1147935 rewrites/second)
result NeList{Nat}: 1 5 8 6 3 7 2 4
Solution 2
rewrites: 285984 in 249ms cpu (249ms real) (1147935 rewrites/second)
result NeList{Nat}: 1 6 8 3 7 4 2 5
An alternative rewriting command dsrewrite (depth strategic rewrite) explores the strategy rewriting graph in depth. Its syntax coincides with that of the srewrite command except for the starting keyword, which can be abbreviated to dsrew.
Using this command in the previous example, we can observe some differences. The first solution is obtained sooner and some rewrites before the second. In absolute terms, both solutions are shown earlier and using fewer rewrites. The memory usage is reduced too.
Maude> dsrew [2] nil using solve .
dsrewrite [2] in BTQUEENS : nil using solve .
Solution 1
rewrites: 15602 in 16ms cpu (17ms real) (942092 rewrites/second)
result NeList{Nat}: 1 5 8 6 3 7 2 4
Solution 2
rewrites: 20339 in 19ms cpu (21ms real) (1022728 rewrites/second)
result NeList{Nat}: 1 6 8 3 7 4 2 5
Rule applications and matchrew matches are issued as in the rewrite and match commands, i.e., from outer to inner positions and from left to right. Rules are selected in their syntactical order within the module.
In an alternative αβ, the successors of α appear before the successors of β.
In an iteration, leaving precedes continuing with another iteration.
Strategy definitions are selected in the order they appear in the module. If the parameters match in different ways, these strategy executions are generated as in the match command.
Rule and strategy condition fragments are processed from left to right and matches are generated as before. Rewriting condition fragments solutions are depthfirst searched using these precedences.