Chapter 6
Module Operations

Specifications and code should be structured in modules of relatively small size to facilitate understandability of large systems, increase reusability of components, and localize the effects of system changes. In Maude, these goals are achieved by means of a module algebra that supports parameterized programming techniques in the OBJ3 style [73] as well as the definition of module hierarchies, i.e., acyclic graphs of module importations; that is, each functional or system module can import other Maude modules as submodules. Since the submodule relation is transitive, we can in this way develop module hierarchies. Mathematically, we can think of such hierarchies as partial orders of theory inclusions, that is, the theory of the importing module contains the theories of its submodules as subtheories.

As in Clear [18], OBJ [73], and other specification languages in that tradition, the abstract syntax for writing specifications in Maude can be seen as given by module expressions, where the notion of module expression is understood as an expression that defines a new module out of previously defined modules by combining and/or modifying them according to a specific set of operations. In fact, structuring is essential in all specification languages, not only to facilitate the construction of specifications from already existing ones—with more or less flexible reusability mechanisms—but also for managing the complexity of understanding and analyzing large specifications. Maude supports module operations for summation, renaming, and instantiation of parameterized modules.

Section 6.1 introduces module importations and the different modes in which such importations can take place. Section 6.2 discusses the summation and renaming module expressions. Section 6.3 introduces parameterized programming, including the use of theories and views, the parameterization of functional and system modules, and the instantiation of parameterized modules. We refer to [404849] for a deeper discussion on the semantics of the Maude module operations.

6.1 Module importation

Recall that a functional module M specifies a membership equational theory of the form (Σ,E A), with Σ its signature, A the equational attributes specified for its operators, and E its set of equations and memberships. A submodule Mof M is either a module directly imported by M, or a submodule of one of the modules directly imported by M. Then Mspecifies a membership equational subtheory (Σ,E′∪ A) ,E A). Specifically, we have three inclusions: Σ′⊆ Σ, E′⊆ E, and A′⊆ A. Furthermore, since in Maude subsort-overloaded operators must have the same equational attributes, Maude will enforce that the inclusion A′⊆ A satisfies this property.

In a similar way, a system module Q specifies a rewrite theory (Σ,E A,ϕ,R). A submodule Qof Q will likewise specify a rewrite subtheory (Σ,E′∪A,R) ,E A,ϕ,R). This means that we have inclusions Σ′⊆ Σ, E′⊆ E, A′⊆ A (again, with the same equational attributes for subsort-overloaded operators), ϕ′⊆ ϕ, and R′⊆ R, where ϕ′⊆ ϕ is an inclusion of functions and means that the freezing function ϕ extends the function ϕ. Note that Qcould be a functional module, which is then understood as the rewrite theory (Σ,E′∪A,), where ϕspecifies whatever freezing information has been given to the operators of Σin Q. A system module cannot be imported into a functional module.

In Maude, a module—any module expression giving rise to a module—can be imported as a submodule of another in three different modes: protecting, extending, or including. This is done with the syntax declarations

  protecting ModuleExpression .
  extending ModuleExpression .
  including ModuleExpression .

which can be abbreviated, respectively, to

  pr ModuleExpression .
  ex ModuleExpression .
  inc ModuleExpression .

In addition to being allowed as arguments of a protecting, extending, or including importation, module expressions can also appear as the source or target of a view (see Section 6.3.2), or as the parameter of a module, provided the top level is a theory (see Section 6.3.3).

Each of the importation modes places specific semantic constraints on the corresponding inclusion between the theory of the submodule and that of the supermodule. The user must be aware that, as explained later, the Maude system does not check that these constraints are satisfied, that is, the different modes of importation can be understood as promises by the user, which would need to be proved by him/herself. Although those importation modes have no effect operationally, they do crucially affect the interpretation given to a module by the theorem proving tools. If a user is doubtful about the appropriate importation mode the default should be to use the including mode, which places weaker requirements on the importation.

Importation statements take a module expression as argument, which may be a module name, the summation of module expressions, the renaming of a module expression, or the instantiation of a parameterized module expression. Modules are constructed for each subexpression of a module expression, and so each submodule signature must be legal. Modules and module expressions are cached both to save time and so that the same module corresponding to a module expression will not be imported twice via a diamond of imports. Mutually or self recursive imports occurring through module expressions are detected and disallowed. Cached modules generated by module expressions that no longer have any users (if the module(s) containing the module expression have been replaced) are deleted. When a module M used in a module expression is modified, any modules generated for module expressions that depend on M are deleted and any modules that depend on M are reevaluated if you attempt to use them. Here the notion of “depends on” is transitive through arbitrary nesting of importation and module expressions.

In addition to being imported by the explicit importation statements we have just introduced, modules can be imported in an implicit way (also in the three possible modes) by means of commands set protect/extend/include module on/off; see more details in Section 18.13 and the detailed example in Section 7.1.

6.1.1 Protecting

Importing a module Minto M in protecting mode intuitively means that no junk and no confusion are added to Mwhen we include it in M. For example, we may import the module NAT of natural numbers into a module FOO. “Junk” would be added to NAT if in FOO we have new ground terms in canonical form in any of the sorts in NAT, namely Nat and NzNat. For example, FOO may have declared a constant infinity of sort NzNat to which no equations apply. “Confusion” would be added if different natural numbers are now identified. For example, if FOO contains the equation s s 0 = 0, then all even numbers will be identified with 0 and all odd numbers with s 0.

Let us explain the semantics of the protecting relation in more detail for functional modules M and M, where Mhas been imported as a submodule in protecting mode, either by an explicit protecting importation in M, or transitively through one of M’s submodules. Let (Σ,E′∪ A) ,E A) be the theory inclusion defined by the module inclusion M′⊆ M. Notice that the existence of the inclusions Σ′⊆ Σ, E′⊆ E, and A′⊆ A means that for each sort sin Σ there is a well-defined function

qs′ : TΣ′∕E ′∪A′,s′ -→ TΣ∕E∪A,s′

mapping the equivalence class [t]E′∪A of a ground term t to the equivalence class [t]EA. By definition, the submodule inclusion M′⊆ M is protecting if and only if for each sort sin Σthe above function is bijective. This captures mathematically the “no junk” (surjectivity) and “no confusion” (injectivity) ideas. Under our ground Church-Rosser and termination assumptions for Mand M this also means that the canonical form of any ground Σ-term t in Mthat has a sort in Σmust be the same as its canonical form in M. The requirement that t must have a sort is crucial. We do not require that for ka kind the map

qk′ : TΣ′∕E ′∪A′,k′ -→ TΣ∕E∪A,k′

is bijective. The reason is that the notion of defined function—that is, an operator that disappears and leaves just a term with constructors—is only meaningful when the result has a sort. The same operator may not disappear for error terms at the kind level. That is, in the module M extending Mthere may easily be new error terms of kind kcreated by new operators in M. For example, if we import the module NAT into the module RAT of rational numbers, the sorts Nat and Rat belong to the same kind, but there are now new error terms in the kind, such as 3 + 7/0. Therefore, we should not care about “error junk” being added by a supermodule at the kind level, provided that the sorts themselves are protected.

For system modules the protecting requirement is interpreted exactly as before as far as their underlying equational theories are concerned. That is, if Q protects Qand the associated theory inclusion is (Σ,E′∪ A,R) ,E A,ϕ,R), then the equational theory inclusion (Σ,E′∪ A) ,E A) must be protecting. We furthermore require that for any two ground Σ-terms t and twe can reach tfrom t by a sequence of rewrites in the module Mif and only if we can do so in the module M; that is, for ground terms in Mwe require that the reachability relation is not altered by the supermodule.

Of course, the protecting assertion cannot be checked by Maude at runtime: it requires inductive theorem proving. Using the proof techniques in [15] together with an inductive theorem prover for membership equational logic and a Church-Rosser checker such as those described in [505227] (which are available in the Maude formal tool environment together with other useful tools for termination and sufficient completeness), this can be done for functional modules. Using the fact that initial models of rewrite theories are also models of equational theories [16], similar proof techniques could be developed to prove the protecting relation between rewrite theories.

6.1.2 Extending

A weaker, yet substantial, requirement about a module importation is expressed by the keyword extending. Intuitively, the idea is to allow “junk,” but to rule out confusion. Extending importations may appear naturally in situations in which the data of some sort is extended with new data elements, yet not identifying previously defined data, like adding a new constant infinity to the natural numbers in a module importing NAT. As another example, when defining the semantics of a programming language in Maude, we can have from the beginning a sort Program, and define incrementally the syntax of programs in several modules, say, EXPRESSION, STATEMENT, PROCEDURE, and so on. This will typically give rise to a family of extending module importations as more syntax is added.

For functional modules Mand M, where Mhas been imported as a submodule in extending mode, either by an explicit extending importation in M, or transitively through one of M’s submodules, if (Σ,E′∪ A) ,E A) is the theory inclusion defined by the module inclusion M′⊆ M, the extending requirement means that for each sort sin Σthe function

qs′ : TΣ′∕E ′∪A′,s′ -→ TΣ∕E∪A,s′

is injective. For system modules the extending requirement is interpreted exactly as before as far as their underlying equational theories are concerned. That is, if Q extends Qand the associated theory inclusion is (Σ,E′∪ A,R) ,E A,ϕ,R), then the equational theory inclusion (Σ,E′∪ A) ,E A) must be extending. We furthermore require that for any two ground Σ-terms t and twe can reach tfrom t by a sequence of rewrites in the module Mif and only if we can do so in the module M; that is, for ground terms in Mthe reachability relation is not altered by the supermodule.

