Chapter 11
Reflection, Metalevel Computation, and Strategies

Informally, a reflective logic is a logic in which important aspects of its metatheory can be represented at the object level in a consistent way, so that the object-level representation correctly simulates the relevant metatheoretic aspects. In other words, a reflective logic is a logic which can be faithfully interpreted in itself. Maude’s language design and implementation make systematic use of the fact that rewriting logic is reflective [29223031]. This makes the metatheory of rewriting logic accessible to the user in a clear and principled way. However, since a naive implementation of reflection can be computationally expensive, a good implementation must provide efficient ways of performing reflective computations. This chapter explains how this is achieved in Maude through its predefined META-LEVEL module, that can be found in the prelude.maude file.

11.1 Reflection and metalevel computation

Rewriting logic is reflective in a precise mathematical way, namely, there is a finitely presented rewrite theory U that is universal in the sense that we can represent in U any finitely presented rewrite theory R (including U itself) as a term R, any terms t,tin R as terms t,t, and any pair (R,t) as a term R,t, in such a way that we have the following equivalence

Rt-→t′ ⇔ U⊢⟨R,t-→R,t.

Since U is representable in itself, we can achieve a “reflective tower” with an arbitrary number of levels of reflection:

Rt t′ ⇔ U⊢⟨R,t⟩→⟨R,t⟩ ⇔ U⊢⟨U,R,t⟩→⟨U,R,t

In this chain of equivalences we say that the first rewriting computation takes place at level 0, the second at level 1, and so on. In a naive implementation, each step up the reflective tower comes at considerable computational cost, because simulating a single step of rewriting at one level involves many rewriting steps one level up. It is therefore important to have systematic ways of lowering the levels of reflective computations as much as possible, so that a rewriting subcomputation happens at a higher level in the tower only when this is strictly necessary.

In Maude, key functionality of the universal theory U has been efficiently implemented in the functional module META-LEVEL. This module includes the modules META-VIEW, META-MODULE, and META-TERM. As an overview,

The functions metaReduce, metaApply, metaXapply, metaRewrite, metaFrewrite, metaMatch, and metaXmatch are called descent functions, since they allow us to descend levels in the reflective tower. The paper [25] provides a formal definition of the notion of descent function, and a detailed explanation of how they can be used to achieve a systematic, conservative way of lowering the levels of reflective computations.

The importation graph in Figure 11.1 shows the relationships between all the modules in the metalevel. The modules NAT-LIST and QID-LIST provide lists of natural numbers and quoted identifiers, respectively (see Section 7.12.1), and the module QID-SET provides sets of quoted identifiers (see Section 7.12.2). Notice that QID-SET is imported (in protecting mode) with renaming

  (op empty to none, op _,_ to _;_ [prec 43])

abbreviated to β in the figure.


PIC


Figure 11.1: Importation graph of metalevel modules


11.2 The META-TERM module

11.2.1 Metarepresenting sorts and kinds

In the META-TERM module, sorts and kinds are metarepresented as data in specific subsorts of the sort Qid of quoted identifiers.

