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 [29, 22, 30, 31]. 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.
Rewriting logic is reflective in a precise mathematical way, namely, there is a finitely presented rewrite
theory 
that is universal in the sense that we can represent in any finitely presented rewrite
theory 
(including itself) as a term , any terms t,t′ in as terms t,t′, and any pair (,t) as a
term ⟨,t⟩, in such a way that we have the following equivalence
⊢ t-→t′ ⇔ ⊢⟨,t⟩-→⟨,t′⟩.
Since is representable in itself, we can achieve a “reflective tower” with an arbitrary number of
levels of reflection:
⊢ t → t′ ⇔ ⊢⟨,t⟩→⟨,t′⟩ ⇔ ⊢⟨,⟨,t⟩⟩→⟨,⟨,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 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
abbreviated to β in the figure.
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.
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.
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.
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.
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,
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.
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
and meta-metarepresented by
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).
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:
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.
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.
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.
For example, we show here the metarepresentations of the modules introduced in Section 5.1 VENDING-MACHINE-SIGNATURE and VENDING-MACHINE.
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.
Module expressions involving renamings and summations can also be metarepresented with the expected syntax:
Finally, the instantiation of a parameterized module is metarepresented as follows:
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:
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.
In the module META-VIEW, which imports META-MODULE, views are metarepresented in a syntax very similar to their original user syntax.
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.
Analogously, the following syntax is used to define set of operator mappings.
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.
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:
Then, we can extract some components of this metarepresented view:
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
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)
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.
For a module 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 and a Boolean value b, and return, respectively, the metarepresentations of the module ,
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 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 .
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.
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:
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 . When 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.
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.
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,
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 t′ as 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′.
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.
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.
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.
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].
The (partial) operation metaReduce takes as arguments the metarepresentation of a module and
the metarepresentation of a term t.
When t is a term in , metaReduce(,t) returns the metarepresentation of the canonical form of
t, using the equations in , 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 of an object module , or the
second argument is not the correct metarepresentation t of a term t in , 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:
Using metaReduce we can simulate at the metalevel the primes computation example at the end of Section 4.4.7.
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:
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.
The (partial) operation metaNormalize takes as arguments the metarepresentation of a module
and the metarepresentation of a term t.
When t is a term in , metaNormalize(,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 , together with
the metarepresentation of its corresponding sort or kind. For example, from the declarations in the
predefined NAT module
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:
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 _+_.
The (partial) operation metaRewrite takes as arguments the metarepresentation of a module , the
metarepresentation of a term t, and a value b of the sort Bound, i.e., either a natural number or the
constant unbounded.
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(, t, b) is the metarepresentation of the
term obtained from t after at most b applications of the rules in 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.
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.
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(, t, b, n) results in the metarepresentation of the
term obtained from t after at most b applications of the rules in 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.
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.
The operation metaApply(, t, l, σ, n) is evaluated as follows:
;
partially
instantiated with σ, with matches that fail to satisfy the condition of their rule discarded;
;
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:
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.
Similarly, we can force the rewriting of the same term so that this time only the rule add-$ is applied.
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.
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(, 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(, 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.
Appropriate selectors extract from the result 4-tuples their four components:
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).
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.
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.
The operation metaMatch(, t, t′, Cond, n) tries to match at the top the terms t and t′ in
the module 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.
Appropriate selectors extract from the result pairs their two components:
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:
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:
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:
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.
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.
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.
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.
The sort Trace is used to represent the path as a list of triples by means of the following syntax:
We run again the same two examples as above, with the following results.
The operations metaSearchPath and metaSearch share caching, so calling one after the other on the same arguments only performs a single search.
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.
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:
The (partial) operation metaPrettyPrint takes as arguments the metarepresentations of a
module 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 . In the event of an error an empty list of quoted identifiers is
returned.
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:
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.
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.
For example,
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.
The operation sortLeq takes as arguments the metarepresentation of a module and the
metarepresentations of two types, that is, either sorts or kinds.
According to whether the types passed to sortLeq as arguments are metarepresented sorts or kinds, we can distinguish the following cases:
and let ≤
be its subsort relation. When s,s′∈ S, sortLeq returns true
if s ≤s′ and false otherwise. For example,
, then sortLeq returns false when both
kinds are different and true when they are equal. For example,
and the other one is a kind in , then sortLeq checks whether
the given sort belongs to the given kind or not. For example,
The operation sameKind takes as arguments the metarepresentation of a module and the
metarepresentations of two types, that is, either sorts or kinds.
Let S be the set of sorts in and let ≤ 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 s′ belong to
the same connected component in the subsort ordering ≤, that is, if they belong to the same
kind, and false otherwise. When the two arguments are kinds in , 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.
The operation completeName takes as arguments the metarepresentation of a module 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
, i.e., the metarepresentation of the comma-separated list of the maximal elements of the
corresponding connected component.
For example,
The operation getKind takes as arguments the metarepresentation of a module and
the metarepresentation of a type, i.e., a sort or a kind. When its second argument is the
metarepresentation of a type in , it returns the metarepresentation of the complete name of the
corresponding kind.
For example,
The operation getKinds takes as its only argument the metarepresentation of a module and
returns the metarepresentation of the set of kinds declared in , with kinds metarepresented using
their complete names.
For example,
The operation lesserSorts takes as arguments the metarepresentation of a module and the
metarepresentation of a type, i.e., a sort or a kind.
Let S be the set of sorts in . When s ∈ S, lesserSorts returns the metarepresentation of the
set of sorts strictly smaller than s in S. For example,
When the second argument of lesserSorts metarepresents a kind in , this operation returns
the metarepresentation of the set of all sorts in such kind. For example,
The operation leastSort takes as arguments the metarepresentation of a module and
the metarepresentation of a term t, and it returns the metarepresentation of the least
sort or kind of t in , 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.
For example,
The operation glbSorts takes as arguments the metarepresentation of a module and the
metarepresentations of two types, that is, either sorts or kinds.
According to whether the types passed to glbSorts as arguments are metarepresented sorts or kinds, we can distinguish the following cases:
, then glbSorts returns the
metarepresentation of the set (which can be empty) consisting of the largest sorts that
are common subsorts of the two given sorts, that is, the set of maximal lower bounds of
the two sorts; when this set is a singleton set {s}, then s will be the greatest lower bound
of the two sorts, thus the operation name glbSorts.
For example, we have the following reductions concerning sorts in the module NUMBERS.
, then glbSorts returns the empty
set when both kinds are different, and the metarepresentation of the kind (using the
corresponding complete name) when both kinds are equal. For example,
and the other one is a kind in , then glbSorts returns
the metarepresentation of the sort when the sort belongs to the kind, and the empty set
otherwise. For example,
The operations maximalSorts and minimalSorts take as arguments the metarepresentation of a
module and the metarepresentation of a kind k. If k is a kind in , 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.
For example,
The operation maximalAritySet takes as arguments the metarepresentation of a module , the
metarepresentation of an operator f in , 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′≤s. 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.
Let us consider for example the operator _+_ in the module NUMBERS, where it is overloaded by means of the following declarations:
With this information, we obtain the following reductions concerning this operator:
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.
The operation wellFormed can take as arguments the metarepresentation of a module , or the
metarepresentation of a module and a term t, or the metarepresentation of a module and a
substitution σ. In the first case, it returns true if is a well-formed module, and false otherwise. In
the second case, if t is a well-formed term in , it returns true; otherwise, it returns false. Finally,
in the third case, if σ is a well-formed substitution in , it returns true; otherwise, it returns
false.
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,
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:
Consider the module BUYING-STRATS below, which imports the META-LEVEL module.
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.
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.
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.
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.
As examples, we apply below the buying strategies (2–4) to spend in different ways the same amount of money: three dollars and a quarter.
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 [23, 25] 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.