Under the Church-Rosser and termination assumptions, the extending ,E′∪A) ,E A) requirement is a form of conservative extension requirement, in the sense that it implies that for any Σground terms t and tthat have a sort in (Σ,E′∪ A), E′∪ Aproves t = tif and only if E A proves t = t. In addition, for system modules it further implies that for any two ground Σ-terms t and tthe reachability relation is not altered by the extension. In summary, equality and reachability are conservatively preserved for ground terms.

Note that the extending relation does not destroy protecting importations further down the hierarchy. That is, if M imports Min extending mode, but Mimports M′′ in protecting mode, then M still imports M′′ in protecting mode, not in extending mode. If we do not want M to protect M′′ (because this is indeed violated), then we have to say so by explicitly giving an extending importation declaration for M′′ in M.

6.1.3 Including

The most general form of module importation is provided by the including keyword. No requirements are made in an including importation about maps of the form qs: there can now be junk (lack of surjectivity) and/or confusion (lack of injectivity). Likewise, for system modules it is not anymore required that the reachability relation between ground terms in the submodule is preserved. The including keyword does however impose some requirements. First of all, there is the requirement that the equational attributes of subsort-overloaded operators must be the same. Furthermore, the including relation does not destroy protecting or extending importations further down the hierarchy. That is, if M imports Min including mode, but Mimports M′′ in protecting (resp. extending) mode, then M still imports M′′ in protecting (resp. extending) mode, not in including mode. If we do not want M to protect or extend M′′ (because this is indeed violated), then we have to say so by explicitly giving an including importation declaration for M′′ in M.

Given that, as already mentioned, there is no difference at runtime between the different modes of importation because the Maude system does not check the corresponding requirements, from a pragmatic point of view, when a user is doubtful about the appropriate importation mode, the best idea is to use the including mode so that at least no false assertion is made.

6.1.4 Default conventions in module importations

We have already explained our default convention when a submodule M0 is imported indirectly and transitively into M through the direct importation by M of a module M1 that itself imports M0. Then, whatever was the mode (protecting, extending, or including) in which M0 was imported by M1 is also, by default, the mode in which M0 is imported by M, unless M contains an explicit declaration importing M0 in a different mode. We now explain what our default convention is in the case of diamond importations.

We talk of a diamond importation of M0 by M, when M0 is imported indirectly by M through the direct importation of two or more different modules, say M1,M2,,Mk. The problem now is that M0 can be imported by each of the modules M1,M2,,Mk in different modes. For example, M1 could import it in protecting mode, M2 in extending mode, M3 in including mode, and so on. What should now be the default convention for the mode in which M imports M0? We adopt a convention that is consistent with a logical understanding of such importation declarations. Indeed, such declarations impose semantic constraints of decreasing strength; that is, we have:

protecting M0  ⇒  extending M0  ⇒  including M0.

The default convention consistent with this logical reading is that the strongest mode wins, i.e., protecting prevails over extending, which itself prevails over including. This is because we view the set of all such importing mode declarations as a conjunction, and exploit the logical equivalence between A B and (A B) A.

Note that this “strongest wins” default mode may not always be the correct or intended mode in which M should import M0. Sometimes it may not be, and then the user should overrule the default convention by declaring explicitly a different mode in which M imports M0. A pragmatic reason why this need for overruling the default mode may arise is that, although a weaker mode of importation (say extending) does not logically preclude such an importation also satisfying a stronger one (say protecting), in practice, when we declare an importation in a weaker mode it can often be because we know or suspect that it fails to satisfy a stronger mode. For example, when we say “extending” we may often mean “extending and not protecting.”

6.1.5 Some module hierarchy examples

Prime numbers sieve

Section 4.4.7 included a functional module specifying the sieve of Eratosthenes to calculate prime numbers.

  fmod SIEVE is  
    protecting NAT .  
    sort NatList .  
    subsort Nat < NatList .  

The predefined module of natural numbers (see Section 7.2) is imported in protecting mode. This is justified because the elements of sort Nat are used to generate the lists of natural numbers by means of a subsort declaration and also as arguments of other operators. However, no new operator of result sort Nat is added in the SIEVE module, and all the equations in this module identify elements of sort NatList without identifying different natural numbers.

Vending machine

The vending machine example in Section 5.1 was presented in a modular way, by separating the underlying signature defining the states of the machine from the rules defining the corresponding transitions.

    var M : Marking .  
    rl [add-q] : M => M q .  

It is important to notice that in this example the importation mode cannot be either protecting or extending, because those modes require preservation of the reachability relation, which clearly is not the case when adding (non-identity) rewrite rules to a functional module (where the reachability relation is the identity).

Bank accounts and object configurations

Later, in Section 8.1, devoted to the definition of configurations of objects and messages for object-based programming, we will present several modules where additional data are introduced in order to run some tests. For example, the following module introduces three new constants to be used as object identifiers, and a new constant to be used as a test configuration. This configuration constant is identified with a term of sort Configuration in the imported module BANK-ACCOUNT by means of an equation whose righthand side is omitted below. However, constants A-001, A-002, and A-003 are new data elements, i.e., junk, of sort Oid. The sort Oid was declared in the module CONFIGURATION, but since it was imported in including mode in BANK-ACCOUNT, it is not necessary to import it in a different mode. Therefore, the appropriate importation mode is extending.

    ex BANK-ACCOUNT .  
    ops A-001 A-002 A-003 : -> Oid .  
    op bankConf : -> Configuration .  
    eq bankConf = ... .  

The following example, from Section 8.3, is more interesting, in that it introduces new sorts MsgBody and Request, not just new constants for a sort in the imported module. Still, the appropriate importation mode is extending because there are no new rewrite rules and no equations, and thus no confusion between elements in imported sorts is introduced.

    sort MsgBody .  
    op msg : Oid Oid MsgBody -> Msg [ctor message] .  
    sort Request .  
    op w4 : Oid Oid MsgBody -> Request [ctor] .  

There are several other modules in Chapter 8 illustrating the use of the extending mode in importing modules, like BANK-MANAGER-TEST, TICKER-TEST, TICKER-FACTORY-TEST, and AGENT-TEST; see Figures 8.1, 8.2, and 8.3.

Hierarchy of predefined modules

A more complex acyclic importation graph corresponds to the hierarchy of predefined modules for basic data types, described later in Chapter 7 and shown in Figure 7.1, where all the importations are in protecting mode.

6.2 Module summation and renaming

6.2.1 The summation module expression

The summation module operation creates a new module that includes all the information in its summands. The syntax for a summation of module expressions is

  ModuleExpression + ModuleExpression
with + associative and commutative.

Summation expressions are flattened before being evaluated, so that A + (B + C) and (C + A) + B both create a single new module A + B + C, The evaluation of a summation module expression results in the creation of a new module, with such a module expression as its name, which imports the module expressions being combined. The new module will be generated having one type or another, depending on the types of the arguments of the summation module expression. A summation is a functional module if all the summands are functional modules and a system module otherwise.

Although the use of the summation module expression is more interesting in combination with other module expressions, let us consider as an example the following module, in which the union of the predefined FLOAT and STRING modules (see Chapter 7) are imported together in protecting mode to illustrate its use.

  fmod FLOAT-STRING is  
    protecting FLOAT + STRING .  

Notice that a declaration

  protecting A + B .

is not equivalent to a sequence of declarations

  protecting A .  
  protecting B .

because in general the modules A and B may share sorts and operators. The same happens with extending declarations, for the same reason. However, a declaration of the form

  including A + B .

is indeed equivalent to a sequence of declarations

  including A .  
  including B .

6.2.2 Module renaming

The syntax of a renaming module expression is

  ModuleExpression * ( Renaming )

where Renaming is a comma-separated sequence of renaming items of the forms:

  sort identifier to identifier
  op identifier to identifier
  op identifier to identifier [ attribute-set ]
  op identifier : type-list -> type to identifier
  op identifier : type-list -> type to identifier
       [ attribute-set ]
  label identifier to identifier

Renaming (_*(_)) binds tighter than summation (_+_), and it groups to the left. Note that, in addition to the typical renamings of sorts and operators, renaming of labels is also supported (which may be useful for metalevel applications). Note also how the renaming of operators allows changing the attributes of the operator being renamed. The only attributes currently allowed in operator maps are prec, gather, and format. The idea is that when you rename an operator, the old syntactic properties may no longer be legal and are reset to defaults, unless you explicitly set them with these attributes; for example, when a change in the syntax of the operator could cause a parsing different from the intended one. Let us see an example in which modifying the grammatical attributes of an operator is useful. Consider the following module defining lists of natural numbers with a max operator returning the greatest of the elements in a list of natural numbers.

  fmod NAT-LIST-MAX is  
    pr NAT .  
    sort NeNatList .  
    subsort Nat < NeNatList .  
    op __ : NeNatList NeNatList -> NeNatList [ctor assoc] .  
    op max : NeNatList -> Nat .  
    var N : Nat .  
    var NL : NeNatList .  
    eq max(N) = N .  
    eq max(N NL) = if N > max(NL) then N else max(NL) fi .  

We may obtain the maximum of a list of natural numbers as follows.

  Maude> red max(4 2 5 3) .  
  result NzNat: 5

Suppose now that we want to change the syntax of the function max in the NAT-LIST-MAX module above to maximum_.

    pr NAT-LIST-MAX * (op max : NeNatList -> Nat to maximum_) .  

