Footnotes

 

(1)

Supported by DARPA through Rome Laboratories Contract F30602-97-C-0312 and NASA Contract NAS2-98073, by Office of Naval Research Contract N00014-96-C-0114, and by National Science Foundation Grants CCR-9505960 and CCR-9633363.  

(2)

We say that the rewriting is done in the free-theory when rewriting with terms whose operators have no equational attributes.  

(3)

It is possible to simultaneously declare several operators having the same arity and coarity by using instead the keyword ops and giving the nonempty list of their corresponding syntactic forms after the ops keyword, as done for the nodes and edges declared in our example.  

(4)

If this list is empty, as for the edges and nodes declared in our example, the operator is called a constant.  

(5)

Such a string may have blank spaces and may consist of several identifiers in the Maude sense; see Section 2.1.1 for more details on the syntactic conventions.  

(6)

Unconditional membership axioms are introduced with the keyword mb. For example, in a module NAT of natural numbers with Peano notation we can define subsorts Zero (for the zero element) and 3*Nat for numbers that are multiples of three by declaring

fmod NAT is 

     sorts Zero 3*Nat Nat .
     subsorts Zero < 3*Nat < Nat .
     op 0 : -> Zero .
     op s_ : Nat -> Nat .
     var M : 3*Nat .
     mb s s s M : 3*Nat .
endfm

 

(7)

It is possible to give instead a single equation of the form exp = exp' as the condition. In fact, giving just a Boolean expression exp as the condition is equivalent to giving the equation exp = true. Note that there is no real loss of generality in restricting conditions to be either a single equation or a Boolean expression, since we can for example express a condition involving a conjunction of equations and membership axioms of the form

t₁=t'₁ /\ ... /\ t_n=t'_n /\ u₁:s₁ /\ ... /\ u_m:s_m

by the single equation

(t₁ == t'₁ and ... and t_n == t'_n and u₁:s₁ and ... and u_m:s_m) = true,

or just by the Boolean expression

t₁ == t'₁ and ... and t_n == t'_n and u₁:s₁ and ... and u_m:s_m.

 

(8)

By default, Maude's pretty printer will display operators in mixfix form whenever possible, but it can be turned to prefix mode by the set print mixfix off command (see Appendix A).  

(9)

More precisely, the scope of applicability of operator evaluation strategies are restricted to functional modules and to the equational part of system modules.  

(10)

Rules or conditional rules can have extra variables in their righthand sides that do not occur in their lefthand sides. For example, the identity rule in the one-sided sequent calculus for linear logic [25] as presented in [32] is of the form

rl [id] : empty => P not P .

where P is a variable of sort Atom, _,_ is the constructor for multisets of propositions and not_ is the negation operator. However, since for applying such rules we need extra information about how the extra variables should be instantiated, rules with extra variables cannot be applied when using the default rewrite command (explained later in this section) to rewrite terms with Maude's default interpreter. They must be executed at the metalevel, using the meta-apply operator in the META-LEVEL module (see Section 2.5.5). In the present version of Maude, the condition of a conditional rule must satisfy the same requirements as those for the condition of a conditional equation explained in Section 2.1, including the requirement that all variables in the condition must appear in the rule's lefthand side. In a future version we plan to support more general conditions, involving extra variables and containing not only equalities and membership axiomss, but also rewrite conditions requiring that a term can rewrite to another term.  

(11)

By always reducing a term to canonical form using the equations before applying a rule, we could potentially miss some rewrites, in the sense that a rule could have been applied before simplifying a term, but cannot be applied after simplification. The property ensuring that we do not miss such rewrites is called coherence (see [61] and Section 4.3). Coherence (or at least "weak coherence") is assumed to hold for system modules. It plays a role analogous to that played by the Church-Rosser property for functional modules.  

(12)

In the models of a rewrite theory the sorts are interpreted as categories, thus the requirement; for functional theories the requirement becomes that each such h_s is bijective. Note that the expected condition would have been to require h to be an R-isomorphism. However, due to the presence of error elements at the kind level, the isomorphism condition would be too strong, since in general, when enlarging a signature, there will be new error terms that cannot be proved equal to old ones. See [4] for a detailed discussion of, and proof techniques for, protecting extensions in membership equational logic.  

(13)

In a membership equational logic signature, terms always have a kind; they may or may not have a sort of that kind. As already mentioned, in Maude kinds are represented as error sorts, that are added by the system at the top of each connected component of sorts defined by the user.  

(14)

Of course, to ensure conservativity we also should assume that the new equations in M do not disturb the equality of terms or the rewriting relation in U. Since the equations are assumed to be Church-Rosser, conservativity of equality can be easily achieved by assuming that the tops of lefthand sides of new equations are new function symbols. Preservation of the rewriting relation can be achieved by forbidding nonvariable overlaps between lefthand sides of new equations and of rules, as done in [10].  

(15)

Of course, when the set of maximal lower bounds of two sorts is a singleton {s}, then s will be the greatest lower bound of the two sorts, thus the notation glbSorts. In subsequent discussions, when we speak of the "greatest lower bound" we will always in fact mean the more general notion of the set of maximal lower bounds.  

(16)

