System modules in Maude are rewrite theories that do not need to be Church-Rosser and terminating. Therefore, we need to have good ways of controlling the rewriting inference process--which in principle could not terminate or 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 using statements in a normal module in Maude, and can be reasoned about as with statements in any other module. In general, strategies are defined in extensions of the META-LEVEL module by using metaReduce, metaApply, metaXapply, etc., as building blocks.
We illustrate some of these possibilities by implementing the following strategies for controlling the execution of the rules in the VENDING-MACHINE module in Section 5.1:
of them, with the coins
already inserted;
fmod BUYING-STRATS is
protecting META-LEVEL .
The function insertCoin below defines the strategy (1): it expects as first argument either 'add-q or 'add-$, for inserting a quarter or a dollar, respectively, and as second argument the metarepresentation of the marking of a vending machine, and it applies once the rule corresponding to the given label. The rules add-q and add-$ are applied using the descent function metaXapply. A rule cannot be applied when the result of metaXapply-ing the rule is not a term of sort Result4Tuple. Note the use of a matching equation in the condition to simplify the presentation of the righthand side of the equation (see Section 4.3), as well as the use of the statement attribute owise (see Section 4.5.4) to define the function insertCoin for unexpected cases.
var T : Term .
var Q : Qid .
var N : Nat .
vars BuyItem? BuyCake? Change? : [Result4Tuple].
op insertCoin : Qid Term -> Term .
ceq insertCoin(Q, T)
= if BuyItem? :: Result4Tuple
then getTerm(BuyItem?)
else T
fi
if (Q == 'add-q or Q == 'add-$)
/\ BuyItem? := metaXapply(upModule('VENDING-MACHINE, false),
T, Q, none, 0, unbounded, 0) .
eq insertCoin(Q, T) = T [owise] .
The function onlyCakes below defines the strategy (2): it applies the rule buy-c as many times as possible, applying the rule change whenever it is necessary. In particular, if the rule buy-c can be applied, then there is a recursive call to the function onlyCakes with the term resulting from its application. If the rule buy-c cannot be applied, then the application of the rule change is attempted. If the rule change can be applied, then there is a recursive call to the function onlyCakes with the term resulting from the change rule application. Otherwise, the argument is returned unchanged. The rules buy-c and change are also applied using the descent function metaXapply.
op onlyCakes : Term -> Term .
ceq onlyCakes(T)
= if BuyCake? :: Result4Tuple
then onlyCakes(getTerm(BuyCake?))
else (if Change? :: Result4Tuple
then onlyCakes(getTerm(Change?))
else T
fi)
fi
if BuyCake? := metaXapply(upModule('VENDING-MACHINE, false),
T, 'buy-c, none, 0, unbounded, 0)
/\ Change? := metaXapply(upModule('VENDING-MACHINE, false),
T, 'change, none, 0, unbounded, 0) .
The function onlyNitems defines the strategy (3): it
applies either the rule buy-c or buy-a (but not both)
at most times. As expected, the rules are applied using the descent function
metaXapply. Note the use of the symmetric difference operator sd
(see Section 7.2) to decrement N.
op onlyNitems : Term Qid Nat -> Term .
ceq onlyNitems(T, Q, N)
= if N == 0
then T
else (if BuyItem? :: Result4Tuple
then onlyNitems(getTerm(BuyItem?), Q, sd(N, 1))
else (if Change? :: Result4Tuple
then onlyNitems(getTerm(Change?), Q, N)
else T
fi)
fi)
fi
if (Q == 'buy-c or Q == 'buy-a)
/\ BuyItem? := metaXapply(upModule('VENDING-MACHINE, false),
T, Q, none, 0, unbounded, 0)
/\ Change? := metaXapply(upModule('VENDING-MACHINE, false),
T, 'change, none, 0, unbounded, 0) .
eq onlyNitems(T, Q, N) = T [owise] .
Finally, the function cakesAndApples defines the strategy (4): it applies the rule buy-c as many times as the rule buy-a. To define this function, we use an auxiliary Boolean function buyItem? that determines whether a given rule (buy-c or buy-a) can be applied. In the definition of cakesAndApples the Boolean function buyItem? is used to check if the rule buy-a can be applied after applying the rule buy-c. When the answer is true, then buy-c and buy-a are applied once, using the function onlyNitems with the appropriate arguments, and the function cakesAndApples is applied again to the result.
op cakesAndApples : Term -> Term .
op buyItem? : Term Qid -> Bool .
ceq buyItem?(T, Q)
= if BuyItem? :: Result4Tuple
then true
else (if Change? :: Result4Tuple
then buyItem?(getTerm(Change?), Q)
else false
fi)
fi
if (Q == 'buy-c or Q == 'buy-a)
/\ BuyItem? := metaXapply(upModule('VENDING-MACHINE, false),
T, Q, none, 0, unbounded, 0)
/\ Change? := metaXapply(upModule('VENDING-MACHINE, false),
T, 'change, none, 0, unbounded, 0) .
eq buyItem?(T, Q) = false [owise] .
eq cakesAndApples(T)
= if buyItem?(T, 'buy-c)
then (if buyItem?(onlyNitems(T, 'buy-c, 1), 'buy-a)
then cakesAndApples(onlyNitems(onlyNitems(T, 'buy-c, 1),
'buy-a, 1))
else T
fi)
else T
fi .
endfm
As examples, we apply below the buying strategies (2-4) to spend in different ways the same amount of money: three dollars and a quarter.
Maude> reduce in BUYING-STRATS :
onlyCakes('__['$.Coin,'$.Coin,'$.Coin,'q.Coin]) .
result GroundTerm: '__['q.Coin,'c.Item,'c.Item,'c.Item]
Maude> reduce in BUYING-STRATS :
onlyNitems('__['$.Coin, '$.Coin, '$.Coin, 'q.Coin],
'buy-a, 3) .
result GroundTerm:
'__['q.Coin, 'q.Coin, 'q.Coin, 'q.Coin, 'a.Item, 'a.Item, 'a.Item]
Maude> reduce in BUYING-STRATS :
cakesAndApples('__['$.Coin, '$.Coin, '$.Coin, 'q.Coin]) .
result GroundTerm: '__['$.Coin, 'q.Coin, 'q.Coin, 'a.Item, 'c.Item]
There is in fact great freedom for defining many different types of strategies, or even many different strategy languages inside Maude. As illustrated above with simple examples, this can be done in a completely user-definable way, so that users are not limited by a fixed and closed particular strategy language. Another example is presented in Section 15.6. See [12] for a general methodology for defining internal strategy languages using reflection, and [13,15] for other examples of rewriting strategies defined in Maude.
However, the great freedom of defining internal strategies at the metalevel is purchased at some cost. First, some familiarity with Maude's metalevel features is required; and second, some cost in performance is incurred in comparison with what might be possible in a direct implementation using Maude's rewrite engine. To address these two issues, a strategy language for Maude, that can be used entirely at the object level, has been proposed and has been implemented in prototype form [54]. Work on an implementation of this strategy language at the level of the Maude rewrite engine has already begun. We expect that this object-level strategy language will be available in future Maude releases.