We can do the following reduction:

  Maude> red maximum 2 3 4 1 .  
  result NeNatList: 2 3 4 1

This result may seem strange, but it makes perfect sense. What has happened is that it has been parsed as (maximum 2) 3 4 1, the only possible parse given the default precedence values and gathering patterns assigned. Since by default maximum_ has precedence 15 and gathering E, it cannot take the list 2 3 4 1 as argument because __ has precedence 41. However, since __ has gathering e E, maximum 2 is a valid argument for it (see Section 3.9 for a detailed discussion on the use of precedence values and gathering patterns and their default values). We can of course obtain the intended result by placing parentheses around the set of numbers,

  Maude> red maximum (2 3 4 1) .  
  result NzNat: 4

but it is more convenient to change the precedence values of the operators. We can, for example, raise the precedence of maximum_.

    pr NAT-LIST-MAX  
         * (op max : NeNatList -> Nat to maximum_ [prec 41]) .  

having then the following reduction.

  Maude> red maximum 2 3 4 1 .  
  result NzNat: 4

Notice that if maximum_ has precedence 41, then (maximum 2) 3 4 1 is no longer a valid parse.

A renaming can be considered as a function that, given a module M and a list of mappings S, returns a copy of the module, with such a module expression as its name, in which the names of sorts, operators, etc. are changed as indicated by the mappings. However, renaming a module that has imports is a subtle issue. Given a structured specification, the renaming not only causes the creation of a copy of the top module in the structure, but renames also the part of the submodule structure that is affected by the renaming. For any other submodule Min the structure which is affected by the mappings, a renamed copy of it is generated with name M * (S), where Sis the subset of mappings in S that affect M.

A module expression A * (R) evaluates to A if A has no content that is affected by the renaming R. Otherwise A * (R) evaluates to a new module A * (R) where Ris obtained by deleting those renaming items that do not affect A, and canonizing the types in operator renamings with respect to A (see below). If A imports modules B and C, A * (R) will import modules obtained by evaluating B * (R) and C * (R).

There are some subtle cases. Consider for example the following three modules:

  fmod RENAMING-EX-A is  
    sort Foo .  
    op a : -> Foo .  
    op f : Foo -> Foo .  

  fmod RENAMING-EX-B is  
    including RENAMING-EX-A .  
    sort Bar .  
    subsort Foo < Bar .  
    op f : Bar -> Bar .  

  fmod RENAMING-EX-C is  
    inc RENAMING-EX-B * (op f : Bar -> Bar to g) .  

Here, the operator f in the module RENAMING-EX-A looks as though it is not affected by the renaming in the module RENAMING-EX-C, but because of the subsort declaration Foo < Bar in RENAMING-EX-B, it should be renamed for consistency. This is internally handled by the Maude system by canonizing the type Bar occurring in the renaming

  op f : Bar -> Bar to g

to the kind expression [Foo,Bar], which includes all of the sorts in the kind [Bar] occurring in RENAMING-EX-B. Thus, the module expression

  RENAMING-EX-B * (op f : Bar -> Bar to g)

evaluates to a new module

  RENAMING-EX-B * (op f : [Foo,Bar] -> [Foo,Bar] to g)

which includes the module expression

  RENAMING-EX-A * (op f : [Foo,Bar] -> [Foo,Bar] to g)

which evaluates to a new module

  RENAMING-EX-A * (op f : [Foo] -> [Foo] to g)

in which f has been renamed.

In general, * does not distribute over +. Consider this other example:

  fmod RENAMING-EX-D is  
    sorts Foo Bar .  

  fmod RENAMING-EX-E is  
    inc RENAMING-EX-D .  
    op f : Foo -> Foo .  

  fmod RENAMING-EX-F is  
    inc RENAMING-EX-D .  
    subsort Foo < Bar .  
    op f : Bar -> Bar .  

It is not the case that the module expressions

  (RENAMING-EX-E + RENAMING-EX-F) * (op f : Bar -> Bar to g)


  (RENAMING-EX-E * (op f : Bar -> Bar to g))  
    + (RENAMING-EX-F * (op f : Bar -> Bar to g))

evaluate to the same module, because in the latter the operator f occurring in RENAMING-EX-E will not be renamed, since f : Bar -> Bar does not occur in RENAMING-EX-E.

Operators with the poly attribute are only affected by operator renamings that do not specify types. Renaming a module does not change its module type, that is, renamed functional modules (resp. system modules) remain functional (resp. system).

6.3 Parameterized programming

Theories, parameterized modules, and views are the basic building blocks of parameterized programming [1873]. As in OBJ, a theory defines the interface of a parameterized module, that is, the structure and properties required of an actual parameter.

A parameterized module is a module with one or more parameters, each of which is expressed by means of one theory, that is, modules can be parameterized by one or more theories. If we want, e.g., to define a list or a set of elements, we may define a module LIST or SET parameterized by a theory expressing the requirements on the type of the elements to store in such data structures. Thus, theories are used to declare the interface requirements for parameterized modules. In the case of lists and sets we do not need any requirement on the data elements, and therefore we may use the trivial theory TRIV, with just a sort Elt, as parameter of such modules; but in other cases, say search trees or sorted lists, we may require, e.g., a particular operator, an order relation, or an equivalence relation, in which cases we shall need to use the appropriate theories describing the specific requirements.

The instantiation of the formal parameters of a parameterized module with actual parameter modules or theories requires a view mapping entities from the formal interface theory to the corresponding entities in the actual parameter module.

6.3.1 Theories

Theories are used to declare module interfaces, namely the syntactic and semantic properties to be satisfied by the actual parameter modules used in an instantiation. As for modules, Maude supports two different types of theories: functional theories and system theories, with the same structure of their module counterparts, but with a different semantics. Functional theories are declared with the keywords fth ... endfth, and system theories with the keywords th ... endth. Both of them can have sorts, subsort relationships, operators, variables, membership axioms, and equations, and can import other theories or modules. System theories can also have rules. Although there is no restriction on the operator attributes that can be used in a theory, there are some subtle restrictions and issues regarding the mapping of such operators (see Section 6.3.2).

Like functional modules, functional theories are membership equational logic theories, but they do not need to be Church-Rosser and terminating, and therefore some or all of their statements may be declared with the nonexec attribute. Theories have a loose semantics, in the sense that any algebra satisfying the equations and membership axioms in the theory is an acceptable model. However, functional theories can be executed in exactly the same way as functional modules; that is, the equations and membership axioms not having the nonexec attribute should be Church-Rosser and terminating, and can be executed by equational simplification, whereas the statements declared as nonexec can be arbitrary and can only be executed in a controlled way at the metalevel. System theories have a similar loose interpretation, but are treated just as system modules for executability purposes. Theories are then allowed to contain rules and equations which, if declared with the nonexec attribute, can be arbitrary, that is, can have variables in their righthand sides or conditions that may not appear in their corresponding lefthand sides and do not obey the admissibility conditions in Sections 4.6 and 5.3. Similarly, conditional membership axioms may have variables in their conditions that do not appear in their head membership assertions. Also, the lefthand side may be a single variable.

Let us begin by introducing the functional theory TRIV, which requires just a sort.

  fth TRIV is  
    sort Elt .  

The theory TRIV is used very often, for instance in the definition of data structures, such as lists, sets, trees, etc., of elements of some type with no specific requirement; in these cases, it is common to define a module, say LIST, SET, TREE, etc., parameterized by the TRIV theory (see Section 6.3.3). The theory TRIV is predefined in Maude, together with several useful views from TRIV to other predefined modules and theories (see Section 7.11.1).

But we can define more interesting theories. For example, the theory of monoids, with an associative binary operator with identity element 1, can be specified as follows:

  fth MONOID is  
    including TRIV .  
    op 1 : -> Elt .  
    op __ : Elt Elt -> Elt [assoc id: 1] .  

Notice the importation of the theory TRIV into the MONOID theory. As for modules, it is possible to structure our theories by importing other theories and modules (and in general module expressions involving theories and modules) into theories. However, a theory cannot be imported into a module: theories can only be used as parameters of modules. Also, theories do not have automatic importation as modules do (e.g., BOOL, as described in Section 7.1).

Modules and theories can be combined in module expressions (they can be summed, for example), and modules can be imported into theories. Basically, we have a lattice


where summation corresponds to join, and where a module or theory may only import a submodule or subtheory of lesser or equal type.

Although the importation of a module into a theory can be done in any mode, a theory can only be imported in including mode into another theory. The including importation of a theory into another theory keeps its loose semantics. However, the importation of a theory into another one in protecting or extending mode would imply additional semantic requirements; such modes of importation are ruled out.1 On the other hand, although a module keeps its initial interpretation when imported into a theory in protecting or extending modes, it looses it if imported in including mode.

Let us see a few examples illustrating all this.

The theory of commutative monoids can be defined just as the theory of monoids; the binary operator _+_ is now declared associative, commutative, and has 0 as its identity element.

  fth +MONOID is  
    including TRIV .  
    op 0 : -> Elt .  
    op _+_ : Elt Elt -> Elt [assoc comm id: 0] .  

The theory of semirings can be expressed as follows.

  fth SEMIRING is  
    including MONOID .  
    including +MONOID .  
    vars X Y Z : Elt .  
    eq X (Y + Z) = (X Y) + (X Z) [nonexec] .  
    eq (X + Y) Z = (X Z) + (Y Z) [nonexec] .  