Of course, the constant SORTING gets also rewritten (in this case, to the meta-representation of the module SORTING); however, to ease readability we have "hidden" this rewrite in all the examples of this section.  

(17)

We talk about an interpreter for Maude functional modules in the sense of reducing the (meta-representation of) a term to its canonical form using the Church-Rosser and terminating equations just as the Maude interpreter would do it. Note, however, that, as already mentioned, the functional module--whose operators cannot have any attributes--is represented here as a system module in which the Church-Rosser equations are represented as rules labeled any.  

(18)

The syntactic order of evaluation is a syntactic notion, having to do with how parentheses are associated. It is different from the semantic notion of order of evaluation of the arguments of an operator specified by a strategy explained in Section 2.1.3.  

(19)

In the current version bubbles can only be used in modules passed to the function meta-parse as arguments. The way of using and defining bubbles will change in future releases.  

(20)

In general, to exclude identifiers I1, I2, ..., Ik, we use the syntax Exclude (I1 I2 ... Ik).

 

(21)

As pointed out in Section 2.5.5, in Core Maude the meta-representation of the module MINI-MAUDE-SYNTAX has to be explicitly given. In Full Maude we can refer to the representation of a module using its name by any of the techniques explained in Section 3.3.  

(22)

We shall see in Section 2.8 that this representation of the input as a list of quoted identifiers is given automatically by the read-eval-print loop supported by the built-in module LOOP-MODE.  

(23)

Note that since the module FULL-MAUDE is a system module in Core Maude, object-oriented declarations such as this one cannot be given directly. Instead, the equivalent declarations desugaring the desired object-oriented module have to be specified.  

(24)

Possibly containing the library of predefined modules and some other predefined modules, such as CONFIGURATION.  

(25)

We call flattened module to the version of the module in which the module and all its submodules have been collapsed to a single module.  

(26)

Renamings and, more generally, module expressions are of course supported in Full Maude.  

(27)

We do not give all the declarations in this chapter. The complete set of declarations can be found in Appendix C.  

(28)

We call rewriting modulo associativity, commutativity and identity ACU-rewriting.  

(29)

See [49] for a general method to specify real-time systems in rewriting logic.  

(30)

Notice that we have simplified the transformation of object-oriented modules into system modules that originally appeared in [38].  

(31)

The built-in module LOOP-MODE presented in Section 2.8 is not supported in Full Maude.  

(32)

To have, for example, the command red in_:_. we would need the operator declaration

  op red in_:_. : ModExp Bubble -> PreCommand .

However, given a command like red in NAT : s 0 . there would be two possible parses: red in |NAT| : |s 0| . and red |in NAT : s 0| .. Both of them are correct parses, but the meta-parse function returns only one of them. In case of ambiguity, one of the possible parses is arbitrarily chosen, preventing us from the possibility of taking the right one. This syntactic limitation as well as those discussed in Section 3.6 will be overcome in a future version.  

(33)

Theories are discussed in Section 3.5.1.  

(34)

Views are discussed in Section 3.5.3.  

(35)

In Full Maude, the importation of a module into a theory is supported only in protecting mode.  

(36)

Note that a declaration importing BOOL is added to all modules and theories. There is no way in the current version of Full Maude of setting off this inclusion. In Core Maude it can be done with the set include command.  

(37)

Notice that naming of parameterized classes follows the same conventions discussed above for parameterized sorts.  

(38)

Each view declaration has an associated set of proof obligations, namely, for each axiom in the source theory it should be the case that the axiom's translation by the view holds in the target. Since the target can be a module interpreted initially, verifying such proof obligations may in general require inductive proof techniques of the style supported for Maude's logic in [12].  

(39)

However, a functional theory may contain functional submodules in protecting mode, imposing the additional requirement that those submodules should be interpreted initially.  

(40)

Of course, if the parameterized module has several parameter theories, we should form their colimit, and consider instead the inclusion of such a colimit into the body.  

(41)

Note that POSET is a good example of a theory where part of the semantics is loose and part of it initial, because it protects the functional module BOOL, which is used in an essential way to define the partial order predicate.  

(42)

Rewriting logic is parameterized by the choice of its underlying equational logic, that can be unsorted, many-sorted, order-sorted, membership equational logic, and so on. For Maude, the underlying equational logic is of course membership equational logic. However, to ease the exposition we give here an unsorted presentation.  

(43)

To simplify the exposition the rules of the logic are given for the case of unconditional rewrite rules. However, all the ideas presented here have been extended to conditional rules in [37] with very general rules of the form

r: [t] --> [t'] if [u₁] --> [v₁] /\ ... /\ [u_k] --> [v_k].

This increases considerably the expressive power of rewrite theories.  

(44)

In the expressions appearing in the equations, when compositions of morphisms are involved, we always implicitly assume that the corresponding domains and codomains match.  

(45)

Note that we use diagrammatic order for the horizontal, alpha*beta, and vertical, gamma;delta, composition of natural transformations [31].  

(46)

Maude's rewrite engine has an extensible design, so that matching algorithms for new theories can be added and can be combined with existing ones [22]. As already mentioned, in the present version, matching modulo associativity, commutativity, (left-, right- or two-sided) identity, and idempotency, and most combinations of these attributes are supported.