A term of sort Sort is any quoted identifier not containing the following characters: ‘:’, ‘.’, ‘[’, and ‘]’. Moreover, the characters ‘{’, ‘}’, and ‘,’ can only appear in structured sort names (see Section 3.3). For example, ’Bool, ’NzNat, a‘{X‘}, a‘{X‘,Y‘}, a‘{b‘,c‘{d‘}‘}‘{e‘}, and a‘{‘(‘} are terms of sort Sort.

An element of sort Kind is a quoted identifier of the form ’‘[SortList‘] where SortList is a single identifier formed by a list of unquoted elements of sort Sort separated by backquoted commas. For example, ’‘[Bool‘] and ’‘[NzNat‘,Zero‘,Nat‘] are valid elements of the sort Kind. Note the use of backquotes to force them to be single identifiers.

Since commas and square brackets are used to metarepresent kinds, these characters are forbidden in sort names, in order to avoid undesirable ambiguities. Periods and colons are also forbidden, due to the metarepresentation of constants and variables, as explained in the next section.

Since operator declarations can use both sorts and kinds, we denote by Type the union of Sort and Kind.

  sorts Sort Kind Type .  
  subsorts Sort Kind < Type < Qid.  
  op <Qids> : -> Sort [special (...)] .  
  op <Qids> : -> Kind [special (...)] .

Remember from the introduction of Chapter 7 that <Qids> is a special operator declaration used to represent sets of constants that are not algebraically constructed, but are instead associated with appropriate C++ code by “hooks” which are specified following the special attribute; see the functional module META-TERM in file prelude.maude for the details omitted here.

11.2.2 Metarepresenting terms

In the module META-TERM, terms are metarepresented as elements of the data type Term of terms. The base cases in the metarepresentation of terms are given by subsorts Constant and Variable of the sort Qid.

  sorts Constant Variable Term .  
  subsorts Constant Variable < Qid Term .  
  op <Qids> : -> Constant [special (...)] .  
  op <Qids> : -> Variable [special (...)] .

Constants are quoted identifiers that contain the constant’s name and its type separated by a ‘.’, e.g., ’0.Nat. Similarly, variables contain their name and type separated by a ‘:’, e.g., ’N:Nat. Appropriate selectors then extract their names and types.

  op getName : Constant -> Qid .  
  op getName : Variable -> Qid .  
  op getType : Constant -> Type .  
  op getType : Variable -> Type .

Since ‘.’ and ‘:’ are not allowed in sort names (see Section 3.3), the name and type of a constant or variable can be calculated easily. Note that there is no restriction in operator or in variable names, and thus the scanning for ‘.’ or ‘:’ is done from right to left in the identifier. That is,

  getName(’:-D:Smile) = ’:-D  
  getType(’:-.|.‘[Smile‘]) = ’‘[Smile‘]

A term different from a constant or a variable is constructed in the usual way, by applying an operator symbol to a nonempty list of terms.

  sorts NeTermList TermList .  
  subsorts Term < NeTermList < TermList .  
  op _,_ : TermList TermList -> TermList  
       [ctor assoc id: empty gather (e E) prec 121] .  
  op _,_ : NeTermList TermList -> NeTermList [ctor ditto] .  
  op _,_ : TermList NeTermList -> NeTermList [ctor ditto] .  
  op _[_] : Qid NeTermList -> Term [ctor] .

The actual sort infrastructure provided by the module META-TERM is a bit more complex, because there are also subsorts and operators for the metarepresentation of ground terms and the corresponding lists of ground terms that we do not describe here (see the file prelude.maude for details).

Since terms in the module META-TERM can be metarepresented just as terms in any other module, the metarepresentation of terms can be iterated.

For example, the term c q M:Marking in the module VENDING-MACHINE in Section 5.1 is metarepresented by

  ’__[’c.Item, ’__[’q.Coin, ’M:Marking]]

and meta-metarepresented by

  ’_‘[_‘][’’__.Qid,  
          ’_‘,_[’’c.Item.Constant,  
                ’_‘[_‘][’’__.Qid,  
                        ’_‘,_[’’q.Coin.Constant,  
                              ’’M:Marking.Variable]]]]

Note that the metarepresentation of a natural number such as, e.g., 42 is ’s_^42[’0.Zero] instead of ’42.NzNat, since, as explained in Section 7.2, 42 is just syntactic sugar for s_^42(0).

11.3 The META-MODULE module: Metarepresenting modules

In the module META-MODULE, which imports META-TERM, functional and system modules, as well as functional and system theories, are metarepresented in a syntax very similar to their original user syntax.

The main differences are that:

1.
terms in equations, membership axioms, and rules are now metarepresented as we have already explained in Section 11.2.2;
2.
in the metarepresentation of modules and theories we follow a fixed order in introducing the different kinds of declarations for sorts, subsort relations, equations, etc., whereas in the user syntax there is considerable flexibility for introducing such different declarations in an interleaved and piecemeal way;
3.
there is no need for variable declarations—in fact, there is no syntax for metarepresenting them—and
4.
sets of identifiers—used in declarations of sorts—are metarepresented as sets of quoted identifiers built with an associative and commutative operator _;_.

The syntax for the top-level operators metarepresenting functional and system modules and functional and system theories (just modules in general) is as follows, where Header means just an identifier in the case of non-parameterized modules or an identifier together with a list of parameter declarations in the case of a parameterized module.

  sorts FModule SModule FTheory STheory Module .  
  subsorts FModule < SModule < Module .  
  subsorts FTheory < STheory < Module .  
  sort Header .  
  subsort Qid < Header .  
  op _{_}  : Qid ParameterDeclList -> Header [ctor] .  
  op fmod_is_sorts_.____endfm : Header ImportList SortSet  
       SubsortDeclSet OpDeclSet MembAxSet EquationSet -> FModule  
       [ctor gather (& & & & & & &)] .  
  op mod_is_sorts_._____endm : Header ImportList SortSet  
       SubsortDeclSet OpDeclSet MembAxSet EquationSet RuleSet  
       -> SModule [ctor gather (& & & & & & & &)] .  
  op fth_is_sorts_.____endfth : Qid ImportList SortSet SubsortDeclSet  
       OpDeclSet MembAxSet EquationSet -> FTheory  
       [ctor gather (& & & & & & &)] .  
  op th_is_sorts_._____endth : Qid ImportList SortSet SubsortDeclSet  
       OpDeclSet MembAxSet EquationSet RuleSet -> STheory  
       [ctor gather (& & & & & & & &)] .

Appropriate selectors then extract from the metarepresentation of modules the metarepresentations of their names, imported submodules, and declared sorts, subsorts, operators, memberships, equations, and rules.

  op getName : Module -> Qid .  
  op getImports : Module -> ImportList .  
  op getSorts : Module -> SortSet .  
  op getSubsorts : Module -> SubsortDeclSet .  
  op getOps : Module -> OpDeclSet .  
  op getMbs : Module -> MembAxSet .  
  op getEqs : Module -> EquationSet .  
  op getRls : Module -> RuleSet .

Without going into all the syntactic details, we show only the operators used to metarepresent sets of sorts and kinds, conditions, equations, and rules. The complete syntax used for metarepresenting modules can be found in the module META-MODULE in the file prelude.maude.

  sorts EmptyTypeSet NeSortSet NeKindSet  
        NeTypeSet SortSet KindSet TypeSet .  
  subsort EmptyTypeSet < SortSet KindSet < TypeSet < QidSet .  
  subsort Sort < NeSortSet < SortSet .  
  subsort Kind < NeKindSet < KindSet .  
  subsort Type NeSortSet NeKindSet < NeTypeSet < TypeSet NeQidSet .  
  op none : -> EmptyTypeSet [ctor] .  
  op _;_ : TypeSet TypeSet -> TypeSet  
       [ctor assoc comm id: none prec 43] .  
  op _;_ : SortSet SortSet -> SortSet [ctor ditto] .  
  op _;_ : KindSet KindSet -> KindSet [ctor ditto] .  
 
  sorts EqCondition Condition .  
  subsort EqCondition < Condition .  
  op nil : -> EqCondition [ctor] .  
  op _=_ : Term Term -> EqCondition [ctor prec 71] .  
  op _:_ : Term Sort -> EqCondition [ctor prec 71] .  
  op _:=_ : Term Term -> EqCondition [ctor prec 71] .  
  op _=>_ : Term Term -> Condition [ctor prec 71] .  
  op _/\_ : EqCondition EqCondition -> EqCondition  
       [ctor assoc id: nil prec 73] .  
  op _/\_ : Condition Condition -> Condition  
       [ctor assoc id: nil prec 73] .  
 
  sorts Equation EquationSet .  
  subsort Equation < EquationSet .  
  op eq_=_[_]. : Term Term AttrSet -> Equation [ctor] .  
  op ceq_=_if_[_]. : Term Term EqCondition AttrSet -> Equation  
       [ctor] .  
  op none : -> EquationSet [ctor] .  
  op __ : EquationSet EquationSet -> EquationSet  
       [ctor assoc comm id: none] .  
 
  sorts Rule RuleSet .  
  subsort Rule < RuleSet .  
  op rl_=>_[_]. : Term Term AttrSet -> Rule [ctor] .  
  op crl_=>_if_[_]. : Term Term Condition AttrSet -> Rule [ctor] .  
  op none : -> RuleSet [ctor] .  
  op __ : RuleSet RuleSet -> RuleSet [ctor assoc comm id: none] .

For example, we show here the metarepresentations of the modules introduced in Section 5.1 VENDING-MACHINE-SIGNATURE and VENDING-MACHINE.

  fmod ’VENDING-MACHINE-SIGNATURE is  
    nil  
    sorts ’Coin ; ’Item ; ’Marking .  
    subsort ’Coin < ’Marking .  
    subsort ’Item < ’Marking .  
    op ’__ : ’Marking ’Marking -> ’Marking  
          [assoc comm id(’null.Marking)] .  
    op ’a : nil -> ’Item [format(’b! ’o)] .  
    op ’null : nil -> ’Marking [none] .  
    op ’$ : nil -> ’Coin [format(’r! ’o)] .  
    op ’q : nil -> ’Coin [format(’r! ’o)] .  
    op ’c : nil -> ’Item [format(’b! ’o)] .  
    none  
    none  
  endfm

  mod ’VENDING-MACHINE is  
    including ’VENDING-MACHINE-SIGNATURE .  
    sorts none .  
    none  
    none  
    none  
    none  
    rl ’M:Marking => ’__[’M:Marking, ’q.Coin] [label(’add-q)] .  
    rl ’M:Marking => ’__[’M:Marking, ’$.Coin] [label(’add-$)] .  
    rl ’$.Coin => ’c.Item [label(’buy-c)] .  
    rl ’$.Coin => ’__[’a.Item, ’q.Coin] [label(’buy-a)] .  
    rl ’__[’q.Coin, ’__[’q.Coin, ’__[’q.Coin, ’q.Coin]]]  
      => ’$.Coin [label(’change)] .  
  endm

Since VENDING-MACHINE-SIGNATURE has no list of imported submodules, no membership axioms, and no equations, those fields are filled, respectively, with the constants nil of sort ImportList, none of sort MembAxSet, and none of sort EquationSet. Similarly, since the module VENDING-MACHINE has no subsort declarations and no operator declarations, those fields are filled, respectively, with the constants none of sort SubsortDeclSet and none of sort OpDeclSet. Variable declarations are not metarepresented, but rather each variable is metarepresented in its “on the fly”-declaration form, i.e., with its sort or kind.

As mentioned above, parameterized modules are also metarepresented through the notion of a header, which is either an identifier (for non-parameterized modules) or an identifier together with a list of parameter declarations (for parameterized modules). Such parameter declarations are metarepresented again with a syntax similar to the user syntax.

  sorts ParameterDecl NeParameterDeclList ParameterDeclList .  
  subsorts ParameterDecl < NeParameterDeclList < ParameterDeclList .  
  op _::_ : Sort ModuleExpression -> ParameterDecl .  
  op nil : -> ParameterDeclList [ctor] .  
  op _,_ : ParameterDeclList ParameterDeclList -> ParameterDeclList  
       [ctor assoc id: nil prec 121] .

Module expressions involving renamings and summations can also be metarepresented with the expected syntax:

  sort ModuleExpression .  
  subsort Qid < ModuleExpression .  
  op _+_ : ModuleExpression ModuleExpression -> ModuleExpression  
       [ctor assoc comm] .  
  op _*(_) : ModuleExpression RenamingSet -> ModuleExpression  
       [ctor prec 39 format (d d s n++i n--i d)] .  
 
  sorts Renaming RenamingSet .  
  subsort Renaming < RenamingSet .  
  op sort_to_ : Qid Qid -> Renaming [ctor] .  
  op op_to_[_] : Qid Qid AttrSet -> Renaming  
       [ctor format (d d d d s d d d)] .  
  op op_:_->_to_[_] : Qid TypeList Type Qid AttrSet -> Renaming  
       [ctor format (d d d d d d d d s d d d)] .  
  op label_to_ : Qid Qid -> Renaming [ctor] .  
  op _,_ : RenamingSet RenamingSet -> RenamingSet  
       [ctor assoc comm prec 43 format (d d ni d)] .

Finally, the instantiation of a parameterized module is metarepresented as follows:

  op _{_} : ModuleExpression ParameterList -> ModuleExpression  
       [ctor prec 37].  
 
  sort EmptyCommaList NeParameterList ParameterList .  
  subsorts Sort < NeParameterList < ParameterList .  
  subsort EmptyCommaList < GroundTermList ParameterList .  
  op empty : -> EmptyCommaList [ctor] .  
  op _,_ : ParameterList ParameterList -> ParameterList [ctor ditto] .

The rules for constructing parameterized metamodules and instantiating parameterized modules existing in the database reflect the object-level rules. In particular, bound parameters are permitted; for example, the following term metarepresents a parameterized module:

  fmod ’PARMODEX{’X :: ’TRIV} is  
    including ’MAP{’String, ’X} .  
    sorts ’Foo .  
    none  
    none  
    none  
    none  
  endfm

Although, as we will see in the following section, views can be metarepresented as terms of the View sort, it is not possible to use the views constructed at the metalevel in module expressions. The views used in the module expressions occurring in metamodules must have been declared at the object level, so that they are present in the database of modules and views declared in the given session. Such views are written in quoted form within metamodule expressions, like ’String in ’MAP{’String, ’X} in the example above.

Note that terms of sort Module can be metarepresented again, yielding then a term of sort Term, and this can be iterated an arbitrary number of times. This is in fact necessary when a metalevel computation has to operate at higher levels.

11.4 The META-VIEW module: Metarepresenting views

In the module META-VIEW, which imports META-MODULE, views are metarepresented in a syntax very similar to their original user syntax.

  sort View .  
  op view_from_to_is__endv : Header ModuleExpression ModuleExpression  
       SortMappingSet OpMappingSet -> View [ctor gather (& & & & &)  
       format (d d d d d d d n++i ni n--i d)] .

The first argument corresponds to the name of the view, while the second and third are module expressiones corresponding to the source (usually a theory) and target (usually a module) of the view, respectively. The fourth and fifth arguments are the sort mappings and the operator mappings defining the view.

The following syntax defines sets of sort mappings in a way completely similar to the user syntax.

  sorts SortMapping SortMappingSet .  
  subsort SortMapping < SortMappingSet .  
  op sort_to_. : Sort Sort -> SortMapping [ctor] .  
  op none : -> SortMappingSet [ctor] .  
  op __ : SortMappingSet SortMappingSet -> SortMappingSet  
       [ctor assoc comm id: none format (d ni d)] .  
  eq S:SortMapping S:SortMapping = S:SortMapping .

Analogously, the following syntax is used to define set of operator mappings.

  sorts OpMapping OpMappingSet .  
  subsort OpMapping < OpMappingSet .  
  op (op_to_.) : Qid Qid -> OpMapping [ctor] .  
  op (op_:_->_to_.) : Qid TypeList Type Qid -> OpMapping [ctor] .  
  op (op_to term_.) : Term Term -> OpMapping [ctor] .  
  op none : -> OpMappingSet [ctor] .  
  op __ : OpMappingSet OpMappingSet -> OpMappingSet  
       [ctor assoc comm id: none format (d ni d)] .  
  eq O:OpMapping O:OpMapping = O:OpMapping .

Finally, appropriate selectors are used to extract from the metarepresentation of a view the corresponding components, namely, the metarepresentations of its name, of its source, of its target, of its set of sort mappings, and of its set of operator mappings.

  op getName : View -> Qid .  
  op getFrom : View -> ModuleExpression .  
  op getTo : View -> ModuleExpression .  
  op getSortMappings : View -> SortMappingSet .  
  op getOpMappings : View -> OpMappingSet .

For example, the metarepresentation of the view RingToRat (see Section 6.3.2) from the theory RING to the predefined RAT module is as follows:

  view ’RingToRat from ’RING to ’RAT is  
    sort ’Ring to ’Rat .  
    op ’z to ’0 .  
    op ’e.Ring to term ’s_[’0.Zero] .  
  endv

Then, we can extract some components of this metarepresented view:

  Maude> reduce in META-VIEW :  
            getFrom(view ’RingToRat from ’RING to ’RAT is  
                      sort ’Ring to ’Rat .  
                      op ’z to ’0 .  
                      op ’e.Ring to term ’s_[’0.Zero] .  
                    endv) .  
  result Sort: ’RING  
 
  Maude> reduce in META-VIEW :  
            getOpMappings(view ’RingToRat from ’RING to ’RAT is  
                            sort ’Ring to ’Rat .  
                            op ’z to ’0 .  
                            op ’e.Ring to term ’s_[’0.Zero] .  
                          endv) .  
  result OpMappingSet:  
    op ’z to ’0 .  
    op ’e.Ring to term ’s_[’0.Zero] .

11.5 The META-LEVEL module: Metalevel operations

The META-LEVEL module, which imports META-VIEW, has several built-in descent functions that provide useful and efficient ways of reducing metalevel computations to object-level ones, as well as several useful operations on sorts and kinds. Since, in general, these operations take among their arguments the metarepresentations of modules, sorts, kinds, terms, and so on, the META-LEVEL modules also provides several built-in functions for moving conveniently between reflection levels. Notice that most of the operations in the module META-LEVEL are partial (as explicitly stated by using the arrow ~> in the corresponding operator declaration). This is due to the fact that they do not make sense on terms that, although may be of the correct sort, for example, Module or Term, either are not correct metarepresentations of modules or are not correct metarepresentations of terms in the module provided as another argument.

Concerning partial operations, the criteria used to choose between using a supersort for the result and having an operator map to a kind is as follows.

If the error return value is built from constructors, say

  op noParse : Nat -> ResultPair? [ctor] .  
  op ambiguity : ResultPair ResultPair -> ResultPair? [ctor] .

it goes to a supersort. In some sense these are not errors, but merely exceptions or out-of-band results for which there is a carefully defined semantics.

The kind is reserved for nonconstructors which may not be able to reduce at all on illegal arguments, like, for example, in the function (notice the form of the arrow)

  op metaParse : Module QidList Type? ~> ResultPair? [special (...)] .

In this second case, an expression that does not evaluate to the appropriate sort represents a real error.

So, for example, a call to metaParse with an ill-formed module would produce an unreduced term metaParse(...) in the kind, whereas a call to metaParse with valid arguments but a list of tokens that could not be parsed to a term of the desired type in the metamodule would produce a term noParse(...) of sort ResultPair? indicating where the parse first failed.

11.5.1 Moving between reflection levels: upModule, upTerm, downTerm, and others

For a module R that has already been loaded into Maude, the operations upSorts, upSubsortDecl, upOpDecls, upMbs, upEqs, upRls, and upModule take as arguments the metarepresentation of the name of R and a Boolean value b, and return, respectively, the metarepresentations of the module R, of its sorts, subsort declarations, operator declarations, membership axioms, equations, and rules. If the second argument of these functions is true, then the resulting metarepresentations will include the corresponding statements that R imports from its submodules; but if the second argument is false, the resulting metarepresentations will only contain the metarepresentations of the statements explicitly declared in R.

  op upModule : Qid Bool ~> Module [special (...)] .  
  op upSorts : Qid Bool ~> SortSet [special (...)] .  
  op upSubsortDecls : Qid Bool ~> SubsortDeclSet [special (...)] .  
  op upOpDecls : Qid Bool ~> OpDeclSet [special (...)] .  
  op upMbs : Qid Bool ~> MembAxSet [special (...)] .  
  op upEqs : Qid Bool ~> EquationSet [special (...)] .  
  op upRls : Qid Bool ~> RuleSet [special (...)] .

We give below simple examples of using these functions. Note that, since BOOL is automatically imported by all modules, its equations are shown when upEqs is called with true as its second argument. For the same reason, the metarepresentation of the VENDING-MACHINE-SIGNATURE module includes an including declaration that was not explicit in that module. Here, and in the rest of this section, we assume that the modules NUMBERS and SIEVE from Chapter 4, as well as the modules VENDING-MACHINE-SIGNATURE and VENDING-MACHINE from Chapter 5, have already been loaded into Maude.

  Maude> reduce in META-LEVEL :  
           upModule(’VENDING-MACHINE-SIGNATURE, false) .  
  result FModule:  
    fmod ’VENDING-MACHINE-SIGNATURE is  
    including ’BOOL .  
    sorts ’Coin ; ’Item ; ’Marking .  
    subsort ’Coin < ’Marking .  
    subsort ’Item < ’Marking .  
    op ’$ : nil -> ’Coin [format(’r! ’o)] .  
    op ’__ : ’Marking ’Marking -> ’Marking  
          [assoc comm id(’null.Marking)] .  
    op ’a : nil -> ’Item [format(’b! ’o)] .  
    op ’c : nil -> ’Item [format(’b! ’o)] .  
    op ’null : nil -> ’Marking [none] .  
    op ’q : nil -> ’Coin [format(’r! ’o)] .  
    none  
    none  
  endfm

  Maude> reduce in META-LEVEL : upEqs(’VENDING-MACHINE, true) .  
  result EquationSet:  
    eq ’_and_[’true.Bool, ’A:Bool] = ’A:Bool [none] .  
    eq ’_and_[’A:Bool, ’A:Bool] = ’A:Bool [none] .  
    eq ’_and_[’A:Bool, ’_xor_[’B:Bool, ’C:Bool]]  
      = ’_xor_[’_and_[’A:Bool, ’B:Bool], ’_and_[’A:Bool, ’C:Bool]]  
      [none] .  
    eq ’_and_[’false.Bool, ’A:Bool] = ’false.Bool [none] .  
    eq ’_or_[’A:Bool,’B:Bool]  
      = ’_xor_[’_and_[’A:Bool, ’B:Bool],’_xor_[’A:Bool, ’B:Bool]]  
      [none] .  
    eq ’_xor_[’A:Bool, ’A:Bool] = ’false.Bool [none] .  
    eq ’_xor_[’false.Bool, ’A:Bool] = ’A:Bool [none] .  
    eq ’not_[’A:Bool] = ’_xor_[’true.Bool, ’A:Bool] [none] .  
    eq ’_implies_[’A:Bool, ’B:Bool]  
      = ’not_[’_xor_[’A:Bool, ’_and_[’A:Bool, ’B:Bool]]] [none] .

  Maude> reduce in META-LEVEL : upEqs(’VENDING-MACHINE, false) .  
  result EquationSet: (none).EquationSet

  Maude> reduce in META-LEVEL : upRls(’VENDING-MACHINE, true) .  
  result RuleSet:  
    rl ’$.Coin => ’c.Item [label(’buy-c)] .  
    rl ’$.Coin => ’__[’q.Coin,’a.Item] [label(’buy-a)] .  
    rl ’M:Marking => ’__[’$.Coin,’M:Marking] [label(’add-$)] .  
    rl ’M:Marking => ’__[’q.Coin,’M:Marking] [label(’add-q)] .  
    rl ’__[’q.Coin,’q.Coin,’q.Coin,’q.Coin] => ’$.Coin  
      [label(’change)] .

In addition to the upModule operator, there is another operator allowing the use of an already loaded module at the metalevel. This operator is defined in the module META-MODULE as follows:

  op [_] : Qid -> Module .  
  eq [Q:Qid] = (th Q:Qid is including Q:Qid .  
                sorts none . none none none none none endth) .

This operator is just syntactic sugar for accessing the corresponding module. Notice that the module is not moved up to the metalevel as upModule does, it is just a way of referring to it, and therefore more efficient.

The META-LEVEL module also provides a function upImports that takes as argument the metarepresentation of the name of a module R . When R is already in the Maude module database, then upImports returns the metarepresentation of its list of imported submodules. The function upImports does not take a Boolean argument, as the previous up-functions, since it is not useful to ask for the list of imported submodules of a flattened module.

  op upImports : Qid ~> ImportList [special (...)] .

In the same way, the META-LEVEL module provides a function upView that takes as argument the metarepresentation of the name of a view; when such a view is in the Maude view database, then upView returns the corresponding metarepresentation.

  op upView : Qid ~> View [special (...)] .

As a simple example, let us consider the view String0 from the predefined theory DEFAULT to the predefined module STRING, all of them provided in prelude.maude; then,

  Maude> reduce in META-LEVEL : upView(’String0) .  
  result View:  
    view ’String0 from ’DEFAULT to ’STRING is  
      sort ’Elt to ’String .  
      op ’0.Elt to term ’"".String .  
    endv

Finally, the META-LEVEL module introduces two polymorphic functions. The function upTerm takes a term t and returns the metarepresentation of its canonical form. The function downTerm takes the metarepresentation of a term t as its first argument and a term tas its second argument, and returns the canonical form of t, if t is a term in the same kind as t; otherwise, it returns the canonical form of t.

  op upTerm : Universal -> Term [poly (1) special (...)] .  
  op downTerm : Term Universal -> Universal  
       [poly (2 0) special (...)] .

As simple examples, we can use the function upTerm to obtain the metarepresentation of the term f(a, f(b, c)) in the module UP-DOWN-TEST below, and the function downTerm to recover the term f(a, f(b, c)) from its metarepresentation.

  fmod UP-DOWN-TEST is  
    protecting META-LEVEL .  
    sort Foo .  
    ops a b c d : -> Foo .  
    op f : Foo Foo -> Foo .  
    op error : -> [Foo] .  
    eq c = d .  
  endfm

  Maude> reduce in UP-DOWN-TEST : upTerm(f(a, f(b, c))) .  
  result GroundTerm: ’f[’a.Foo,’f[’b.Foo,’d.Foo]]

Notice in the previous example that the given argument has been reduced before obtaining its metarepresentation, more specifically, the subterm c has become d. In the following examples we can observe the same behavior with respect to downTerm.

  Maude> reduce in UP-DOWN-TEST :  
           downTerm(’f[’a.Foo,’f[’b.Foo,’c.Foo]], error) .  
  result Foo: f(a, f(b, d))

  Maude> reduce in UP-DOWN-TEST :  
           downTerm(upTerm(f(a, f(b, c))), error) .  
  result Foo: f(a, f(b, d))

In our last example, we show the result of downTerm when its first argument does not correspond to the metarepresentation of a term in the module UP-DOWN-TEST; notice the constant e in the metarepresented term that does not correspond to a declared constant in the module.

  Maude> reduce in UP-DOWN-TEST :  
           downTerm(’f[’a.Foo,’f[’b.Foo,’e.Foo]], error) .  
  Advisory: could not find a constant e of  
            sort Foo in meta-module UP-DOWN-TEST.  
  result [Foo]: error

Due to the failure in moving down the metarepresented term given as first argument, the result is the term given as second argument, namely, error, which was declared in the module UP-DOWN-TEST as a constant of kind [Foo].

11.5.2 Simplifying: metaReduce and metaNormalize

metaReduce

The (partial) operation metaReduce takes as arguments the metarepresentation of a module R and the metarepresentation of a term t.

  sort ResultPair .  
  op {_,_} : Term Type -> ResultPair [ctor] .  
  op metaReduce : Module Term ~> ResultPair [special (...)] .

When t is a term in R, metaReduce(R,t) returns the metarepresentation of the canonical form of t, using the equations in R, together with the metarepresentation of its corresponding sort or kind. The reduction strategy used by metaReduce coincides with that of the reduce command (see Sections 4.9 and 18.2).

As said above, in general, when either the first argument of metaReduce is a term of sort Module but not a correct metarepresentation R of an object module R, or the second argument is not the correct metarepresentation t of a term t in R, the operation metaReduce is undefined, that is, the term metaReduce(u,v) does not reduce and it does not get evaluated to a term of sort ResultPair, but only to an expression in the kind [ResultPair].

Appropriate selectors extract from the result pairs their two components:

  op getTerm : ResultPair -> Term .  
  op getType : ResultPair -> Type .

Using metaReduce we can simulate at the metalevel the primes computation example at the end of Section 4.4.7.

  Maude> reduce in META-LEVEL :  
           metaReduce(upModule(’SIEVE, false),  
             ’show_upto_[’primes.NatList, ’s_^10[’0.Zero]]) .  
  result ResultPair:  
    {’_._[’s_^2[’0.Zero], ’s_^3[’0.Zero], ’s_^5[’0.Zero],  
          ’s_^7[’0.Zero], ’s_^11[’0.Zero], ’s_^13[’0.Zero],  
          ’s_^17[’0.Zero], ’s_^19[’0.Zero], ’s_^23[’0.Zero],  
          ’s_^29[’0.Zero]],  
     ’NatList}

We can also insert a new element into an empty map of the type declared in the module PARMODEX at the end of Section 11.3 as follows:

  Maude> red in META-LEVEL :  
           metaReduce(  
             fmod ’PARMODEX{’X :: ’TRIV} is  
               including ’MAP{’String, ’X} .  
               sorts ’Foo .  
               none  
               none  
               none  
               none  
             endfm,  
             ’insert[’"foo".String, ’A:X$Elt,  
                     ’empty.Map‘{String‘,X‘}]) .  
  result ResultPair:  
    {’_|->_[’"foo".String,’A:X$Elt],’Entry‘{String‘,X‘}}

Notice that the module expression ’MAP{’String, ’X} has a bound parameter X, which appears also in the sort X$Elt in the on-the-fly declaration of the variable A:X$Elt.

metaNormalize

The (partial) operation metaNormalize takes as arguments the metarepresentation of a module R and the metarepresentation of a term t.

  op metaNormalize : Module Term ~> ResultPair [special (...)] .

When t is a term in R, metaNormalize(R,t) returns the metarepresentation of the normal form of t with respect to the equational theory consisting of the equational attributes of the operators in t, without doing any simplification or rewriting with respect to equations or rules in R, together with the metarepresentation of its corresponding sort or kind. For example, from the declarations in the predefined NAT module

  op s_ : Nat -> NzNat  [ctor iter  special (...)] .  
  op _+_ : NzNat Nat -> NzNat [assoc comm prec 33 special (...)] .  
  op _+_ : Nat Nat -> Nat [ditto] .

we know that the successor operator satisfies the iter theory (see Section 4.4.2) and that the addition operator is associative and commutative (see Section 4.4.1). With this information it is easy to make sense of the following results:

  Maude> red in META-LEVEL :  
           metaNormalize(upModule(’NAT, false), ’s_[’s_[’0.Zero]]) .  
  result ResultPair: {’s_^2[’0.Zero],’NzNat}  
 
  Maude> red in META-LEVEL :  
           metaNormalize(upModule(’NAT, false),  
             ’_+_[’s_[’s_[’0.Zero]],’0.Zero]) .  
  result ResultPair: {’_+_[’0.Zero,’s_^2[’0.Zero]],’NzNat}  
 
  Maude> red in META-LEVEL :  
           metaNormalize(upModule(’NAT, false),  
             ’_+_[’0.Zero,’_+_[’s_[’s_[’0.Zero]],’0.Zero]]) .  
  result ResultPair: {’_+_[’0.Zero,’0.Zero,’s_^2[’0.Zero]],’NzNat}

Notice that associative terms are flattened and, if they are also commutative, the subterms are sorted with respect to an internal order. Notice also that in the last two examples the subterm ’0.Zero does not disappear. This is because 0 is not declared as an identity element for _+_.

11.5.3 Rewriting: metaRewrite and metaFrewrite

metaRewrite

The (partial) operation metaRewrite takes as arguments the metarepresentation of a module R, the metarepresentation of a term t, and a value b of the sort Bound, i.e., either a natural number or the constant unbounded.

  sort Bound .  
  subsort Nat < Bound .  
  op unbounded :-> Bound [ctor] .  
  op metaRewrite : Module Term Bound ~> ResultPair [special (...)] .

The operation metaRewrite is entirely analogous to metaReduce, but instead of using only the equational part of a module it now uses both the equations and the rules to rewrite the term. The reduction strategy used by metaRewrite coincides with that of the rewrite command (see Sections 5.4 and 18.2). That is, the result of metaRewrite(R, t, b) is the metarepresentation of the term obtained from t after at most b applications of the rules in R using the rewrite strategy, together with the metarepresentation of its corresponding sort or kind. When the value unbounded is given as the third argument, no bound is imposed to the number of rewrites, and rewriting proceeds to the bitter end.

Using metaRewrite we can redo at the metalevel the examples in Section 5.4.

  Maude> reduce in META-LEVEL :  
           metaRewrite(upModule(’VENDING-MACHINE, false),  
             ’__[’$.Coin, ’__[’$.Coin, ’__[’q.Coin, ’q.Coin]]], 1) .  
  result ResultPair:  
    {’__[’$.Coin, ’$.Coin, ’q.Coin, ’q.Coin, ’q.Coin], ’Marking}

  Maude> reduce in META-LEVEL :  
           metaRewrite(upModule(’VENDING-MACHINE, false),  
             ’__[’$.Coin, ’__[’$.Coin, ’__[’q.Coin, ’q.Coin]]], 2) .  
  result ResultPair:  
    {’__[’$.Coin, ’$.Coin, ’$.Coin, ’q.Coin, ’q.Coin, ’q.Coin],  
         ’Marking}

metaFrewrite

Position fair rewriting, which was described in Section 5.4, is metarepresented by the operation metaFrewrite. This (partial) operation takes as arguments the metarepresentation of a module, the metarepresentation of a term, a value of sort Bound, and a natural number.

  op metaFrewrite : Module Term Bound Nat ~> ResultPair  
       [special (...)] .

The reduction strategy used by metaFrewrite coincides with that of the frewrite command in Maude, except that a final (semantic) sort calculation is performed at the end in order to produce a correct ResultPair. That is, frewrite(R, t, b, n) results in the metarepresentation of the term obtained from t after at most b applications of the rules in R using the frewrite strategy, with at most n rewrites at each entitled position on each traversal of a subject term, together with the metarepresentation of its corresponding sort or kind. When the value unbounded is given as the third argument, no bound is imposed to the number of rewrites.

Using metaFrewrite we can redo at the metalevel the examples in Section 5.4.

  Maude> reduce in META-LEVEL :  
           metaFrewrite(upModule(’VENDING-MACHINE, false),  
             ’__[’$.Coin, ’__[’$.Coin, ’__[’q.Coin, ’q.Coin]]],  
             1, 1) .  
  result ResultPair:  
    {’__[’$.Coin, ’q.Coin, ’q.Coin, ’c.Item], ’Marking}  
 
  Maude> reduce in META-LEVEL :  
           metaFrewrite(upModule(’VENDING-MACHINE, false),  
             ’__[’$.Coin, ’__[’$.Coin, ’__[’q.Coin, ’q.Coin]]],  
             12, 1) .  
  result ResultPair:  
    {’__[’$.Coin, ’$.Coin, ’$.Coin, ’$.Coin, ’q.Coin, ’q.Coin,  
         ’q.Coin, ’q.Coin, ’q.Coin, ’q.Coin, ’q.Coin, ’q.Coin,  
         ’q.Coin,’a.Item,’c.Item],  
     ’Marking}

11.5.4 Applying rules: metaApply and metaXapply

metaApply

The (partial) operation metaApply takes as arguments the metarepresentation of a module, the metarepresentation of a term, the metarepresentation of a rule label, the metarepresentation of a set of assignments (possibly empty) defining a partial substitution, and a natural number.

  sorts Assignment Substitution .  
  subsort Assignment < Substitution .  
  op _<-_ : Variable Term -> Assignment [ctor prec 63] .  
  op none : -> Substitution [ctor] .  
  op _;_ : Substitution Substitution -> Substitution  
       [assoc comm id: none prec 65] .  
 
  sort ResultTriple ResultTriple? .  
  subsort ResultTriple < ResultTriple? .  
  op {_,_,_} : Term Type Substitution -> ResultTriple [ctor] .  
  op failure : -> ResultTriple? [ctor] .  
  op metaApply : Module Term Qid Substitution Nat ~> ResultTriple?  
       [special (...)] .

The operation metaApply(R, t, l, σ, n) is evaluated as follows:

1.
the term t is first fully reduced using the equations in R;
2.
the resulting term is matched at the top against all rules with label l in R partially instantiated with σ, with matches that fail to satisfy the condition of their rule discarded;
3.
the first n successful matches are discarded; if there is an (n + 1)th match, its rule is applied using that match and the steps 4 and 5 below are taken; otherwise failure is returned;
4.
the term resulting from applying the given rule with the (n + 1)th match is fully reduced using the equations in R;
5.
the triple formed by the metarepresentation of the resulting fully reduced term, the metarepresentation of its corresponding sort or kind, and the metarepresentation of the substitution used in the reduction is returned.

The failure value should not be confused with the “undefined” value for the metaApply operation. As already mentioned before for descent functions in general, this operation is partial because it does not make sense on some nonvalid arguments that are terms of the appropriate sort but are not correct metarepresentations. However, even if all arguments are valid in this sense, the intended rule application may fail, either because there is no match or because the match does not satisfy the corresponding rule condition, and then failure is used to represent this situation, which is important to distinguish from ill-formed invocations, for example, for error recovery purposes.

Note also that, according to the information in step 3 above, the last argument of metaApply is a natural number used to enumerate (starting from 0) all the possible solutions of the intended rule application. For efficiency, the different solutions should be generated in order, that is, starting with the argument 0 and increasing it until a failure is obtained, indicating that there are no more solutions.

Appropriate selectors extract from the result triples their three components:

  op getTerm : ResultTriple -> Term .  
  op getType : ResultTriple -> Type .  
  op getSubstitution : ResultTriple -> Substitution .

As an example, we can force at the metalevel the rewriting of the term $ in the module VENDING-MACHINE, so that only the rule buy-c is used, and only once.

  Maude> reduce in META-LEVEL :  
           metaApply(upModule(’VENDING-MACHINE, false),  
             ’$.Coin, ’buy-c, none, 0) .  
  result ResultTriple: {’c.Item, ’Item, none}

Similarly, we can force the rewriting of the same term so that this time only the rule add-$ is applied.

  Maude> reduce in META-LEVEL :  
           metaApply(upModule(’VENDING-MACHINE, false),  
             ’$.Coin, ’add-$, none, 0) .  
  result ResultTriple:  
    {’__[’$.Coin, ’$.Coin], ’Marking, ’M:Marking <- ’$.Coin}

However, using metaApply, we cannot force the term q $ to be rewritten with the rule buy-c, since its lefthand side, $, does not match (without extension) this term. In this case, we should use instead the metaXapply operation described below.

  Maude> reduce in META-LEVEL :  
           metaApply(upModule(’VENDING-MACHINE, false),  
             ’__[’q.Coin, ’$.Coin], ’buy-c, none, 0) .  
  result ResultTriple?: (failure).ResultTriple?

metaXapply

The (partial) operation metaXapply takes as arguments the metarepresentation of a module, the metarepresentation of a term, the metarepresentation of a rule label, the metarepresentation of a set of assignments (possibly empty) defining a partial substitution, a natural number, a Bound value, and another natural number.

The operation metaXapply(R, t, l, σ, n, b, m) is evaluated as the function metaApply but using extension (see Section 4.8) and in any possible position, not only at the top. The arguments n and b can be used to localize the part of the term where the rule application can take place:

Notice that nested occurrences of an operator with the assoc attribute are counted as a single operator for depth purposes, that is, matching takes place on the flattened term (see Section 4.8). The same idea applies to iter operators (see section 4.4.2): a whole stack of an iter operator counts as a single operator. Furthermore, because of matching with extension, the solution may have an extra layer, as illustrated in the matching examples at the end of Section 11.5.5.

The last Nat argument m in metaXapply(R, t, l, σ, n, b, m), as in the case of the operation metaApply, is the solution number, used to enumerate multiple solutions. The first solution is 0, and they should again be generated in order for efficiency.

The result of metaXapply has an additional component, giving the context (a term with a single “hole”, represented []) inside the given term t, where the rewriting has taken place. The sort NeCTermList represents nonempty lists of terms with exactly one “hole,” that is, exactly one term of sort Context, the rest being of sort Term. The sort GTermList is the supersort of NeCTermList and TermList needed for the assoc attribute (hidden in the following declarations in the ditto attribute) to make sense.

  sorts Context NeCTermList GTermList .  
  subsorts Context < NeCTermList < GTermList .  
  subsort TermList < GTermList .  
 
  op [] : -> Context [ctor] .  
  op _,_ : TermList NeCTermList -> NeCTermList [ctor ditto] .  
  op _,_ : NeCTermList TermList -> NeCTermList [ctor ditto] .  
  op _,_ : GTermList GTermList -> GTermList [ctor ditto] .  
  op _[_] : Qid NeCTermList -> Context [ctor] .  
 
  sorts Result4Tuple Result4Tuple? .  
  subsort Result4Tuple < Result4Tuple? .  
  op {_,_,_,_} : Term Type Substitution Context -> Result4Tuple  
       [ctor] .  
  op failure : -> Result4Tuple? [ctor] .  
 
  op metaXapply :  
       Module Term Qid Substitution Nat Bound Nat ~> Result4Tuple?  
       [special (...)] .

Appropriate selectors extract from the result 4-tuples their four components:

  op getTerm : Result4Tuple -> Term .  
  op getType : Result4Tuple -> Type .  
  op getSubstitution : Result4Tuple -> Substitution .  
  op getContext : Result4Tuple -> Context .

As an example, we can force at the metalevel the rewriting of the term $ q in the module VENDING-MACHINE so that only the rule buy-c is used (compare with the last metaApply example).

  Maude> reduce in META-LEVEL :  
           metaXapply(upModule(’VENDING-MACHINE, false),  
             ’__[’q.Coin, ’$.Coin], ’buy-c, none, 0, unbounded, 0) .  
  result Result4Tuple:  
    {’__[’q.Coin, ’c.Item], ’Marking, none, ’__[’q.Coin, []]}

Notice the fragment ’__[’q.Coin, []] of the result, providing the context where the rule has been applied. Since this is the only possible solution, if we request the “next” solution (by increasing to 1 the last argument), the result will be a failure.

  Maude> reduce in META-LEVEL :  
           metaXapply(upModule(’VENDING-MACHINE, false),  
             ’__[’q.Coin, ’$.Coin], ’buy-c, none, 0, unbounded, 1) .  
  result Result4Tuple?: (failure).Result4Tuple?

11.5.5 Matching: metaMatch and metaXmatch

The (partial) operation metaMatch takes as arguments the metarepresentation of a module, the metarepresentations of two terms, the metarepresentation of a condition, and a natural number.

  sort Substitution? .  
  subsort Substitution < Substitution? .  
  op noMatch : -> Substitution? [ctor] .  
  op metaMatch : Module Term Term Condition Nat ~> Substitution?  
       [special (...)] .

The operation metaMatch(R, t, t, Cond, n) tries to match at the top the terms t and tin the module R in such a way that the resulting substitution satisfies the condition Cond. The last argument is used to enumerate possible matches. If the matching attempt is successful, the result is the corresponding substitution; otherwise, noMatch is returned. The generalization to metaXmatch follows exactly the same ideas as for metaXapply. Notice that the operation metaMatch provides the metalevel counterpart of the object-level command match, while the operation metaXmatch provides a generalization of the object-level command xmatch (see Sections 4.7, 4.8, and 18.3) in that it is possible to specify min and max depths (in terms of theory layers) and search for proper subterms that do not belong to the top theory layer. The object-level behavior of the xmatch command is obtained by setting both min and max depth to 0.

  sorts MatchPair MatchPair? .  
  subsort MatchPair < MatchPair? .  
  op {_,_} : Substitution Context -> MatchPair [ctor] .  
  op noMatch : -> MatchPair? [ctor] .  
  op metaXmatch :  
       Module Term Term Condition Nat Bound Nat ~> MatchPair?  
       [special (...)] .

Appropriate selectors extract from the result pairs their two components:

  op getSubstitution : MatchPair -> Substitution .  
  op getContext : MatchPair -> Context .

In the following examples, we try to match the pattern M:Marking $ with the term $ q c a in several different ways:

As mentioned in the previous section, when matching with extension, the solution may have an extra layer. Let us consider, for example, the following module:

  fmod METAXMATCH-EX is  
    pr META-LEVEL .  
    op foo : QidSet ~> QidSet .  
  endfm

Then we take at the metalevel the pattern _;_(’A, QS:QidSet) and the (flattened) subject term foo(_;_(’A, ’B, ’C)), and ask for matches with extension under at most 1 theory layer, as shown in the following reductions:

  Maude> red metaXmatch(upModule(’METAXMATCH-EX, false),  
               upTerm((’A ; QS:QidSet)),  
               upTerm(foo(’A ; ’B ; ’C)), nil, 0, 1, 0) .  
  result MatchPair: {’QS:QidSet <- ’_;_[’’B.Sort, ’’C.Sort], ’foo[[]]}  
 
  Maude> red metaXmatch(upModule(’METAXMATCH-EX, false),  
               upTerm((’A ; QS:QidSet)),  
               upTerm(foo(’A ; ’B ; ’C)), nil, 0, 1, 1) .  
  result MatchPair: {’QS:QidSet <- ’’C.Sort, ’foo[’_;_[’’B.Sort, []]]}  
 
  Maude> red metaXmatch(upModule(’METAXMATCH-EX, false),  
               upTerm((’A ; QS:QidSet)),  
               upTerm(foo(’A ; ’B ; ’C)), nil, 0, 1, 2) .  
  result MatchPair: {’QS:QidSet <- ’’B.Sort, ’foo[’_;_[’’C.Sort, []]]}  
 
  Maude> red metaXmatch(upModule(’METAXMATCH-EX, false),  
               upTerm((’A ; QS:QidSet)),  
               upTerm(foo(’A ; ’B ; ’C)), nil, 0, 1, 3) .  
  result MatchPair?: (noMatch).MatchPair?

Obviously, there is no match at the top, but under one theory layer (the foo operator) we have _;_(’A, ’B, ’C). The first solution is the expected one, with the variable QS:QidSet matching the subterm _;_(’B, ’C). However, in the next two solutions we see that we also have the variable QS:QidSet matching either the fragment ’C or ’B while the other fragment goes into the extension. Then the context in the solution has 2 theory layers but this is just a feature of matching with extension: some solutions will have an extra layer.

As another example of this situation, let us consider the following reductions:

  Maude> reduce in META-LEVEL :  
           metaXmatch(upModule(’METAXMATCH-EX, false),  
             upTerm(s N:Nat), upTerm(prec(s_^2(0))), nil, 0, 1, 0) .  
  result MatchPair: {’N:Nat <- ’s_[’0.Zero], ’prec[[]]}  
 
  Maude> red metaXmatch(upModule(’METAXMATCH-EX, false),  
               upTerm(s N:Nat), upTerm(prec(s_^2(0))), nil, 0, 1, 1) .  
  result MatchPair: {’N:Nat <- ’0.Zero, ’prec[’s_[[]]]}

Here the context in the first solution has one theory layer while the context in the second has two, but the actual matching problem solved (with extension), namely, s N <=? s_^2(0) under the single theory layer provided by the operator prec is the same in both reductions.

11.5.6 Searching: metaSearch and metaSearchPath

metaSearch

The operation metaSearch takes as arguments the metarepresentation of a module, the metarepresentation of the starting term for search, the metarepresentation of the pattern to search for, the metarepresentation of a condition to be satisfied, the metarepresentation of the kind of search to carry on, a Bound value, and a natural number.

  op metaSearch :  
       Module Term Term Condition Qid Bound Nat ~> ResultTriple?  
       [special (...)] .

The searching strategy used by metaSearch coincides with that of the object-level search command in Maude (see Sections 5.4 and 18.4). The Qid values that are allowed as arguments are: ’* for a search involving zero or more rewrites (corresponding to =>* in the search command), ’+ for a search consisting in one or more rewrites (=>+), and ’! for a search that only matches canonical forms (=>!). The Bound argument indicates the maximum depth of the search, and the Nat argument is the solution number. To indicate a search consisting in exactly one rewrite, we set the maximum depth of the search to the number 1.

Using metaSearch we can redo at the metalevel the last example in Section 5.4. The results give us the answer to the question: if I have already inserted one dollar and three quarters in the vending machine, can I get two cakes and an apple? The answer is yes; in fact, there are several ways.

  Maude> reduce in META-LEVEL :  
           metaSearch(upModule(’VENDING-MACHINE, false),  
             ’__[’$.Coin, ’q.Coin, ’q.Coin,’q.Coin],  
             ’__[’c.Item, ’a.Item, ’c.Item, ’M:Marking],  
             nil, ’+, unbounded, 0) .  
  result ResultTriple:  
    {’__[’q.Coin,’q.Coin,’q.Coin,’q.Coin,’a.Item,’c.Item,’c.Item],  
     ’Marking,  
     ’M:Marking <- ’__[’q.Coin, ’q.Coin, ’q.Coin, ’q.Coin]}

  Maude> reduce in META-LEVEL :  
           metaSearch(upModule(’VENDING-MACHINE, false),  
             ’__[’$.Coin, ’q.Coin, ’q.Coin, ’q.Coin],  
             ’__[’c.Item, ’a.Item, ’c.Item, ’M:Marking],  
             nil, ’+, unbounded, 1) .  
  result ResultTriple:  
    {’__[’a.Item, ’c.Item, ’c.Item],  
     ’Marking,  
     ’M:Marking <- ’null.Marking}

metaSearchPath

The operation metaSearchPath is complementary to metaSearch and carries out the same search, but instead of returning the final state and matching substitution it returns the sequence of states and rules on a path starting with the reduced initial state and leading to (but not including) the final state.

  op metaSearchPath :  
       Module Term Term Condition Qid Bound Nat ~> Trace?  
       [special (...)] .

The sort Trace is used to represent the path as a list of triples by means of the following syntax:

  sorts TraceStep Trace Trace? .  
  subsorts TraceStep < Trace < Trace? .  
  op {_,_,_} : Term Type Rule -> TraceStep [ctor] .  
  op nil : -> Trace [ctor] .  
  op __ : Trace Trace -> Trace [ctor assoc id: nil format (d n d)] .  
  op failure : -> Trace? [ctor] .

We run again the same two examples as above, with the following results.

  Maude> reduce in META-LEVEL :  
           metaSearchPath(upModule(’VENDING-MACHINE, false),  
             ’__[’$.Coin, ’q.Coin, ’q.Coin,’q.Coin],  
             ’__[’c.Item, ’a.Item, ’c.Item, ’M:Marking],  
             nil, ’+, unbounded, 0) .  
  result Trace:  
    {’__[’$.Coin,’q.Coin,’q.Coin,’q.Coin],  
     ’Marking,  
     rl ’M:Marking => ’__[’$.Coin,’M:Marking] [label(’add-$)] .}  
    {’__[’$.Coin,’$.Coin,’q.Coin,’q.Coin,’q.Coin],  
     ’Marking,  
     rl ’M:Marking => ’__[’$.Coin,’M:Marking] [label(’add-$)] .}  
    {’__[’$.Coin,’$.Coin,’$.Coin,’q.Coin,’q.Coin,’q.Coin],  
     ’Marking,  
     rl ’$.Coin => ’c.Item [label(’buy-c)] .}  
    {’__[’$.Coin,’$.Coin,’q.Coin,’q.Coin,’q.Coin,’c.Item],  
     ’Marking,  
     rl ’$.Coin => ’c.Item [label(’buy-c)] .}  
    {’__[’$.Coin,’q.Coin,’q.Coin,’q.Coin,’c.Item,’c.Item],  
     ’Marking,  
     rl ’$.Coin => ’__[’q.Coin,’a.Item] [label(’buy-a)] .}

  Maude> reduce in META-LEVEL :  
           metaSearchPath(upModule(’VENDING-MACHINE, false),  
             ’__[’$.Coin, ’q.Coin, ’q.Coin, ’q.Coin],  
             ’__[’c.Item, ’a.Item, ’c.Item, ’M:Marking],  
             nil, ’+, unbounded, 1) .  
  result Trace:  
    {’__[’$.Coin,’q.Coin,’q.Coin,’q.Coin],  
     ’Marking,  
     rl ’M:Marking => ’__[’$.Coin,’M:Marking] [label(’add-$)] .}  
    {’__[’$.Coin,’$.Coin,’q.Coin,’q.Coin,’q.Coin],  
     ’Marking,  
     rl ’$.Coin => ’c.Item [label(’buy-c)] .}  
    {’__[’$.Coin,’q.Coin,’q.Coin,’q.Coin,’c.Item],  
     ’Marking,  
     rl ’$.Coin => ’__[’q.Coin,’a.Item] [label(’buy-a)] .}  
    {’__[’q.Coin,’q.Coin,’q.Coin,’q.Coin,’a.Item,’c.Item],  
     ’Marking,  
     rl ’__[’q.Coin,’q.Coin,’q.Coin,’q.Coin] => ’$.Coin  
       [label(’change)] .}  
    {’__[’$.Coin,’a.Item,’c.Item],  
     ’Marking,  
     rl ’$.Coin => ’c.Item [label(’buy-c)] .}

The operations metaSearchPath and metaSearch share caching, so calling one after the other on the same arguments only performs a single search.

11.5.7 Parsing and pretty-printing: metaParse and metaPrettyPrint

metaParse

The (partial) operation metaParse takes as arguments the metarepresentation of a module, a list of quoted identifiers metarepresenting a list of tokens, and a value of the sort Type?, i.e., either the metarepresentation of a component or the constant anyType.

  sort Type? .  
  subsort Type < Type? .  
  op anyType : -> Type? [ctor] .  
  sort ResultPair? .  
  subsort ResultPair < ResultPair? .  
  op noParse : Nat -> ResultPair? [ctor] .  
  op ambiguity : ResultPair ResultPair -> ResultPair? [ctor] .  
  op metaParse : Module QidList Type? ~> ResultPair? [special (...)] .

The operation metaParse reflects the parse command in Maude (see Section 3.9.4); that is, it tries to parse the given list of tokens as a term of the given type in the module given as first argument; the constant anyType allows any component. If metaParse succeeds, it returns the metarepresentation of the parsed term with its corresponding sort or kind. Otherwise, it returns:

These are simple examples of using metaParse:

  Maude> reduce in META-LEVEL :  
           metaParse(upModule(’VENDING-MACHINE, false),  
             ’$ ’q ’q ’q, ’Marking) .  
  result ResultPair:  
    {’__[’$.Coin,’__[’q.Coin,’__[’q.Coin,’q.Coin]]],’Marking}

  Maude> reduce in META-LEVEL :  
           metaParse(upModule(’VENDING-MACHINE, false),  
             ’$ ’q ’d ’q, ’Marking) .  
  result ResultPair?: noParse(2)

metaPrettyPrint

The (partial) operation metaPrettyPrint takes as arguments the metarepresentations of a module R and of a term t together with a set of printing options, and it returns a list of quoted identifiers that metarepresents the string of tokens produced by pretty-printing the term t in the signature of R. In the event of an error an empty list of quoted identifiers is returned.

  op metaPrettyPrint : Module Term PrintOptionSet ~> QidList  
       [special (...)] .

Pretty-printing a term involves more than just naively using the mixfix syntax for operators. Precedence and gathering information and the relative positions of underscores in an operator and its parent in the term must be considered to determine whether parentheses need to be inserted around any given subterm to avoid ambiguity. If there is ad-hoc overloading in the module, additional checks must be done to determine if and where sort disambiguation syntax is needed.

The print options argument is built with the following syntax:

  sorts PrintOption PrintOptionSet .  
  subsort PrintOption < PrintOptionSet .  
  ops mixfix with-parens flat format number rat : -> PrintOption  
        [ctor] .  
  op none : -> PrintOptionSet [ctor] .  
  op __ : PrintOptionSet PrintOptionSet -> PrintOptionSet  
          [ctor assoc comm id: none] .  
 

The available print options form a subset of the global print options described in Section 18.8, which are ignored by this operation.

As an example, we can use metaPrettyPrint to pretty print the result of parsing at the metalevel the list of tokens $ q q q in the module VENDING-MACHINE, first with prefix syntax, then with mixfix syntax, and finally with mixfix syntax and taking into account the format attribute.

  Maude> reduce in META-LEVEL :  
           metaPrettyPrint(upModule(’VENDING-MACHINE, false),  
             ’__[’$.Coin, ’__[’q.Coin, ’__[’q.Coin, ’q.Coin]]],  
             none) .  
  result NeQidList:  
    ’__ ’‘( ’$ ’‘, ’__ ’‘( ’q ’‘, ’__ ’‘( ’q ’‘, ’q ’‘) ’‘) ’‘)

  Maude> reduce in META-LEVEL :  
           metaPrettyPrint(upModule(’VENDING-MACHINE, false),  
             ’__[’$.Coin, ’__[’q.Coin, ’__[’q.Coin, ’q.Coin]]],  
             mixfix) .  
  result NeTypeList: ’$ ’q ’q ’q

  Maude> reduce in META-LEVEL :  
           metaPrettyPrint(upModule(’VENDING-MACHINE, false),  
             ’__[’$.Coin, ’__[’q.Coin, ’__[’q.Coin, ’q.Coin]]],  
             mixfix format) .  
  result NeTypeList:  
    ’\r ’\! ’$ ’\o ’\r ’\! ’q ’\o ’\r ’\! ’q ’\o ’\r ’\! ’q ’\o

It is important to notice that metaPrettyPrint uses the information provided by the format attribute in the last reduction above. For example, the operator $ in the module VENDING-MACHINE-SIGNATURE in Section 5.1 was declared with attribute format (r! o), and therefore it is meta-pretty-printed as ’\r ’\! ’$ ’\o.

For backwards compatibility there is available the following variation of the metaPrettyPrint operation, which provides a set of default print options.

  op metaPrettyPrint : Module Term ~> QidList .  
  eq metaPrettyPrint(M:Module, T:Term)  
    = metaPrettyPrint(M:Module, T:Term,  
        mixfix flat format number rat) .

For example,

  Maude> reduce in META-LEVEL :  
           metaPrettyPrint(upModule(’VENDING-MACHINE, false),  
             ’__[’$.Coin, ’__[’q.Coin, ’__[’q.Coin, ’q.Coin]]]) .  
  result NeTypeList:  
    ’\r ’\! ’$ ’\o ’\r ’\! ’q ’\o ’\r ’\! ’q ’\o ’\r ’\! ’q ’\o

11.5.8 Sort operations

The META-LEVEL module also provides in a built-in way commonly needed operations on the poset of sorts of a given module.

All these operations, related to sorts and kinds, take as first argument a term of sort Module. Assuming that this term is indeed the metarepresentation of a module, the remaining arguments might be terms representing sorts or kinds that do not correspond to sorts or kinds declared in such a module; in this case, the operation is undefined.

In the following we include descriptions together with simple examples of using these operations.

sortLeq

The operation sortLeq takes as arguments the metarepresentation of a module R and the metarepresentations of two types, that is, either sorts or kinds.

  op sortLeq : Module Type Type ~> Bool [special (...)] .

According to whether the types passed to sortLeq as arguments are metarepresented sorts or kinds, we can distinguish the following cases:

sameKind

The operation sameKind takes as arguments the metarepresentation of a module R and the metarepresentations of two types, that is, either sorts or kinds.

  op sameKind : Module Type Type ~> Bool [special (...)] .

Let S be the set of sorts in R and let R be its subsort relation. When the two types passed as arguments to sameKind are sorts s,s′∈ S, the operation sameKind returns true if s and sbelong to the same connected component in the subsort ordering R, that is, if they belong to the same kind, and false otherwise. When the two arguments are kinds in R, sameKind returns true when they are indeed the same, and false otherwise. Finally, when one argument is one sort and the other is a kind, this operation ckecks whether the sort belongs to the kind.

For example, we have the following reductions about sorts and kinds in the module NUMBERS.

  Maude> reduce in META-LEVEL :  
           sameKind(upModule(’NUMBERS, false), ’Zero, ’NzNat) .  
  result Bool: true

  Maude> reduce in META-LEVEL :  
           sameKind(upModule(’NUMBERS, false), ’Zero, ’Nat3) .  
  result Bool: false

  Maude> reduce in META-LEVEL :  
          sameKind(upModule(’NUMBERS, false), ’‘[Zero‘], ’‘[NzNat‘]) .  
  result Bool: true

  Maude> reduce in META-LEVEL :  
           sameKind(upModule(’NUMBERS, false), ’‘[Zero‘], ’NzNat) .  
  result Bool: true

completeName

The operation completeName takes as arguments the metarepresentation of a module R and the metarepresentation of a sort s or a kind k. When its second argument is the metarepresentation of a sort s, it returns the same metarepresentation of s. But if its second argument is the metarepresentation of a kind k, then it returns the metarepresentation of the complete name of k in R, i.e., the metarepresentation of the comma-separated list of the maximal elements of the corresponding connected component.

  op completeName : Module Type ~> Type [special (...)] .

For example,

  Maude> reduce in META-LEVEL :  
           completeName(upModule(’NUMBERS, false), ’Zero) .  
  result Sort: ’Zero

  Maude> reduce in META-LEVEL :  
           completeName(upModule(’NUMBERS, false), ’‘[Zero‘]) .  
  result Kind: ’‘[NatSeq‘,NatSet‘]

getKind and getKinds

The operation getKind takes as arguments the metarepresentation of a module R and the metarepresentation of a type, i.e., a sort or a kind. When its second argument is the metarepresentation of a type in R, it returns the metarepresentation of the complete name of the corresponding kind.

  op getKind : Module Type ~> Kind [special (...)] .

For example,

  Maude> reduce in META-LEVEL :  
           getKind(upModule(’NUMBERS, false), ’Zero) .  
  result Kind: ’‘[NatSeq‘,NatSet‘]

  Maude> reduce in META-LEVEL :  
           getKind(upModule(’NUMBERS, false), ’‘[Zero‘]) .  
  result Kind: ’‘[NatSeq‘,NatSet‘]

The operation getKinds takes as its only argument the metarepresentation of a module R and returns the metarepresentation of the set of kinds declared in R, with kinds metarepresented using their complete names.

  op getKinds : Module ~> KindSet [special (...)] .

For example,

  Maude> reduce in META-LEVEL : getKinds(upModule(’NUMBERS, false)) .  
  result NeKindSet: ’‘[Bool‘] ; ’‘[Nat3‘] ; ’‘[NatSeq‘,NatSet‘]

lesserSorts

The operation lesserSorts takes as arguments the metarepresentation of a module R and the metarepresentation of a type, i.e., a sort or a kind.

  op lesserSorts : Module Type ~> SortSet [special (...)] .

Let S be the set of sorts in R. When s S, lesserSorts returns the metarepresentation of the set of sorts strictly smaller than s in S. For example,

  Maude> reduce in META-LEVEL :  
           lesserSorts(upModule(’NUMBERS, false), ’Nat) .  
  result NeSortSet: ’NzNat ; ’Zero

  Maude> reduce in META-LEVEL :  
           lesserSorts(upModule(’NUMBERS, false), ’Zero) .  
  result EmptyTypeSet: (none).EmptyTypeSet

  Maude> reduce in META-LEVEL :  
           lesserSorts(upModule(’NUMBERS, false), ’NatSeq) .  
  result NeSortSet: ’Nat ; ’NzNat ; ’Zero

When the second argument of lesserSorts metarepresents a kind in R, this operation returns the metarepresentation of the set of all sorts in such kind. For example,

  Maude> reduce in META-LEVEL :  
           lesserSorts(upModule(’NUMBERS, false), ’‘[NatSeq‘]) .  
  result NeSortSet: ’Nat ; ’NatSeq ; ’NatSet ; ’NzNat ; ’Zero

  Maude> reduce in META-LEVEL :  
           lesserSorts(upModule(’NUMBERS, false), ’‘[Bool‘]) .  
  result Sort: ’Bool

leastSort

The operation leastSort takes as arguments the metarepresentation of a module R and the metarepresentation of a term t, and it returns the metarepresentation of the least sort or kind of t in R, obtained without reducing the term, that is, the memberships in the module are used to get the information, but equations are not used to reduce the term.

  op leastSort : Module Term ~> Type [special (...)] .

For example,

  Maude> reduce in META-LEVEL :  
     leastSort(upModule(’NUMBERS, false), ’p[’s_[’zero.Zero]]) .  
  result Sort: ’Nat

glbSorts

The operation glbSorts takes as arguments the metarepresentation of a module R and the metarepresentations of two types, that is, either sorts or kinds.

  op glbSorts : Module Type Type ~> TypeSet [special (...)] .

According to whether the types passed to glbSorts as arguments are metarepresented sorts or kinds, we can distinguish the following cases:

maximalSorts and minimalSorts

The operations maximalSorts and minimalSorts take as arguments the metarepresentation of a module R and the metarepresentation of a kind k. If k is a kind in R, maximalSorts returns the metarepresentation of the set of the maximal sorts in the connected component of k, while minimalSorts returns the metarepresentation of the set of its minimal sorts.

  op maximalSorts : Module Kind ~> SortSet [special (...)] .  
  op minimalSorts : Module Kind ~> SortSet [special (...)] .

For example,

  Maude> reduce in META-LEVEL :  
     maximalSorts(upModule(’NUMBERS, false), ’‘[Zero‘]) .  
  result NeSortSet: ’NatSeq ; ’NatSet

  Maude> reduce in META-LEVEL :  
     minimalSorts(upModule(’NUMBERS, false), ’‘[Zero‘]) .  
  result NeSortSet: ’Zero ; ’NzNat

maximalAritySet

The operation maximalAritySet takes as arguments the metarepresentation of a module R, the metarepresentation of an operator f in R, the metarepresentation of an arity (list of types) for f and the metarepresentation of a sort s, and then computes the set of maximal arities (lists of types) that f could take and have a sort s′≤Rs. This result might be the empty set if s is small or f is only defined at the kind level.

Notice that the result of this operation is a set of lists of types, which is built by means of the following syntax, extending the syntax for building lists of types that we only show partially here and whose full specification can be found in the module META-MODULE in the file prelude.maude available with the Maude distribution.

  sort NeTypeList TypeList .  
  op nil : -> TypeList [ctor] .  
  op __ : TypeList TypeList -> TypeList [ctor ditto] .  
 
  sort TypeListSet .  
  subsort TypeList TypeSet < TypeListSet .  
  op _;_ : TypeListSet TypeListSet -> TypeListSet [ctor ditto] .  
  eq T:TypeList ; T:TypeList = T:TypeList .  
 
  op maximalAritySet : Module Qid TypeList Sort ~> TypeListSet  
    [special (...)] .

Let us consider for example the operator _+_ in the module NUMBERS, where it is overloaded by means of the following declarations:

  op _+_ : Nat Nat -> Nat [assoc comm].  
  op _+_ : NzNat Nat -> NzNat [ditto] .  
  op _+_ : Nat3 Nat3 -> Nat3 [comm] .

With this information, we obtain the following reductions concerning this operator:

  Maude> reduce in META-LEVEL :  
           maximalAritySet(upModule(’NUMBERS, false),  
             ’_+_, ’NzNat ’NzNat, ’NzNat) .  
  result TypeListSet: ’Nat ’NzNat ; ’NzNat ’Nat

  Maude> reduce in META-LEVEL :  
           maximalAritySet(upModule(’NUMBERS, false),  
             ’_+_, ’Nat ’Nat, ’NzNat) .  
  result TypeListSet: ’Nat ’NzNat ; ’NzNat ’Nat

  Maude> reduce in META-LEVEL :  
           maximalAritySet(upModule(’NUMBERS, false),  
             ’_+_, ’Nat ’Nat, ’Nat) .  
  result NeTypeList: ’Nat ’Nat

  Maude> reduce in META-LEVEL :  
           maximalAritySet(upModule(’NUMBERS, false),  
             ’_+_, ’Nat3 ’Nat3, ’Nat3) .  
  result NeTypeList: ’Nat3 ’Nat3

Notice that if the operator f and the list of types passed as arguments to maximalAritySet do not match, then the result is an error, which is represented as a non-reduced term in a metalevel kind. We have for instance the following example where we have omitted the lengthy metarepresentation of the NUMBERS module.

  Maude> reduce in META-LEVEL :  
           maximalAritySet(upModule(’NUMBERS, false),  
             ’_+_, ’Nat3 ’Nat3, ’NzNat) .  
  result [GTermList,ParameterList,QidList,  
          TypeListSet,Type?,ModuleExpression,Header]:  
    maximalAritySet(fmod ’NUMBERS is ... endfm,  
      ’_+_, ’Nat3 ’Nat3, ’NzNat)

11.5.9 Other metalevel operations: wellFormed

The operation wellFormed can take as arguments the metarepresentation of a module R, or the metarepresentation of a module R and a term t, or the metarepresentation of a module R and a substitution σ. In the first case, it returns true if R is a well-formed module, and false otherwise. In the second case, if t is a well-formed term in R, it returns true; otherwise, it returns false. Finally, in the third case, if σ is a well-formed substitution in R, it returns true; otherwise, it returns false.

  op wellFormed : Module -> Bool [special (...)] .  
  op wellFormed : Module Term ~> Bool [special (...)] .  
  op wellFormed : Module Substitution ~> Bool [special (...)] .

Note that the first operation is total, while the other two are partial (notice the form of the arrow in the declarations). The reason is that the last two are not defined when the term given as first argument does not represent a module, and then it does not make sense to check whether a term or substitution is well formed with respect to such a wrong “module.” For example,

  Maude> reduce in META-LEVEL :  
           wellFormed(upModule(’NUMBERS, false)) .  
  result Bool: true

  Maude> reduce in META-LEVEL :  
           wellFormed(upModule(’NUMBERS, false), ’p[’zero.Zero]) .  
  result Bool: true

  Maude> reduce in META-LEVEL :  
           wellFormed(upModule(’NUMBERS, false),  
             ’s_[’zero.Zero, ’zero.Zero]) .  
  Advisory: could not find an operator s_ with appropriate domain  
      in meta-module NUMBERS when trying to interprete metaterm  
      ’s_[’zero.Zero,’zero.Zero].  
  result Bool: false

  Maude> reduce in META-LEVEL :  
           wellFormed(upModule(’NUMBERS, false),  
             ’N:Zero <- ’zero.Zero) .  
  result Bool: true

  Maude> reduce in META-LEVEL :  
           wellFormed(upModule(’NUMBERS, false),  
             ’N:Nat <- ’p[’zero.Zero]) .  
  result Bool: false

  Maude> reduce in META-LEVEL :  
           wellFormed(upModule(’NUMBERS, false),  
             ’N:Zero <- ’s_[’zero.Zero,’zero.Zero]) .  
  Advisory: could not find an operator s_ with appropriate domain  
      in meta-module NUMBERS when trying to interprete metaterm  
      ’s_[’zero.Zero,’zero.Zero].  
  result Bool: false

11.6 Internal strategies

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:

1.
insert either a dollar or a quarter in the vending machine;
2.
only buy cakes, and buy as many cakes as possible, with the coins already inserted;
3.
only buy either cakes or apples, and buy at most n of them, with the coins already inserted;
4.
buy the same number of apples and cakes, and buy as many as possible, with the coins already inserted.

Consider the module BUYING-STRATS below, which imports the META-LEVEL module.

  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 n 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 (24) 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 17.6. See [22] for a general methodology for defining internal strategy languages using reflection, and [2325] 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 [88]. 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.