Note the use of the nonexec attribute, and note also that given the semantics of theory inclusions, there is no difference between having a structured theory or one flat theory including all the declarations.2 For example, the theory of commutative rings can be defined directly as follows:

  fth RING is  
    sort Ring .  
    ops z e : -> Ring .  
    op _+_ : Ring Ring -> Ring [assoc comm id: z] .  
    op _*_ : Ring Ring -> Ring [assoc comm id: e] .  
    op -_ : Ring -> Ring .  
    vars A B C : Ring .  
    eq A + (- A) = z [nonexec] .  
    eq A * (B + C) = (A * B) + (A * C) [nonexec] .  

but could also be defined as a structured theory including the theories of commutative groups and commutative monoids (renamed if necessary), to which the distributivity axiom is added.

As mentioned above, the including importation of a theory into another theory keeps its loose semantics. However, if the imported theory contains a module, which therefore must be interpreted with an initial semantics (see Section 5.3), then that initial semantics is maintained by the importation. For example, in the definition of the TAOSET theory below, the declaration protecting BOOL ensures that the initial semantics of the functional module for the Booleans is preserved, which is in fact a crucial requirement.

Let us consider now a hierarchy of theories for partially and totally ordered sets. The most basic theory specifies a transitive and antisymmetric order _<_ on a set:

  fth TAOSET is  
    protecting BOOL .  
    sort Elt .  
    op _<_ : Elt Elt -> Bool .  
    vars X Y Z : Elt .  
    ceq X < Z = true if X < Y /\ Y < Z [nonexec label transitive] .  
    ceq X = Y if X < Y /\ Y < X [nonexec label antisymmetric] .  

By adding irreflexivity to TAOSET we get a theory specifying a strict partial order:

  fth SPOSET is  
    including TAOSET .  
    var X : Elt .  
    eq X < X = false [nonexec label irreflexive] .  

Notice that in this case antisymmetry is implied by irreflexivity and transitivity. Of course, there are different ways of presenting a theory, and in particular one can always write the corresponding flat theory with only the axioms for irreflexivity and transitivity. In the presentation above, the initial semantics of BOOL when it is imported in protecting mode in TAOSET is preserved when the latter is included in SPOSET. The same will hold in further importations in this hierarchy of order theories.

On the other hand, by adding reflexivity to TAOSET we get a theory specifying a non-strict partial order. Notice the renaming in the importation, so that the name of the order _<=_ reflects its reflexivity.

  fth NSPOSET is  
    including TAOSET * (op _<_ to _<=_) .  
    var X : Elt .  
    eq X <= X = true [nonexec label reflexive] .  

Having both _<_ and _<=_ available together is useful in some applications. There are standard ways of associating a strict partial order with a non-strict partial order and the other way around:

These equivalences can be expressed as Maude theories as follows, where we use the same name for both theories because they are equivalent, that is, we have two different presentations of the same theory and in what follows we will not care about which version of POSET is used.

  fth POSET is  
    including SPOSET .  
    op _<=_ : Elt Elt -> Bool .  
    vars X Y : Elt .  
    eq X <= X = true [nonexec] .  
    ceq X <= Y = true if X < Y [nonexec] .  
    ceq X = Y if X <= Y /\ X < Y = false [nonexec] .  

  fth POSET is  
    including NSPOSET .  
    op _<_ : Elt Elt -> Bool .  
    vars X Y : Elt .  
    eq X < X = false [nonexec] .  
    ceq X <= Y = true if X < Y [nonexec] .  
    ceq X = Y if X <= Y /\ X < Y = false [nonexec] .  

Notice that the axioms are almost the same in both presentations of POSET, but, while the first presentation defines the reflexive order _<=_ in terms of the irreflexive one _<_, the second presentation defines the irreflexive order _<_ in terms of the reflexive one _<=_.

To each of the previous theories we can add an axiom requiring the order to be total (or linear), that is, two different elements have to be related one way or the other. In this way, we have the following theories for a strict total order, a non-strict total order, and a total order with both operations.

  fth STOSET is  
    including SPOSET .  
    vars X Y : Elt .  
    ceq X = Y if X < Y = false /\ Y < X = false [nonexec label total] .  

  fth NSTOSET is  
    including NSPOSET .  
    vars X Y : Elt .  
    ceq X <= Y = true if Y <= X = false [nonexec label total] .  

  fth TOSET is  
    including POSET .  
    vars X Y : Elt .  
    ceq X <= Y = true if Y <= X = false [nonexec label total] .  

As already mentioned above, the requirement ensuring the initial semantics of BOOL when it is protected in TAOSET is then preserved by the remaining theories when TAOSET is included in them via a chain of including importations. In fact, we are dealing with structures in which part of them, not only the top theory, has a loose semantics, while other parts contain modules with an initial semantics.

This hierarchy of order theories is displayed in Figure 6.1, where we represent by boxes the modules (with initiality constraints), by ovals the theories (with loose semantics), by triple arrows the protecting importations, and by single arrows the including importations.


Figure 6.1: Hierarchy of order theories

Finally, as an example of a system theory, let us consider the theory CHOICE of bags of elements with a choice operator defined on the bags by a rewrite rule that nondeterministically picks up one of the elements in the bag. We can specify this theory as follows, where we have a sort Bag declared as a supersort of the sort Elt.

  th CHOICE is  
    sorts Bag Elt .  
    subsort Elt < Bag .  
    op empty : -> Bag .  
    op __ : Bag Bag -> Bag [assoc comm id: empty] .  
    op choice : Bag -> Elt .  
    var E : Elt .  
    var B : Bag .  
    rl [choice] : choice(E B) => E .  


We use views to specify how a particular target module or theory is claimed to satisfy a source theory. In general, there may be several ways in which such requirements might be satisfied, if at all, by the target module or theory; that is, there can be many different views, each specifying a particular interpretation of the source theory in the target. 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 true 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 [27], and for which tools in the Maude formal environment can be used. Such proof obligations are not discharged or checked by the system.

In the definition of a view we have to indicate its name (which has to be a single identifier, as defined in Section 3.1), the source theory, the target module or theory, and the mapping of each sort and operator in the source theory. The name space of views is separate from the name space of modules and theories, which means that, e.g., a view and a module could have the same name. In fact, we shall see below how we recommend naming inclusion views as the target theory. The source and target of a view can be any module expression, with the source module expression evaluating to a theory and the target module expression evaluating to a module or a theory.

The syntax for views is as follows:

  view ViewName from Source to Target is

The mapping of a sort in the source theory to a sort in the target module or theory is expressed with syntax

  sort identifier to identifier .

For each sort S in the source theory, there must exist a sort Sin the target module or theory which is its mapping under the view; unmentioned sorts get the identity mapping. Furthermore, if sorts S and T in the source theory are in the same kind, then their mappings Sand Tunder the view must be in the same kind in the target module or theory. Finally, if S is a subsort of T, then it must be true that Sis a subsort of T.

The mapping of operators is expressed with syntax

  op identifier to identifier .
  op identifier : type-list -> type to identifier .
  op op-expr to term term .

In the first case, where only an operator identifier is given, the map affects all operators with the same name. Existence of appropriate operators in the target is checked for. In the second case, when explicit arity and coarity are given, the operator map affects not only the operators with such arity and coarity, but also the entire family of subsort-overloaded operators (see Section 3.6) associated with the given operator. The third case is similar to the second one, but instead of mapping the operator to another operator, it is mapped to a given term with variables; op-expr is a term consisting of a single operator applied to variables—declared either on-the-fly or with variable declarations in the same view—and the target term is any term with variables, those in the source op-expr in the corresponding sorts resulting from the mapping. See below for more details and examples.

Maps must preserve the arities and the types of operators, and sort maps and operator maps must be compatible. For each operator f : S1Sn -> T in the source theory there must exist an operator f : S1Sn -> T in the target module or theory, where Si is the mapping of sort Si under such a view.

Unmentioned operators also get the identity mapping. Thus, “obvious” parts of a mapping do not need to be explicitly given, namely, any identical mapping of a sort or operator such that its arity and coarity are mapped to those of an operator with the same name in the target can be omitted.3

As a first example, the following view StringAsToset defines a view from the theory TOSET, presented in Section 6.3.1, to the predefined functional module STRING, described in Section 7.8.

  view StringAsToset from TOSET to STRING is  
    sort Elt to String .  

Notice that the identity maps op _<_ to _<_ and op _<=_ to _<=_ have been omitted.

The maps sending operators to derived operators, that is, terms with variables, allow us to map an operator, not only to another operator, but also to an expression. The view RingToRat below is a view from the theory RING, presented in Section 6.3.1, to the predefined functional module RAT, described in Section 7.6.

  view RingToRat from RING to RAT is  
    sort Ring to Rat .  
    op e to term 1 .  
    op z to 0 .  

Notice that we have followed the convention of omitting the “obvious” parts of the map concerning the operators _+_ and _*_. Furthermore, we have used an operator map sending the operator e to the term 1, due to the fact that in RAT 1 is not a constant, but the term s_^1(0) (see Sections 4.4.2, 7.2, and 7.6 for details). Note that the map op e to term 1 cannot be expressed with the other forms of operator maps, because 1 is not an operator, but just syntactic sugar for the term s_^1(0).

