Prev Up Next
Go backward to 2.5.4 Representing Modules
Go up to 2.5 Reflection and the META-LEVEL
Go forward to 2.5.6 Parsing, Pretty Printing, and Sort Functions

2.5.5 Descent Functions

META-LEVEL has three built-in descent functions, meta-reduce, meta-apply, and meta-rewrite, that provide three useful and efficient ways of reducing metalevel computations to object-level ones.

The operation meta-reduce takes as arguments the representation of a module R and the representation of a term t, of a membership predicate t:s, or of a lazy membership predicate t::s, in that module. It has syntax 

  op meta-reduce : Module Term -> Term [special ( ... )] .
When the second argument is the representation  |¯t¯|  of a term t in R, the function meta-reduce returns the representation of the fully reduced form of the term t using the equations in R, e.g., 
  Maude> red meta-reduce( |¯NAT¯| ,  |¯s 0 + 0¯| ) .
  result Term:  |¯s 0¯|
Note that in order to simplify the presentation we use the meta-notations  |¯t¯|  and  |¯Id¯|  for t a term and Id the name of a module. As explained in Section 3.4, in Full Maude we can use the up command to get the meta-representation denoted by the overline notation. In Core Maude, however, such a meta-representation has to be explicitly given, that is, the example above must be written as follows. 
  Maude> red meta-reduce(
                fmod 'NAT is
                   nil
                   sorts 'Zero ; 'Nat .
                   subsort 'Zero < 'Nat .
                   op '0 : nil -> 'Zero [none] .
                   op 's_ : 'Nat -> 'Nat [none] .
                   op '_+_ : 'Nat 'Nat -> 'Nat [comm] .
                   op '_*_ : 'Nat 'Nat -> 'Nat [comm] .
                   var 'N : 'Nat .
                   var 'M : 'Nat .
                   none
                   eq '_+_[{'0}'Nat, 'N] = 'N .
                   eq '_+_['s_['N], 'M] = 's_['_+_['N, 'M]] .
                   eq '_*_[{'0}'Nat, 'N] = {'0}'Nat .
                   eq '_*_['s_['N], 'M] = '_+_['N, '_*_['N, 'M]] .
                endfm,
                '_+_['s_[{'0}'Nat], {'0}'Nat]) .
  result Term: 's_[{'0}'Zero]
This is particularly cumbersome for the meta-representation of modules, which can be quite big. However, as illustrated by the examples in Section 2.6, one easy solution is to define a new module importing META-LEVEL in which we introduce a new constant of sort Module or FModule to name the module in question--in this example, the constant NAT--and then give an equation identifying such a constant with the meta-representation of the given module.

Similarly, when the second argument of meta-reduce is the representation of a membership predicate t:s (or a lazy membership predicate t::s) the term t is fully reduced using the equations in R and the least sort of the reduced term is computed (respectively, the least sort of the term t according to the order-sorted signature and the membership axioms of the module R is computed) and then the representation of the Boolean value of the corresponding predicate is returned.

The interpreter function for meta-reduce( |¯R¯| , |¯t¯| ) rewrites the term t to normal form using only the equations in R, and does so according to the operator evaluation strategies (see Section 2.1.3 and [21]) declared for each operator in the signature of R--which by default is bottom-up for operators with no such strategies declared. In other words, the interpreter strategy for this function coincides with that of the red command in Maude, that is,

meta-reduce( |¯R¯| , |¯t¯| )=  |¯IMaude(R,t,red)¯| .

The operation meta-rewrite has syntax 

  op meta-rewrite : Module Term MachineInt -> Term 
        [special ( ... )] .
It is entirely analogous to meta-reduce, but instead of using only the equational part of a module it now uses both the equations and the rules to rewrite the term using Maude's default strategy. Its first two arguments are the representations of a module R and of a term t, and its third argument is a positive machine integer n. Its result is the representation of the term obtained from t after at most n applications of the rules in R using the strategy of Maude's default interpreter, which applies the rules in a fair, top-down fashion. When the value 0 is given as the third argument, no bound is given to the number of rewrites, and rewriting proceeds to the bitter end. Again, meta-rewrite is a paradigmatic example of a descent function; its corresponding interpreter strategy is that of the rewrite command in Maude [9], that is,
meta-rewrite( |¯R¯| , |¯t¯| ,n)=  |¯IMaude(R,t,rewrite [n])¯| .

The operation meta-apply has syntax: 

  op meta-apply : 
        Module Term Qid Substitution MachineInt -> ResultPair 
        [special ( ... )] .
The first four arguments are representations in META-LEVEL of a module R, a term t in R, a label l of some rules in R, and a set of assignments (possibly empty) defining a partial substitution sigma for the variables in those rules. The last argument is a natural number n. meta-apply then returns a pair of sort ResultPair consisting of a term and a substitution. The syntax for substitutions and for results is 
  sorts Assignment Substitution ResultPair .
  subsort Assignment < Substitution .

  op _<-_ : Qid Term -> Assignment .
  op none : -> Substitution .
  op _;_ : Substitution Substitution -> Substitution 
            [assoc comm id: none] .
  op {_,_} : Term Substitution -> ResultPair .
The operation meta-apply is evaluated as follows:
  1. the term t is first fully reduced using the equations in R;
  2. the resulting term is matched against all rules with label l partially instantiated with sigma, 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 {error*, none} 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 pair formed using the constructor {_,_} whose first element is the representation of the resulting fully reduced term and whose second element is the representation of the match used in the reduction is returned.

The interpreter strategy associated to meta-apply( |¯R¯| , |¯t¯| , |¯l¯| ,  |¯sigma¯| ,n) is not that of a user-level command in the Maude interpreter. It is instead a built-in strategy internal to the interpreter that attempts one rewrite at the top as explained above.

Prev Up Next