Strategy language for Maude

S. Eker, N. Martí-Oliet, J. Meseguer, and A. Verdejo

We are developing a basic strategy language for Maude, to be used at the object level, rather than at the metalevel. The strategy language allows the definition of strategy expressions that control the way a term is rewritten. Our design is based on a strict separation between the rewrite rules in system modules and the strategy expressions, that are specified in separate strategy modules. Thus, in our proposal it is not possible to use strategy expressions in the rewrite rules of a system module: they can only be specified in a separate strategy module. In fact, this separation makes possible defining different strategy modules to control in different ways the rewrites of a single system module.

A strategy is described as an operation that, when applied to a given term, produces a set of terms as a result, given that the process is nondeterministic in general. The basic strategies consist of the application of a rule (identified by the corresponding rule label) to a given term, and allowing variables in a rule to be instantiated before its application by means of a substitution. For conditional rules (which may contain rewrite conditions) such rewrite conditions can also be controlled by means of strategies. Basic strategies are combined by means of several combinators, including: regular expression constructions (concatenation, union, and iteration), if-then-else, combinators to control the way subterms of a given term are rewritten, and recursion.

The current design of the language is presented in this paper.

The language is being incorporated to the Maude system, but in the meantime you can use our prototype. It has been implemented on top of Full Maude. To use it you only need to load into Maude the maude-strat.maude file (updated February 27, 2011, to be run on Maude 2.6). The prototype supports all the language but strategy module importation and parametrization.

We can see how to use the prototype with an example. After loading the prototype we can enter a system module like the following one. It defines a blackboard as a multiset of natural numbers, some operations on the blackboard, and a rule selecting two numbers in the blackboard and replacing them by their arithmetic mean.

(mod BLACKBOARD is
  pr NAT .
  sort Blackboard .
  subsort Nat < Blackboard .

  op __ : Blackboard Blackboard -> Blackboard [assoc comm] .

  op minimum : Blackboard -> Nat .
  op remove : Nat Blackboard -> Blackboard .

  vars M N X : Nat .
  var B : Blackboard .

  eq minimum(N) = N .
  eq minimum(N M) = if (N < M) then N else M fi . 
  eq minimum(N M B) = if (N < M) then minimum(N B) 
                                 else minimum(M B) fi .
  eq remove(X, X B) = B .
  eq remove(X, B) = B [owise] .

  rl [play] : M N => (M + N) quo 2 .
endm)

With this module loaded we can already use the command for rewriting using a strategy.

Maude> (srew 2 4 6 8 using play .)
rewrite with strategy :
result Blackboard :
        3 6 8

It returns the first solution. We can ask for the next one:

Maude> (next .)
next solution rewriting with strategy :
result Blackboard :
        4 5 6

and then continue using again the strategy play:

Maude> (cont using play .)
rewrite with strategy :
result Blackboard :
        4 6

We can also ask for all the solutions obtained by applying a strategy to a given term:

Maude> (srewall 2 4 6 8 using play .)
rewrite with strategy :
Solution 1 :    3 6 8
Solution 2 :    4 4 8
Solution 3 :    4 5 6
Solution 4 :    2 5 8
Solution 5 :    2 6 6
Solution 6 :    2 4 7

We can also introduce strategy modules where strategies can be defined. The following module defines a strategy minmin that continuously applies the rewrite rule play to the two minimum values in the blackboard:

(smod BLACKBOARD-STRAT is
  
  strat minmin : @ Blackboard .

  vars X Y : Nat .
  var  B : Blackboard .

  sd minmin := 
     (matchrew B s.t. X := minimum(B) /\ Y := minimum(remove(X,B)) by
              B using play[M <- X ; N <- Y] 
     ) ! .
     
endsm)

And then the defined strategies can also be used in the strategy commands:

Maude> (srew 2000 20 2 200 10 50 using minmin .)
rewrite with strategy :
result NzNat :
        1057

Here you can find other simple examples:

Rewriting semantics

In order to advance the semantic foundations of the Maude strategy language, we have developed a detailed operational semantics by rewriting to Maude's strategy language. This is most fitting, since rewriting logic is a general semantic framework in which strategies themselves should not be thought of as extra-logical constructs, but should instead be expressed inside the logic. This idea of giving an operational, rewriting semantics to the strategy language is achieved in this paper by means of a theory transformation.

By taking advantage of the reflective properties of rewriting logic, which allow to consider metalevel entities such as theories as usual data, the transformation could be implemented as an operation from rewrite theories to rewrite theories, specified itself in rewriting logic. Instead of doing this, we have written a parameterized module that extends the metalevel with the rewriting semantics of the strategy language in a generic and quite efficient way.

Any questions or comments are welcomed. Alberto Verdejo