As another example, consider the case in which we want to define a view from the theory NSPOSET in which we have a sort Elt and a non-strict “less or equal” operator _<=_ : Elt Elt -> Bool, to a module defining the integers with no such operator but instead with a strict operator “less than” _<_ : Int Int -> Bool. Then, we can define a view with maps

  sort Elt to Int .  
  op X:Elt <= Y:Elt to term X:Int < Y:Int or X:Int == Y:Int .

where we have also used the predefined equality operator _==_. The lefthand side of the operator mapping, X:Elt <= Y:Elt in this case, which consists of an operator with only variable arguments, must parse to a unique term in the source theory. Each of the variables used in the maps must have a unique base name (e.g., using both X:Foo and X:Bar in the same argument list is disallowed).

Also, the righthand side, X:Int < Y:Int or X:Int == Y:Int in this case, must parse to a unique term in the target module or theory. The only variables that may occur in the target term are those appearing in the source term; however, they may occur multiple times or not at all. If the source term parses to a sort S or kind [S], then the target term must parse to sort T or kind [T] such that T and the mapping of S under the view Sbelong to the same kind.

Views may also contain variable declarations. The syntax is identical to that in modules and theories. However, its semantics is subtly different. Instead of declaring a single variable, a declaration

  var X : S    .

now declares two aliases with the same name; in the lefthand side of an operator mapping, X is an alias for X:S   while in the righthand side of an operator mapping, X is an alias for X:S′  , with S the mapping of S under the view.

For example, we can define a view from the theory SPOSET with a strict order operation _<_ to the predefined functional module INT of integers (see Section 7.4) in such a way that the _<_ order relation of a poset is mapped to an expression using the “less than or equal” operator _<=_ on sort Int and the predefined inequality operator _=/=_ in BOOL (see Sections 7.4 and 7.1) as follows:

  view SPosetToInt from SPOSET to INT is  
    sort Elt to Int .  
    vars X Y : Elt .  
    op X < Y to term X <= Y and X =/= Y .  

Alternatively, we can specify this view without a variable declaration as

  view SPosetToInt from SPOSET to INT is  
    sort Elt to Int .  
    op X:Elt < Y:Elt to term X:Int <= Y:Int and X:Int =/= Y:Int .  

Note that this view imposes several proof obligations to be checked by the user. In particular, the translations by the view of the axioms in SPOSET should hold in the target. Given variables X, Y, and Z of sort Int, the following axioms should be true in INT:

  eq X <= X and X =/= X = false .  
  ceq X <= Z and X =/= Z = true  
    if X <= Y and X =/= Y /\ Y <= Z and Y =/= Z .  
  ceq X = Y if X <= Y and X =/= Y /\ Y <= X and Y =/= X .

Of course, since the predefined INT module indeed includes both operators _<_ and _<=_, it is not necessary to use the feature described in the previous example. We can instead have simpler view declarations such as the following:

  view IntAsStoset from STOSET to INT is  
    sort Elt to Int .  

  view IntAsToset from TOSET to INT is  
    sort Elt to Int .  

where the identity maps op _<_ to _<_ and op _<=_ to _<=_ have been omitted.

We recommend following the convention of naming views from TRIV by the name of the sort to which Elt is mapped, when the name of this sort is not structured.4 Thus, a view from the theory TRIV to the module INT that sends the sort Elt to Int should be named Int (as we shall see in Section 7.11.1, the view Int is predefined in Maude).

  view Int from TRIV to INT is  
    sort Elt to Int .  

This convention can add understandability to the specifications. As we will see in Section 6.3.4, given a module LIST of lists parameterized by TRIV with a sort List{X}, once it is instantiated, e.g., with the view Int above, the sort List{X} becomes List{Int}, defining lists of integers. Using names of views as labels in interfaces of parameterized modules (see Section 6.3.4 below) should be avoided, since this can sometimes generate ambiguities.

We can also have views between theories, which is particularly useful to compose instantiations of views to link the formal parameter of some parameterized module to some actual parameter via some intermediate formal parameter of another parameterized module. We will discuss the uses of these views and give some examples in the coming sections. An example of a view whose target is a theory is the following:

  view PosetToToset from POSET to TOSET is  
    sort Elt to Elt .  

As said above, identity maps can be omitted. Thus, the following definition is equivalent to the previous one.

  view PosetToToset from POSET to TOSET is  

In this example the PosetToToset view represents the inclusion of the POSET theory into TOSET.

In those cases in which a view defines a theory inclusion from TRIV into another theory, we recommend following the convention of naming the view with the name of the target theory. An example that will be very useful later is the inclusion of TRIV into TOSET, which is expressed as a view as follows:

  view TOSET from TRIV to TOSET is  

Let us finish this section by commenting on some subtle issues that can arise with operator mappings:

6.3.3 Parameterized modules

System modules and functional modules can be parameterized. A parameterized system module has syntax

  mod M{X1 :: T1 , , Xn :: Tn} is ... endm

with n 1. Parameterized functional modules have completely analogous syntax.

The {X1 :: T1 ,, Xn :: Tn} part is called the interface, where each pair Xi ::Ti is a parameter, and each Xi is an identifier—the parameter name or parameter label—and each Ti is an expression that yields a theory—the parameter theory. Each parameter name in an interface must be unique, although there is no uniqueness restriction on the parameter theories of a module—we can have, e.g., two TRIV parameters. The parameter theories of a functional module must be functional theories.

In a parameterized module M, all the sorts and statement labels coming from theories in its interface must be qualified by their names. Thus, given a parameter Xi ::Ti, each sort S in Ti must be qualified as Xi$S, and each label l of a statement occurring in Ti must be qualified as Xi$l. In fact, the parameterized module M is flattened as follows. For each parameter Xi ::Ti, a renamed copy of the theory Ti, called Xi ::Ti is included. The renaming maps each sort S to Xi$S, and each label l of a statement occurring in Ti to Xi$l. The renaming percolates down through nested inclusions of theories, but has no effect on importations of modules. Thus, if Ti includes a theory T, when the renamed theory Xi ::Ti is created and included into M, and the renamed theory Xi ::T will also be created and included into Xi ::Ti.5 However, the renaming will have no effect on modules imported by either the Ti or T; for example, if BOOL is imported by one of these theories, it is not renamed, but imported in the same way into M.

For example, a parameterized module PRELIM-SET with TRIV as interface can be defined as follows:

  fmod PRELIM-SET{X :: TRIV} is  
    protecting BOOL .  
    sorts Set NeSet .  
    subsorts X$Elt < NeSet < Set .  
    op empty : -> Set .  
    op _,_ : Set Set -> Set [assoc comm id: empty] .  
    op _,_ : NeSet NeSet -> NeSet [ditto] .  
    op _in_ : X$Elt Set -> Bool .  
    op _-_ : Set Set -> Set .   *** set difference  
    var  E : X$Elt .  
    vars S S’ : Set .  
    eq E, E = E .  
    eq E in E, S = true .  
    eq E in S = false [owise] .  
    eq (E, S) - (E, S’) = S - (E, S’) .  
    eq S - S’ = S [owise] .  

In Maude—unlike OBJ3 and other similar languages—sorts are not systematically qualified by their module name. This convention of not qualifying sorts may be particularly weak when dealing with parameterized modules. However, given that Maude supports ad-hoc overloading and that constants can be qualified in order to be disambiguated (see Section 3.9.3), the problem of ambiguity in a signature is reduced to collisions of sorts. For example, in a module one may very easily need sets of integers and sets of quoted identifiers, in which case, given the specification of the PRELIM-SET module above, we would get two Set sorts from different importations which would be confused into one sort. Our solution consists in qualifying parameterized sorts, not with the module expression they belong to, but with the name of the view or views used in the instantiation of the parameterized module. Since we assume that all views are named, these names are the ones used in the qualification. Specifically, in the body of a parameterized module M{X1 ::T1 ,,Xn ::Tn}, any sort S can be written in the form S{X1 ,,Xn}. When the module is instantiated with views V 1 V n, then this sort is instantiated to S{V 1 ,,V n}.

Note that, although we strongly recommend it, the parameterization of sorts is optional, and therefore, for example, the above PRELIM-SET specification is a perfectly valid parameterized module.

Sorts declared in the parameterized module M{X1 ::T1 ,,Xn ::Tn} may in general be parameterized as S{Y 1 ,,Y m}, with m 1, and where each Y j is an Xi. It is recommended that all sorts declared in a parameterized module be parameterized with m = n and Y j = Xj for 1 j n, but this is not enforced—parameterized sorts may duplicate, omit, or reorder parameters and unparameterized sorts are also allowed.

Thus, the previous PRELIM-SET module to define sets could instead have been specified in a better way as follows:

  fmod BASIC-SET{X :: TRIV} is  
    protecting BOOL .  
    sorts Set{X} NeSet{X} .  
    subsorts X$Elt < NeSet{X} < Set{X} .  
    op empty : -> Set{X} .  
    op _,_ : Set{X} Set{X} -> Set{X} [assoc comm id: empty] .  
    op _,_ : NeSet{X} NeSet{X} -> NeSet{X} [ditto] .  
    op _in_ : X$Elt Set{X} -> Bool .  
    op _-_ : Set{X} Set{X} -> Set{X} .   *** set difference  
    var  E : X$Elt .  
    vars S S’ : Set{X} .  
    eq E, E = E .  
    eq E in E, S = true .  
    eq E in S = false [owise] .  
    eq (E, S) - (E, S’) = S - (E, S’) .  
    eq S - S’ = S [owise] .  

