System modules in Maude are rewrite theories that do not need to be Church-Rosser and terminating. We need to have good ways of controlling the rewriting inference process--which in principle could go in many undesired directions--by means of adequate strategies. In Maude, thanks to its reflective capabilities, strategies can be made internal to the system. That is, they can be defined by rewrite rules in a normal module in Maude, and can be reasoned about as with rules in any other module.
In fact, there is great freedom for defining many different strategy languages inside Maude. This can be done in a completely user-definable way, so that users are not limited by a fixed and closed strategy language. The idea is to use the operations meta-reduce, meta-apply, and meta-rewrite as basic strategy expressions, and then to extend the module META-LEVEL by additional strategy expressions and corresponding semantic rules. Here we follow the methodology for defining and proving correct internal strategy languages for reflective logics introduced in [15, 10].
To illustrate this idea, let us reconsider the module SORTING for sorting vectors of integers introduced in Section 2.2. We will use this module as a running example to explain the way in which the application of rules can be controlled.
As mentioned before, strategy languages can be defined within Maude in user-definable extensions of the module META-LEVEL. As an example, we introduce the following module STRATEGY. We first introduce the basic syntax; the module's equations are then discussed and illustrated with examples in the rest of the section.
fmod STRATEGY is
protecting META-LEVEL .
sorts MetaVar Binding BindingList
Strategy StrategyExpression .
subsort MetaVar < Term .
ops I J : -> MetaVar .
op binding : MetaVar Term -> Binding .
op nilBindingList : -> BindingList .
op bindingList : Binding BindingList -> BindingList .
op rewInWith :
Module Term BindingList Strategy -> StrategyExpression .
op set : MetaVar Term -> Strategy .
op rewInWithAux :
StrategyExpression Strategy -> StrategyExpression .
op idle : -> Strategy .
op failure : -> StrategyExpression .
op and : Strategy Strategy -> Strategy .
op apply : Qid -> Strategy .
op applyWithSubst : Qid Substitution -> Strategy .
op iterate : Strategy -> Strategy .
op while : Term Strategy -> Strategy .
op orelse : Strategy Strategy -> Strategy .
op extTerm : ResultPair -> Term .
op extSubst : ResultPair -> Substitution .
op update : BindingList Binding -> BindingList .
op applyBindingListSubst :
Module Substitution BindingList -> Substitution .
op substituteMetaVars : TermList BindingList -> TermList .
op SORTING : -> Module .
var M : Module .
vars V V' F G L : Qid .
vars T T' : Term .
var TL : TermList .
var SB : Substitution .
vars B B' : Binding .
vars BL BL' : BindingList .
var MV MV' : MetaVar .
vars ST ST' : Strategy .
eq SORTING
= (mod 'SORTING is
including 'MACHINE-INT .
sorts 'Pair ; 'PairSet .
subsort 'Pair < 'PairSet .
op '<_;_> : 'MachineInt 'MachineInt -> 'Pair
[none] .
op 'empty : nil -> 'PairSet [none] .
op '__ : 'PairSet 'PairSet -> 'PairSet
[assoc comm id({'empty}'PairSet)] .
var 'I : 'MachineInt .
var 'J : 'MachineInt .
var 'X : 'MachineInt .
var 'Y : 'MachineInt .
none
none
crl ['sort]: '__['<_;_>['J, 'X], '<_;_>['I, 'Y]]
=> '__['<_;_>['J, 'Y], '<_;_>['I, 'X]]
if '_and_['_<_['J, 'I], '_>_['X, 'Y]]
= {'true}'Bool .
endm) .
Before we explain some of the strategies that can be defined using the strategy language introduced in STRATEGY, note that the default strategy of the Maude interpreter for system modules can be easily (and efficiently) called using the built-in function meta-rewrite introduced in Section 2.5.5.
Maude> rew meta-rewrite(SORTING,
'__['<_;_>[{'1}'MachineInt, {'3}'MachineInt],
'<_;_>[{'2}'MachineInt, {'2}'MachineInt],
'<_;_>[{'3}'MachineInt, {'1}'MachineInt]],
0) .
result Term: '__['<_;_>[{'1}'NzMachineInt,{'1}'NzMachineInt],
'<_;_>[{'2}'NzMachineInt,{'2}'NzMachineInt],
'<_;_>[{'3}'NzMachineInt,{'3}'NzMachineInt]]
Maude> rew meta-rewrite(SORTING,
'__['<_;_>[{'1}'MachineInt, {'3}'MachineInt],
'<_;_>[{'2}'MachineInt, {'2}'MachineInt],
'<_;_>[{'3}'MachineInt, {'1}'MachineInt]],
2) .
result Term: '__['<_;_>[{'1}'NzMachineInt,{'1}'NzMachineInt],
'<_;_>[{'2}'NzMachineInt,{'3}'NzMachineInt],
'<_;_>[{'3}'NzMachineInt,{'2}'NzMachineInt]]
In the module STRATEGY the function rewInWith computes strategy expressions. The first two arguments of rewInWith are the metarepresentations of a module T and a term t in META-LEVEL. The fourth argument is the strategy S we want to compute, and the third argument is used to store information that may be relevant for S. Our definition of rewInWith is such that, as the computation of a given strategy expression proceeds, t gets rewritten by controlled application of rules in T, the information stored in the third argument may be updated, and the strategy S is rewritten into the remaining strategy to be computed. In case of termination, this is the idle strategy and we are done. The strategy expression failure is returned when a requested strategy cannot be carried out.
A basic strategy we can express is the application of a rule once at the top of a term (if the top operator has attributes containing axioms such as associativity or associativity and commutativity, matching is done modulo those axioms) with the first possible match found when no constraints are placed on the matching substitution. For this basic strategy, we introduce in our signature the constructor apply, whose only argument is an identifier corresponding to the rule label to be applied, and we define the value of rewInWith for this strategy, using the built-in operation meta-apply, as follows:
eq rewInWith(M, T, BL, apply(L))
= if meta-apply(M, T, L, none, 0)
== {error*, none}
then failure
else rewInWith(M,
extTerm(meta-apply(M, T, L, none, 0)),
BL, idle)
fi .
The operations extTerm and extSubst are selectors extracting the first and second component, respectively, from a pair constructed with {_,_}.
eq extSubst({T, SB}) = SB .
eq extTerm({T, SB}) = T .
Maude> rew rewInWith(SORTING,
'__['<_;_>[{'1}'MachineInt, {'3}'MachineInt],
'<_;_>[{'2}'MachineInt, {'2}'MachineInt],
'<_;_>[{'3}'MachineInt, {'1}'MachineInt]],
nilBindingList,
apply('sort)).
result StrategyExpression:
rewInWith(SORTING 16,
'__['<_;_>[{'1}'NzMachineInt,{'2}'NzMachineInt],
'<_;_>[{'2}'NzMachineInt,{'3}'NzMachineInt],
'<_;_>[{'3}'NzMachineInt,{'1}'NzMachineInt]],
nilBindingList,
idle)
The information relevant for the computation of a strategy expression is recorded as a list of bindings of values to metavariables, where the values are of sort Term (that is, they are representations of terms) and metavariables are introduced by the user as constants of sort MetaVar. The sort MetaVar is declared as a subsort of the sort Term, so that in any expression in which the representation of a term t can appear, a metavariable--to which the representation of t may be bound--can appear as well.
The computation of the strategy set updates the recorded information. This is done by the function update. Notice that the terms whose representations are bound to metavariables are kept in fully reduced form, using the built-in operation meta-reduce. The representation of the term set to a metavariable may itself contain metavariables, which must be substituted by the representations of the terms they are bound to in the list of bindings present before the updating. This is done by the function substituteMetaVars. Recall that the default operational semantics for functional modules, and therefore for the function meta-reduce, is eager (i.e., bottom up or call-by-value).
eq rewInWith(M, T, BL, set(MV, T'))
= rewInWith(M, T,
update(BL,
binding(MV, meta-reduce(M,
substituteMetaVars(T', BL)))),
idle) .
eq substituteMetaVars(T, nilBindingList)
= T .
eq substituteMetaVars(MV, bindingList(binding(MV', T'), BL))
= if MV == MV' then T'
else substituteMetaVars(MV, BL) fi .
eq substituteMetaVars(F, BL)
= F .
eq substituteMetaVars({F}S, BL) = {F}S .
eq substituteMetaVars(F[TL], BL)
= F[substituteMetaVars(TL, BL)] .
eq substituteMetaVars((T, TL), BL)
= (substituteMetaVars(T, BL), substituteMetaVars(TL, BL)).
eq update(bindingList(binding(MV, T), BL), binding(MV', T'))
= if MV == MV'
then bindingList(binding(MV, T'), BL)
else bindingList(binding(MV, T),
update(BL, binding(MV', T')))
fi .
eq update(nilBindingList, B)
= bindingList(B, nilBindingList) .
We can see the computation of a set-strategy expression with the following example:
Maude> rew rewInWith(SORTING,
'__['<_;_>[{'1}'MachineInt, {'3}'MachineInt],
'<_;_>[{'2}'MachineInt, {'2}'MachineInt],
'<_;_>[{'3}'MachineInt, {'1}'MachineInt]],
nilBindingList,
set(I, {'1}'MachineInt)).
result StrategyExpression:
rewInWith(SORTING,
'__['<_;_>[{'1}'MachineInt,{'3}'MachineInt],
'<_;_>[{'2}'MachineInt,{'2}'MachineInt],
'<_;_>[{'3}'MachineInt,{'1}'MachineInt]],
bindingList(binding(I, {'1}'NzMachineInt),
nilBindingList),
idle)
The computation of the strategy applyWithSubst applies a rule partially instantiated with a set of assignments once at the top of a term (if the top operator has attributes containing axioms such as associativity or associativity and commutativity, matching is done modulo those axioms) using the first successful match consistent with the given partial substitution. The representations of the terms assigned to variables may contain metavariables that must be substituted by the representations of the terms they are bound to in the current list of bindings. This is done by the function applyBindingListSubst.
eq rewInWith(M, T, BL, applyWithSubst(L, SB))
= if meta-apply(M, T, L,
applyBindingListSubst(M, SB, BL), 0)
== {error*, none}
then failure
else rewInWith(M, extTerm(meta-apply(M, T, L,
applyBindingListSubst(M, SB, BL), 0)),
BL, idle)
fi .
eq applyBindingListSubst(M, none, BL)
= none .
eq applyBindingListSubst(M, ((V <- T); SB), BL)
= ((V <- meta-reduce(M, substituteMetaVars(T, BL)));
applyBindingListSubst(M, SB, BL)) .
Many interesting strategies are defined as concatenations of more basic strategies, or iterations of a given strategy. Frequently, the strategies must consider possible branchings in their computations, or establish conditions for further computations. To represent these cases, we extend our basic strategy language with the constructors and, orelse, iterate, and while.
The equations for the strategies and, orelse, and iterate are defined as follows.
eq rewInWith(M, T, BL, and(ST, ST'))
= if rewInWith(M, T, BL, ST) == failure
then failure
else rewInWithAux(rewInWith(M, T, BL, ST), ST')
fi .
eq rewInWith(M, T, BL, orelse(ST, ST'))
= if rewInWith(M, T, BL, ST) == failure
then rewInWith(M, T, BL, ST')
else rewInWith(M, T, BL, ST)
fi .
eq rewInWith(M, T, BL, iterate(ST))
= if rewInWith(M, T, BL, ST) == failure
then rewInWith(M, T, BL, idle)
else rewInWithAux(rewInWith(M, T, BL, ST), iterate(ST))
fi .
eq rewInWithAux(rewInWith(M, T, BL, idle), ST)
= rewInWith(M, T, BL, ST) .
Maude> rew rewInWith(SORTING,
'__['<_;_>[{'1}'MachineInt, {'3}'MachineInt],
'<_;_>[{'2}'MachineInt, {'2}'MachineInt],
'<_;_>[{'3}'MachineInt, {'1}'MachineInt]],
nilBindingList,
and(set(I, {'3}'MachineInt),
applyWithSubst('sort, ('I <- I)))) .
result StrategyExpression:
rewInWith(SORTING,
'__['<_;_>[{'1}'NzMachineInt,{'1}'NzMachineInt],
'<_;_>[{'2}'NzMachineInt,{'2}'NzMachineInt],
'<_;_>[{'3}'NzMachineInt,{'3}'NzMachineInt]],
bindingList(binding(I, {'3}'NzMachineInt),
nilBindingList),
idle)
Maude> rew rewInWith(SORTING,
'__['<_;_>[{'1}'MachineInt, {'3}'MachineInt],
'<_;_>[{'2}'MachineInt, {'2}'MachineInt],
'<_;_>[{'3}'MachineInt, {'1}'MachineInt]],
bindingList(binding(J, {'2}'MachineInt),
nilBindingList),
orelse(applyWithSubst('sort, ('J <- {'4}'MachineInt)),
applyWithSubst('sort, ('J <- J)))).
result StrategyExpression:
rewInWith(SORTING,
'__['<_;_>[{'1}'NzMachineInt,{'3}'NzMachineInt],
'<_;_>[{'2}'NzMachineInt,{'1}'NzMachineInt],
'<_;_>[{'3}'NzMachineInt,{'2}'NzMachineInt]],
bindingList(binding(J, {'2}'MachineInt),
nilBindingList),
idle)
Maude> rew rewInWith(SORTING,
'__['<_;_>[{'1}'MachineInt, {'3}'MachineInt],
'<_;_>[{'2}'MachineInt, {'2}'MachineInt],
'<_;_>[{'3}'MachineInt, {'1}'MachineInt]],
nilBindingList,
iterate(apply('sort))).
result StrategyExpression:
rewInWith(SORTING,
'__['<_;_>[{'1}'NzMachineInt,{'1}'NzMachineInt],
'<_;_>[{'2}'NzMachineInt,{'2}'NzMachineInt],
'<_;_>[{'3}'NzMachineInt,{'3}'NzMachineInt]],
nilBindingList, idle)
Finally, the strategy while makes the computation of a given strategy conditional to the satisfaction of a condition. This condition should be the representation in META-LEVEL of a term of sort Bool. As usual, the condition may contain metavariables that must be substituted by the representations of terms they are bound to in the current list of bindings. Notice that the definition of the value of rewInWith for the constructor while makes the iterative computation of the strategy contained in the second argument of while depend on the satisfaction (at the metalevel) of the condition represented in the first argument of while.
eq rewInWith(M, T, BL, while(T', ST))
= if meta-reduce(M, substituteMetaVars(T', BL))
== {'true}'Bool
then (if rewInWith(M, T, BL, ST) == failure
then rewInWith(M, T, BL, idle)
else rewInWithAux(rewInWith(M, T, BL, ST),
while(T', ST))
fi)
else rewInWith(M, T, BL, idle)
fi .
Now we can extend our basic strategy language to define, as an example, the algorithm for insertion sorting. The strategy insert(n) below can be used to sort a vector of integers of length n. The main loop in insertion sorting looks at each element of the vector of integers from the second to the n-th, and inserts it in the appropriate place among its predecessors in the vector.
We introduce two new metavariables X and Y.
op insert : MachineInt -> Strategy .
ops X Y : -> MetaVar .
var N : MachineInt .
eq insert(N)
= and(set(Y, {'2}'MachineInt),
while('_<=_[Y, {index(', N)}'MachineInt],
and(set(X, Y),
and(while('_>_[X, {'1}'MachineInt],
and(applyWithSubst('sort,
(('I <- X);
('J <- '_-_[X, {'1}'MachineInt]))),
set(X, '_-_[X, {'1}'MachineInt]))),
set(Y, '_+_[Y, {'1}'MachineInt]))))) .
Maude> rew rewInWith(SORTING,
'__['<_;_>[{'1}'MachineInt, {'10}'MachineInt],
'<_;_>[{'2}'MachineInt, {'9}'MachineInt],
'<_;_>[{'3}'MachineInt, {'8}'MachineInt],
'<_;_>[{'4}'MachineInt, {'7}'MachineInt],
'<_;_>[{'5}'MachineInt, {'6}'MachineInt],
'<_;_>[{'6}'MachineInt, {'5}'MachineInt],
'<_;_>[{'7}'MachineInt, {'4}'MachineInt],
'<_;_>[{'8}'MachineInt, {'3}'MachineInt],
'<_;_>[{'9}'MachineInt, {'2}'MachineInt],
'<_;_>[{'10}'MachineInt, {'1}'MachineInt]],
nilBindingList,
insert(10)) .
result StrategyExpression:
rewInWith(SORTING,
'__['<_;_>[{'1}'NzMachineInt,{'1}'NzMachineInt],
'<_;_>[{'2}'NzMachineInt,{'2}'NzMachineInt],
'<_;_>[{'3}'NzMachineInt,{'3}'NzMachineInt],
'<_;_>[{'4}'NzMachineInt,{'4}'NzMachineInt],
'<_;_>[{'5}'NzMachineInt,{'5}'NzMachineInt],
'<_;_>[{'6}'NzMachineInt,{'6}'NzMachineInt],
'<_;_>[{'7}'NzMachineInt,{'7}'NzMachineInt],
'<_;_>[{'8}'NzMachineInt,{'8}'NzMachineInt],
'<_;_>[{'9}'NzMachineInt,{'9}'NzMachineInt],
'<_;_>[{'10}'NzMachineInt,{'10}'NzMachineInt]],
bindingList(binding(Y, {'11}'NzMachineInt),
bindingList(binding(X, {'1}'NzMachineInt),
nilBindingList)),
idle)