When this module is instantiated with the predefined view Int, the sort Set{X} becomes Set{Int}, and when it is instantiated with the predefined view Qid (see Section 7.11.1) it becomes Set{Qid}. In the following sections we will see additional examples of how this qualification convention for the sorts of a parameterized module avoids many unintended collisions of sort names, thus making renaming practically unnecessary.6

As another simple example of parameterized module, we consider a module MAYBE{X :: TRIV} in which we declare a sort Maybe{X} as a supersort of the sort Elt of the parameter theory and a constant maybe of this sort Maybe{X}. This technique is useful to declare a partial function as a total function, as we will see in the PFUN module of Section 15.3.2.

  fmod MAYBE{X :: TRIV} is  
    sort Maybe{X} .  
    subsort X$Elt < Maybe{X} .  
    op maybe : -> Maybe{X} [ctor] .  

The PRELIM-SET, BASIC-SET, and MAYBE modules above have only one parameter. In general, however, parameterized modules can have several parameters. It can furthermore happen that several parameters are declared with the same parameter theory, that is, we can have, for example, an interface of the form {X :: TRIV, Y :: TRIV} involving two copies of the theory TRIV. Therefore, parameters cannot be treated as normal submodules, since we do not want them to be shared when their labels are different. We regard the relationship between the body of a parameterized module and the interface of its parameters not as an inclusion, but as a module constructor which is evaluated generating renamed copies of the parameters, which are then included. For the above interface, two copies of the theory TRIV are generated, with names X :: TRIV and Y :: TRIV. As already mentioned, in such copies of parameter theories, sorts are renamed as follows: if Z is the label of a parameter theory T, then each sort S in T is renamed to Z$S and each statement label l is renamed to Z$l. All occurrences of these sorts and labels in the body of the parameterized module must mention their corresponding renaming.

Let us consider as an example the following module PAIR, in which we would like to point out the use of the qualifications for the sorts coming from each of the parameters.

  fmod PAIR{X :: TRIV, Y :: TRIV} is  
    sort Pair{X, Y} .  
    op <_;_> : X$Elt Y$Elt -> Pair{X, Y} .  
    op 1st : Pair{X, Y} -> X$Elt .  
    op 2nd : Pair{X, Y} -> Y$Elt .  
    var A : X$Elt .  
    var B : Y$Elt .  
    eq 1st(< A ; B >) = A .  
    eq 2nd(< A ; B >) = B .  

As already mentioned, if a parameter theory is structured, this renaming process for parameter theories is carried out not only at the top level, but for the whole “theory part,” that is, renaming subtheories but not renaming submodules. Consider, for example, the following parameterized module defining a lexicographical ordering on pairs of elements of two totally strictly ordered sets.

  fmod LEX-PAIR{X :: STOSET, Y :: STOSET} is  
    sort Pair{X, Y} .  
    op <_;_> : X$Elt Y$Elt -> Pair{X, Y} .  
    op _<_ : Pair{X, Y} Pair{X, Y} -> Bool .  
    op 1st : Pair{X, Y} -> X$Elt .  
    op 2nd : Pair{X, Y} -> Y$Elt .  
    vars A A’ : X$Elt .  
    vars B B’ : Y$Elt .  
    eq 1st(< A ; B >) = A .  
    eq 2nd(< A ; B >) = B .  
    eq < A ; B > < < A’ ; B’ > = (A < A’) or (A == A’ and B < B’) .  

Representing by boxes the modules (with initiality constraints), by ovals the theories (with loose semantics), by triple arrows the protecting and parameter importations, and by single arrows the including importations, we can depict the structure of the LEX-PAIR functional module defining a lexicographic order on pairs as in Figure 6.2, where we have two copies not only of STOSET but also of the SPOSET and TAOSET subtheories (see also Figure 6.1 in page 338), but only one copy of the BOOL submodule.


Figure 6.2: Structure of LEX-PAIR

The parameter theory of a module can be any module expression whose result is a theory. The following module defines bags of elements with an occurrences operation that returns the number of occurrences of a particular element in a given bag.

  fmod BAG{X :: TRIV * (sort Elt to Element)} is  
    protecting NAT .  
    sorts Bag{X} NeBag{X} .  
    subsorts X$Element < NeBag{X} < Bag{X} .  
    op mt : -> Bag{X} .  
    op __ : Bag{X} Bag{X} -> Bag{X} [assoc comm id: mt] .  
    op __ : Bag{X} NeBag{X} -> NeBag{X} [ditto] .  
    op occurrences : X$Element Bag{X} -> Nat .  
    vars E E’ : X$Element .  
    var  S : Bag{X} .  
    eq occurrences(E, E S) = 1 + occurrences(E, S) .  
    eq occurrences(E, S) = 0 [owise] .  

Module instantiation will be explained in the next section, and then we shall see some execution examples.

6.3.4 Module instantiation

Instantiation is the process by which actual parameters are bound to the formal parameters of a parameterized module and a new module is created as a result. This can be seen in fact as the evaluation of a module expression. The instantiation requires a view from each formal parameter to its corresponding actual parameter. Each such view is then used to bind the names of sorts, operators, etc. in the formal parameters to the corresponding sorts, operators (or expressions), etc. in the actual target.

The instantiation of a parameterized module must be made with views explicitly defined previously. Thus, given the views Int (from TRIV to INT) and IntAsStoset (from STOSET to INT), both introduced in Section 6.3.2, we can define sets of integers with the module expression BASIC-SET{Int}, and lexicographically ordered pairs of integers with LEX-PAIR{IntAsStoset, IntAsStoset}.

As mentioned in Section 6.3.2, there are also views from theories to theories. Using such views we can, for example, instantiate the module BASIC-SET with the view TOSET (from TRIV to TOSET) given also in Section 6.3.2. The result is a module BASIC-SET{TOSET} which is still parameterized, but now by the theory TOSET. We can instantiate it again with a view from TOSET to some other theory or module, for example, IntAsToset (from TOSET to INT), obtaining the module BASIC-SET{TOSET}{IntAsToset}, which defines sets of integers. Note that certain new operations, which would not be meaningful in the original BASIC-SET module, could now be defined in a totally parametric way in an extension of BASIC-SET{TOSET}. For example, we could define in this way a maximum function

  op max : NeSet{TOSET}{X} -> X$Elt .

as done in the SET-MAX module later in this section.

Another interesting use of parameterized modules is the linking of parameters. Suppose that we wish to define lists of sets of elements. We may define a module SET-LIST parameterized by the theory TRIV that imports the module BASIC-SET and declares the sort SetList{X} with constructors nil and _;_. Note however that BASIC-SET is also a parameterized module, which must be instantiated to be imported. In cases like this one, we can use the label of the parameter to link the parameter of the module with the parameter of the submodule. Once the module is instantiated, the parameterized submodule gets instantiated with the same view. Thus, if the module SET-LIST below is instantiated by, say, the view Int to define lists of sets of integers, the submodule BASIC-SET also gets instantiated with the same view, providing a definition of sets of integers.7

  fmod SET-LIST{X :: TRIV} is  
    protecting BASIC-SET{X} .  
    sort SetList{X} .  
    subsort Set{X} < SetList{X} .  
    op nil : -> SetList{X} [ctor] .  
    op _;_ : SetList{X} SetList{X} -> SetList{X}  
        [ctor assoc id: nil] .  

As another example, let us consider the following modules MONOMIAL and POLYNOMIAL, defining, respectively, monomials on a set of variables and polynomials on a commutative ring and a set of variables. First, the module MONOMIAL defines monomials as terms of the form X ^ N, with X a variable8 and N a nonzero natural number indicating the power to which the variable is raised, and with an empty syntax multiplication operation __ on monomials.

  fmod MONOMIAL{X :: TRIV} is  
    protecting NAT .  
    sorts Pow{X} Mon{X} .  
    subsorts Pow{X} < Mon{X} .  
    *** multiplication  
    op __ : Mon{X} Mon{X} -> Mon{X} [assoc comm] .  
    op _^_ : X$Elt NzNat -> Pow{X} .  
    var  X : X$Elt .  
    vars N M : NzNat .  
    eq (X ^ N) (X ^ M) = X ^ (N + M) .  

Once we have the specification of monomials, we can specify polynomials as monomials with coefficients in some commutative ring, and with addition and multiplication operations. Thus, for specifying polynomials on a ring and a set of variables in a module POLYNOMIAL, we need to import the above module MONOMIAL. But notice that POLYNOMIAL is parameterized by two theories: RING, for the coefficients, and TRIV, for the variables. Since we need to import monomials on the same set of variables, we need to bind or link such parameters. This linking is done by means of the label X of the parameter theory X :: TRIV.

  fmod POLYNOMIAL{R :: RING, X :: TRIV} is  
    protecting MONOMIAL{X} .  
    sorts Poly{R, X} .  
    subsorts R$Ring < Poly{R, X} .  
    *** multiplication  
    op __ : Poly{R, X} Poly{R, X} -> Poly{R, X} [assoc comm] .  
    *** addition  
    op _++_ : Poly{R, X} Poly{R, X} -> Poly{R, X} [assoc comm] .  
    op --_ : Poly{R, X} -> Poly{R, X} .  
    op __ : R$Ring Mon{X} -> Poly{R, X} .  
    vars A B : R$Ring .  
    vars U V : Mon{X} .  
    vars P Q R : Poly{R, X} .  
    eq P ++ z = P .  
    eq P ++ (-- P) = z .  
    eq P e = P .  
    eq -- (P ++ Q) = (-- P) ++ (-- Q) .  
    eq -- (A U) = (- A) U .  
    eq P (Q ++ R) = (P Q) ++ (P R) .  
    eq z U = z .  
    eq z P = z .  
    eq A (B U) = (A B) U .  
    eq (A U) ++ (B U) = (A ++ B) U .  
    eq (A U) (B V) = (A B) (U V) .  
    eq A B = A * B .  
    eq A ++ B = A + B .  

If the module POLYNOMIAL is instantiated with, say, views RingToRat and Qid, the submodule MONOMIAL then gets automatically instantiated with Qid, thanks to the binding of the parameters.

As an additional example, let us give a more concise definition of the parameterized module LEX-PAIR{X :: STOSET, Y :: STOSET} given in Section 6.3.3 using these ideas as follows:

  view STOSET from TRIV to STOSET is  

  fmod LEX-PAIR{X :: STOSET, Y :: STOSET} is  
    protecting PAIR{STOSET, STOSET}{X, Y} .  
    op _<_ :  
        Pair{STOSET, STOSET}{X, Y} Pair{STOSET, STOSET}{X, Y} -> Bool .  
    vars A A’ : X$Elt .  
    vars B B’ : Y$Elt .  
    eq < A ; B > < < A’ ; B’ > = (A < A’) or (A == A’ and B < B’) .  

In Section 6.2.2, we presented a NAT-LIST-MAX module in which we defined a max function that returns the greatest element of a list of natural numbers. However, we can define such a function on lists or sets of any type of elements as long as there is a total order relation available for them. Let us consider the following module SET-MAX, parameterized by the theory TOSET (see Section 6.3.1. Given a non-empty finite set of elements in a totally ordered set, the operation max returns the maximum element in the set. Note that we have used the or-else operator for short-circuit disjunction from the EXT-BOOL module to improve the efficiency of the calculation.

  fmod SET-MAX{T :: TOSET} is  
    protecting BASIC-SET{TOSET}{T} .  
    protecting EXT-BOOL .  
    op max : NeSet{TOSET}{T} -> T$Elt .  
    var E : T$Elt .  
    var S : Set{TOSET}{T} .  
    eq max(E, S)  
      = if S == empty or-else max(S) < E  
        then E  
        else max(S)  
        fi .  

We can now calculate the maximum of a set of integers by instantiating this module with the view IntAsToset introduced in Section 6.3.2. Notice that in this example we need an extra set of parentheses to disambiguate between the operator max just defined and the associative operator max on integers.

  fmod INT-SET-MAX is  
    protecting SET-MAX{IntAsToset} .  

  Maude> red max((4, 3, 5, 2, 1)) .  
  result NzNat: 5

Similarly, we can calculate the greatest element in sets of any type with a total order relation; for example, sets of strings, by using the view StringAsToset also introduced in Section 6.3.2:

  fmod STRING-SET-MAX is  
    protecting SET-MAX{StringAsToset} .  

  Maude> red max("four", "three", "five", "two", "one") .  
  result String: "two"

Notice that, if we have several parameters, we can instantiate the parameterized module or theory with some views going to theories and others going to modules. The result in such case is the expected one, that is, we get a module or theory parameterized by the targets of those views going to theories. For example, the module RAT-POLY below gives us a specification of the polynomials with rational coefficients by just importing the module POLYNOMIAL introduced above instantiated with the view RingToRat from the theory RING to the functional module RAT (see Section 6.3.2).

  fmod RAT-POLY{X :: TRIV} is  
    protecting POLYNOMIAL{RingToRat, X} .  

We can then define the polynomials with rational coefficients and with quoted identifiers as variables by instantiating the module RAT-POLY with the following Qid view, which is predefined in Maude (see Section 7.11.1).

  view Qid from TRIV to QID is  
    sort Elt to Qid .  

  fmod QID-RAT-POLY is  
    pr RAT-POLY{Qid} .  

Let us reduce as an example the following polynomial expression:

  Maude> red in QID-RAT-POLY :  
           (((2 / 3) ((’X ^ 2) (’Y ^ 3)))  
            ++ ((7 / 5) ((’Y ^ 2) (’Z ^ 5))))  
           (((1 / 7) (’U ^ 2))  
            ++ (1 / 2)) .  
  result Poly{RingToRat, Qid}:  
              (1/3  (’X ^ 2) ’Y ^ 3)  
           ++ (1/5  (’U ^ 2) (’Y ^ 2) ’Z ^ 5)  
           ++ (2/21 (’U ^ 2) (’X ^ 2) ’Y ^ 3)  
           ++ (7/10 (’Y ^ 2) ’Z ^ 5)

Summarizing, a parameterized module M{X1 ::T1 ,,Xn ::Tn} with n free parameters is instantiated by the module expression M{A1, , An}, where each Ai is an instance of one of the following three alternatives:

Parameterized modules with free parameters cannot be imported: first all of the free parameters must be instantiated away. Parameterized modules with bound parameters may only be imported, since they were created for module expressions in a context where the parameters are bound by an enclosing parameterized module.

Parameterized functional modules may be instantiated with views that have system modules as their targets; then the instantiated module is promoted to a system module.

Parameterized modules cannot be summed, even if all the parameters are bound. Parameterized modules may be renamed, but the renaming must not affect any sorts or operators coming from a parameter theory. The result of renaming a parameterized module is a parameterized module with the same parameters, and we can use it as any other parameterized module; for example, we can instantiate it with a view, or bind its parameters to the parameters of the module in which the module expression is being imported, as in the following example, where we rename the SET-LIST parameterized module above.

  fmod MY-SET-LIST{Y :: TRIV} is  
    pr (SET-LIST  
          * (sort Set{X} to MySet{X},  
             op __ : SetList{X} SetList{X} -> SetList{X} to _._))  
          {Y} .  

  fmod MY-QID-SET-LIST is  
    protecting MY-SET-LIST{Qid} .  

The SET-LIST module has only free parameters and so it can be renamed; however its renaming imports the renaming of BASIC-SET{X} which has a bound parameter. Note that the parameter of the sorts appearing in the renaming of the SET-LIST module is X, since this is the label of the parameter in such module. We have used label Y for the parameter of MY-SET-LIST to emphasize this fact, although they could be the same.

Allowing renaming of modules with bound parameters requires that renamings be capable of instantiation; that is, parameterized sort names inside a renaming have their parameters instantiated, with an extra pair of curly brackets being added in the case of instantiation by a view with a theory as target.

Let us illustrate these ideas. When, due to instantiation by a view with a theory as target, a bound parameter in a renamed module escapes and needs to be rebound by an extra instantiation, the extra instantiation is inserted before rather than after the renaming. Let us consider the following example, where we use the views TOSET, from the theory TRIV to the theory TOSET, and IntAsToset, from the theory TOSET to the predefined module INT, both described in Section 6.3.2.

  fmod RENAMING-PAR-MOD-A{X :: TRIV} is  
    sort Foo{X} .  
    op f : Foo{X} -> Foo{X} .  

  fmod RENAMING-PAR-MOD-B{X :: TRIV} is  
    extending RENAMING-PAR-MOD-A{X} .  
    sort Bar{X} .  
    op g : Bar{X} -> Foo{X} .  

  fmod RENAMING-PAR-MOD-C is  
    pr (RENAMING-PAR-MOD-B * (sort Foo{X} to Foo’{X},  
               sort Bar{X} to Bar’{X},  
               op f : Foo{X} -> Foo{X} to f’,  
               op g : Bar{X} -> Foo{X} to g’)) {TOSET} {IntAsToset} .  

In this case, the module RENAMING-PAR-MOD-A gets instantiated before it is renamed:

    * (sort Foo{TOSET}{IntAsToset} to Foo’{TOSET}{IntAsToset},  
       op f : [Foo{TOSET}{IntAsToset}] -> [Foo{TOSET}{IntAsToset}]  
         to f’)

Passing parameters from an enclosing module in nonfinal instantiations is prohibited. This restriction avoids many subtle issues. Thus:

  fmod ILLEGAL-INST{X :: RING, Y :: POSET} is  
    protecting POLYNOMIAL{X, POSET}{Y} .  

is illegal, because X occurs in the nonfinal instantiation POLYNOMIAL{X, POSET}. With appropriate views, this example can be correctly written as follows:

  view RING from RING to RING is  

  view POSET from TRIV to POSET is  

  fmod LEGAL-INST{X :: RING, Y :: POSET} is  
    protecting POLYNOMIAL{RING, POSET}{X, Y} .  

Another way of viewing this restriction is that parameters from an enclosing module and views with theories as targets may not occur in the same instantiation. Note that views with theories as targets may never occur in a final instantiation (otherwise there would be free parameters in an import) and must occur in any nonfinal instantiation (otherwise there would be no free parameters for the next instantiation).

6.3.5 Lists

There are different ways of building lists. One possibility is to begin with the empty list and the singleton lists, and then use the concatenation operation to get bigger lists. However, concatenation cannot be a free list constructor, because it satisfies an associativity equation and has the empty list as identity. This approach will be used in the predefined module for generic lists described in Section 7.12.1, and appears in many similar examples throughout this book. Given the support for equational attributes (associativity, commutativity, etc.) in Maude, as explained in Section 4.4.1, one can argue that this is indeed the most natural specification for lists in Maude.

Here we use instead the two standard free constructors for lists that can be found in many functional programming languages: the empty list nil, here denoted [], and the cons operation that adds an element to the beginning of a list, here denoted with the mixfix syntax _:_. This approach facilitates proving properties of lists by structural induction in Maude’s inductive theorem prover (ITP), and provides a simple basis for specifying sorted lists and sorting operations on them in Section 6.3.6.

As usual, head and tail are the selectors associated with the _:_ constructor. Since they are not defined on the empty list, we avoid their partiality in the same way as we have done for stacks and queues in the previous sections by means of a subsort NeList of non-empty lists.

  fmod LIST-CONS{X :: TRIV} is  
    protecting NAT .  
    sorts NeList{X} List{X} .  
    subsort NeList{X} < List{X} .  
    op [] : -> List{X} [ctor] .  
    op _:_ : X$Elt List{X} -> NeList{X} [ctor] .  
    op tail : NeList{X} -> List{X} .  
    op head : NeList{X} -> X$Elt .  
    var E : X$Elt .  
    var N : Nat .  
    vars L L’ : List{X} .  
    eq tail(E : L) = L .  
    eq head(E : L) = E .

Three interesting operations on lists are list concatenation (here denoted with mixfix syntax _++_), the length of a list, and reversing a list. The length operator has a result of sort Nat, that comes from the predefined module NAT, imported in protecting mode. These three operations are defined as usual by structural induction on the two constructors, with an equation for the empty base case and another for the cons case E : L.

Here we are not concerned with efficiency and therefore we just specify the operations in a simple way, without using, for example, tail-recursive auxiliary operations in the style of Section 7.12.1.

    op _++_ : List{X} List{X} -> List{X} .  
    op length : List{X} -> Nat .  
    op reverse : List{X} -> List{X} .  
    eq [] ++ L = L .  
    eq (E : L) ++ L’ = E : (L ++ L’) .  
    eq length([]) = 0 .  
    eq length(E : L) = 1 + length(L) .  
    eq reverse([]) = [] .  
    eq reverse(E : L) = reverse(L) ++ (E : []) .

In this specification of generic lists we also add two operations that will be useful later, in Section 6.3.6, when sorting lists: take_from_ and throw_from_. The first one builds a list by taking the first n elements of the given list, while the second one deletes the first n elements of the given list. Both of them are defined by structural induction on both arguments, the base case being when either the first is 0 or the second is empty. As usual, s_ denotes the successor operator on natural numbers.

    op take_from_ : Nat List{X} -> List{X} .  
    op throw_from_ : Nat List{X} -> List{X} .  
    eq take 0 from L = [] .  
    eq take N from [] = [] .  
    eq take s(N) from (E : L) = E : take N from L .  
    eq throw 0 from L = L .  
    eq throw N from [] = [] .  
    eq throw s(N) from (E : L) = throw N from L .  

The following sample reduction shows the result of reversing a list of character strings.

  fmod LIST-CONS-TEST is  
    protecting LIST-CONS{String} .  

  Maude> red reverse("one" : "two" : "three" : []) .  
  result NeList{String}: "three" : "two" : "one" : []

6.3.6 Sorted lists

In order-sorted equational specifications, subsorts must be defined by means of constructors, but it is not possible to have a subsort of sorted lists, for example, defined by a property over lists; a more expressive formalism is needed. Membership equational logic allows subsort definition by means of conditions involving equations and/or sort predicates. In this example we use this technique to define a subsort of sorted lists, included in the sort of lists imported from the module LIST-CONS in Section 6.3.5. Furthermore, we will also specify here different well-known sorting algorithms.

Parameterized sorted lists need a stronger requirement than TRIV, because a total order over the elements to be sorted is needed. Since repetitions pose no problems for sorting a list, the order relation should be non-strict, like in the NSTOSET theory introduced in Section 6.3.1. However, for the specification of the sorting algorithms, it is more convenient to use also the strict version of the order. For these reasons, we will use as requirement for parameterized sorted lists the theory TOSET, also introduced in Section 6.3.1.

The parameterized module for sorted lists imports the parameterized list module. However, note that we want lists over a totally ordered set, instead of lists over any set; therefore, first we partially instantiate LIST-CONS with an inclusion view from the theory TRIV to the theory TOSET.

  view TOSET from TRIV to TOSET is  

We are still left with a parameterized module and corresponding dependent sorts, but now with respect to the TOSET requirement. This is the reason justifying the notation LIST-CONS{TOSET}{X} in the protecting importation below, as well as NeList{TOSET}{X} and List{TOSET}{X} as names of the imported sorts.

Notice the three (conditional) membership axioms defining the subsort SortedList{X}: the empty and singleton lists are always sorted, and a longer list is sorted when the first element is less than or equal to the second, and the list without the first element is also sorted.

  fmod SORTED-LIST{X :: TOSET} is  
    protecting LIST-CONS{TOSET}{X} .  
    sorts SortedList{X} NeSortedList{X} .  
    subsorts NeSortedList{X} < SortedList{X} < List{TOSET}{X} .  
    subsort NeSortedList{X} < NeList{TOSET}{X} .  
    vars N M : X$Elt .  
    vars L L’ : List{TOSET}{X} .  
    vars OL OL’ : SortedList{X} .  
    var NEOL : NeSortedList{X} .  
    mb [] : SortedList{X} .  
    mb (N : []) : NeSortedList{X} .  
    cmb (N : NEOL) : NeSortedList{X} if N <= head(NEOL) .

As part of this module, we also define several well-known sorting operations: insertion-sort, quicksort, and mergesort, based on appropriate auxiliary operations. The important point is that we are able to give finer typing to all these sorting operations than the usual typing in other algebraic specification frameworks or functional programming languages. For example, insertion-sort is declared as an operation from List{TOSET}{X} to SortedList{X}, instead of the much less informative typing from List{TOSET}{X} to List{TOSET}{X}. The same applies to each of the auxiliary operations. Furthermore, a function that requires its input argument to be a sorted list can now be defined as a total function, whereas in less expressive typing formalisms it would have to be either partial, or to be defined with exceptional behavior on the erroneous arguments.

The operation insert-list inserts an element in the appropriate position of an already sorted list, so that the resulting list is also sorted. The sorting operation insertion-sort recursively sorts the list without the first element and then calls insert-list, which inserts the missing element in the correct position.

    op insertion-sort : List{TOSET}{X} -> SortedList{X} .  
    op insert-list : SortedList{X} X$Elt -> SortedList{X} .  
    eq insertion-sort([]) = [] .  
    eq insertion-sort(N : L) = insert-list(insertion-sort(L), N) .  
    eq insert-list([], M) = M : [] .  
    ceq insert-list(N : OL, M) = M : N : OL if M <= N .  
    ceq insert-list(N : OL, M) = N : insert-list(OL, M) if N < M .

The sorting operation mergesort splits a given list in half by means of the operations take_from_ and throw_from_ described in Section 6.3.5 above, recursively sorts each sublist, and then calls the commutative merge operation on the sorted sublists to obtain the final sorted result. In Section 7.12.6 on sortable lists there is a more efficient (albeit more complex) definition of the mergesort algorithm on lists.

    op mergesort : List{TOSET}{X} -> SortedList{X} .  
    op merge : SortedList{X} SortedList{X} -> SortedList{X} [comm] .  
    eq mergesort([]) = [] .  
    eq mergesort(N : []) = N : [] .  
    ceq mergesort(L)  
      = merge(mergesort(take (length(L) quo 2) from L),  
              mergesort(throw (length(L) quo 2) from L))  
      if length(L) > 1 .  
    eq merge(OL, []) = OL .  
    ceq merge(N : OL, M : OL’) = N : merge(OL, M : OL’) if N <= M .

Finally, quicksort works on a list by separating its elements into those smaller than the first element (taken as the pivot) and those bigger than the first, recursively sorts each of the resulting lists, and simply puts them together by concatenating them with the pivot in the middle.

    op quicksort : List{TOSET}{X} -> SortedList{X} .  
    op leq-elems : List{TOSET}{X} X$Elt -> List{TOSET}{X} .  
    op gr-elems : List{TOSET}{X} X$Elt -> List{TOSET}{X} .  
    eq quicksort([]) = [] .  
    eq quicksort(N : L)  
     = quicksort(leq-elems(L,N)) ++ (N : quicksort(gr-elems(L,N))) .  
    eq leq-elems([], M) = [] .  
    ceq leq-elems(N : L, M) = N : leq-elems(L, M) if N <= M .  
    ceq leq-elems(N : L, M) = leq-elems(L, M) if M < N .  
    eq gr-elems([], M) = [] .  
    ceq gr-elems(N : L, M) = gr-elems(L, M) if N <= M .  
    ceq gr-elems(N : L, M) = N : gr-elems(L, M) if M < N .  

We now apply the sorting operations to lists of natural numbers.

  view NatAsToset from TOSET to NAT is  
    sort Elt to Nat .  

  fmod SORTED-LIST-TEST is  
    protecting SORTED-LIST{NatAsToset} .  

  Maude> red insertion-sort(5 : 4 : 3 : 2 : 1 : 0 : []) .  
  result NeSortedList{NatAsToset}: 0 : 1 : 2 : 3 : 4 : 5 : []  
  Maude> red mergesort(5 : 3 : 1 : 0 : 2 : 4 : []) .  
  result NeSortedList{NatAsToset}: 0 : 1 : 2 : 3 : 4 : 5 : []  
  Maude> red quicksort(0 : 1 : 2 : 5 : 4 : 3 : []) .  
  result NeSortedList{NatAsToset}: 0 : 1 : 2 : 3 : 4 : 5 : []