Chapter 15
Full Maude: Extending Core Maude

During the development of the Maude system we have put special emphasis on the creation of metaprogramming facilities to allow the generation of execution environments for a wide variety of languages and logics. The first most obvious area where Maude can be used as a metalanguage is in building language extensions for Maude itself. Our experience in this regard—first reported in [45], and further documented in [46404147]—is very encouraging.

We have been able to define in Core Maude a language, that we call Full Maude, with all the features of Maude plus notation for object-oriented programming, parameterized views, module expressions specifying tuples of any size, etc. Although the Maude distribution has included the specification/implementation of Full Maude since it was first distributed in 1999, Core Maude and Full Maude are now closer than ever before. Many of the features now available in Core Maude, like parameterized modules, views, and module expressions like summation, renaming and instantiation, were available in Full Maude long before they were available in Core Maude [45]. In fact, Full Maude has not only been a complement to Core Maude, but also a vehicle to experiment with new language features. Once these features have been mature enough to be implemented in the core language, we have made the effort to do so. Similarly, it is very likely that those features in Full Maude which are not yet available in Core Maude will become part of it sooner or later, and that new features will be added to Full Maude for purposes of language design and experimentation. This applies not only to Full Maude, but also to further language extensions based on Full Maude such as the strategy language proposed in [88], whose Core Maude implementation is currently underway.

Full Maude implements a complete user interface for the extended language. Using the META-LEVEL and LOOP-MODE modules, we have been able to define in Core Maude all the additional functionality required for parsing, evaluating, and pretty-printing modules in the extended language, and also for input/output interaction, as already discussed in Chapter 13. Thanks to the efficient implementation of the rewrite engine, the parser, and the META-LEVEL module, such a language extension executes with reasonable efficiency.

Full Maude contains Core Maude as a sublanguage, so that Core Maude modules can also be entered at the Full Maude level. However, currently there are a few syntactic restrictions that have to be satisfied by modules and commands in order to be acceptable inputs at the Full Maude level, including the fact that Full Maude inputs, for both modules and commands, must be enclosed in parentheses. These syntactic restrictions are explained in Section 15.6.

The structure of this chapter is as follows. Section 15.1 gives instructions on how to load and use Full Maude, how to enter modules, reduce terms, trace executions, etc. Section 15.2 explains how modules in Core Maude’s database may be used in Full Maude. Section 15.3 introduces the additional module operations that are available in Full Maude. Section 15.4 explains how to move terms and modules up and down reflection levels. Finally, Section 15.6 enumerates the main differences between Full Maude and Core Maude.

15.1 Running Full Maude

Since the execution environment for Full Maude has been implemented in Core Maude, to initialize the system so that we can start using it the first thing we have to do is to load the FULL-MAUDE module in the system. Assuming that the file full-maude.maude, which contains the executable specification of Full Maude, is located in the current directory (or in a place where Maude can locate it, see Section 2.2), we just need to type the corresponding in or load command in the Maude prompt:

  Maude> load full-maude.maude  
 
              Full Maude 2.7.1 Jun 30th 2016

The Full Maude system is then loaded, and we can use it as any other module.

Since Maude can take file names as arguments when started, assuming one is working on a Linux platform, one may also run Maude as follows:

  ~/maude-linux/bin$ ./maude.linux full-maude.maude  
                     \||||||||||||||||||/  
                   --- Welcome to Maude ---  
                     /||||||||||||||||||\  
                Maude 2.7.1 built: Jun 27 2016 16:43:23  
            Copyright 1997-2016 SRI International  
               Tue Jun 28 09:25:34 2016  
 
              Full Maude 2.7.1 Jun 30th 2016

At the end of this file full-maude.maude there is the command

  loop init .

which initializes the system just after loading the specification. This command starts the read-eval-print loop (see Section 13.1) to allow the interaction with the user by entering modules, theories, views, and commands, and to maintain a database in which to store all the modules, theories and views being introduced. The term init is a constant of sort System, in the specification of Full Maude, standing for the initial state of the Full Maude database.

Typing control-C may result in the loop being broken, and with it the current execution of Full Maude. Maude may try to recover the loop by itself, but if it is not successful we must reinitialize it with the loop command. That is, we need to type

  Maude> loop init .

This command will be successful only if the full-maude.maude file is loaded and the FULL-MAUDE module is the default one. If it is not the default one, we may select it with the select command (see Section 18.13):

  Maude> select FULL-MAUDE .  
  Maude> loop init .

The loop init command may be omitted here: Maude will try to restart the loop, using the last loop command, if something is written in parentheses henceforth.

Let us recall from Section 13.1 that to get something into the LOOP-MODE system the text has to be enclosed in parentheses. This means that any module, theory, view, or command intended for Full Maude has to be enclosed in parentheses. Since Core Maude is running underneath Full Maude—indeed, it now provides what might be called the system programming level—it will handle any input not enclosed in parentheses. This allows the possibility of using both systems at the same time. Thanks to this, we may use many Core Maude commands when interacting with Full Maude. For example, we may use Core Maude trace or profile facilities on Full Maude specifications, may load files, etc. However, this may lead to some confusion, and we should take care of putting parentheses around those pieces of text intended for Full Maude.

A Core Maude module, such as those presented in previous sections, can be entered in Full Maude by enclosing it in parentheses. For example, a module PATH1 can be entered to Full Maude as follows:

  Maude> (fmod PATH is  
            sorts Node Edge .  
            ops source target : Edge -> Node .  
 
            sort Path .  
            subsort Edge < Path .  
            op _;_ : [Path] [Path] -> [Path] .  
 
            var  E : Edge .  
            vars P Q R S : Path .  
            cmb E ; P : Path if target(E) = source(P) .  
            ceq (P ; Q) ; R  
              = P ; (Q ; R)  
              if target(P) = source(Q) /\ target(Q) = source(R) .  
 
            ops source target : Path -> Node .  
            ceq source(P) = source(E) if E ; S := P .  
            ceq target(P) = target(S) if E ; S := P .  
 
            protecting NAT .  
 
            ops n1 n2 n3 n4 n5 : -> Node .  
            ops a b c d e f : -> Edge .  
            op length : Path -> Nat .  
 
            eq length(E) = 1 .  
            ceq length(E ; P) = 1 + length(P) if E ; P : Path .  
 
            eq source(a) = n1 .  
            eq target(a) = n2 .  
            eq source(b) = n1 .  
            eq target(b) = n3 .  
            eq source(c) = n3 .  
            eq target(c) = n4 .  
            eq source(d) = n4 .  
            eq target(d) = n2 .  
            eq source(e) = n2 .  
            eq target(e) = n5 .  
            eq source(f) = n2 .  
            eq target(f) = n1 .  
          endfm)  
 
  rewrites: 5438 in 10ms cpu (157ms real) (543800 rews/sec)  
  Introduced module PATH

As in Core Maude, we can enter any module or command by writing it directly after the prompt, or by having it in a file and then using the in or load commands. Also as in Core Maude, we can write several Full Maude modules or commands in a file and then enter all of them with a single in or load command (without parentheses), but each of the modules or commands has to be enclosed in parentheses.

When entering a module, as above, Maude gives us information about the rewrites executed to handle such a module. This is the number of rewrites done by Full Maude to evaluate the module being entered. In the same way, every time we enter a command, although in most cases it finally makes a call to Core Maude, Full Maude needs to perform some additional rewrites. Thus, as we will see below, the number of rewrites given by the system for Full Maude commands includes the reductions due to the evaluation of the command and those due to the execution of the command itself.

We can perform reduction or rewriting using a syntax for commands such as that of Core Maude.

  Maude> (red in PATH : b ; (c ; d) .)  
  rewrites: 893 in 30ms cpu (21ms real) (29766 rewrites/second)  
  reduce in PATH :  
    b ;(c ; d)  
  result Path :  
    b ;(c ; d)

  Maude> (red length(b ; (c ; d)) .)  
  rewrites: 474 in 10ms cpu (2ms real) (47400 rewrites/second)  
  reduce in PATH :  
    length(b ;(c ; d))  
  result NzNat :  
    3

  Maude> (red a ; (b ; c) .)  
  rewrites: 587 in 0ms cpu (2ms real) (~ rewrites/second)  
  reduce in PATH :  
    a ;(b ; c)  
  result [Path] :  
    a ;(b ; c)

  Maude> (red source(a ; (b ; c)) .)  
  rewrites: 616 in 0ms cpu (2ms real) (~ rewrites/second)  
  reduce in PATH :  
    source(a ;(b ; c))  
  result [Node] :  
    source(a ;(b ; c))

  rewrites: 622 in 0ms cpu (2ms real) (~ rewrites/second)  
  reduce in PATH :  
    target((a ; b); c)  
  result [Node] :  
    target((a ; b); c)

  Maude> (red length(a ; (b ; c)) .)  
  rewrites: 579 in 0ms cpu (2ms real) (~ rewrites/second)  
  reduce in PATH :  
    length(a ;(b ; c))  
  result [Nat] :  
    length(a ;(b ; c))

Note the number of rewrites. These figures include, as said above, the rewrites accomplished by Full Maude in the processing of the inputs and outputs, plus the number of rewrites of the reduction itself. For example, the first two reductions above in Core Maude would produce the following output:

  Maude> red in PATH : b ; (c ; d) .  
  reduce in PATH : b ; (c ; d) .  
  rewrites: 7 in 0ms cpu (23ms real) (~ rews/sec)  
  result Path: b ; (c ; d)  
 
  Maude> red length(b ; (c ; d)) .  
  reduce in PATH : length(b ; (c ; d)) .  
  rewrites: 12 in 0ms cpu (0ms real) (~ rews/sec)  
  result NzNat: 3

Tracing, debugging, profiling, and the other facilities available in Core Maude (see Section 14.1) are also available in Full Maude. Since these facilities are provided by Core Maude, the corresponding commands for managing them must be written without parentheses. For example, we can do the following:

  Maude> set trace on .  
  Maude> set trace mb off .  
  Maude> set trace condition off .  
  Maude> set trace substitution off .  
  Maude> (red length(b ; c) .)  
  *********** trial #1  
  ceq length(E:Edge ; P:Path) = length(P:Path) + 1  
    if E:Edge ; P:Path : Path .  
  *********** solving condition fragment  
  E:Edge ; P:Path : Path  
  *********** success for condition fragment  
  E:Edge ; P:Path : Path  
  *********** success #1  
  *********** equation  
  ceq length(E:Edge ; P:Path) = length(P:Path) + 1  
    if E:Edge ; P:Path : Path .  
  length(b ; c)  
  --->  
  length(c) + 1  
  *********** equation  
  eq length(E:Edge) = 1 .  
  length(c)  
  --->  
  1  
  *********** equation  
  (built-in equation for symbol _+_)  
  1 + 1  
  --->  
  2  
  rewrites: 444 in 0ms cpu (7ms real) (~ rewrites/second)  
  reduce in PATH :  
    length(b ; c)  
  result NzNat :  
    2

One should always bear in mind that Full Maude is part of the specification being run. The specification of Full Maude is loaded in the system, and as said above, some of the rewrites taking place are the result of applying equations or rules in these modules. In the case of tracing, the rewrites done by Full Maude are not shown thanks to one of the trace commands available, namely trace exclude (see Sections 14.1.1 and 18.6). With such a command we may exclude particular modules from being traced. In particular, the full-maude.maude file includes the command trace exclude FULL-MAUDE, where FULL-MAUDE is the top module of the specification of Full Maude.

15.2 Using Core Maude modules in Full Maude

Full Maude maintains a module database independent from the one used by Core Maude to store the modules entered into it. In fact, this module database is a Maude term stored as part of the state in the LOOP-MODE input/output object. Therefore, a module entered into Core Maude can only import modules previously entered into Core Maude. However, Full Maude modules can import modules previously entered either into Full Maude or into Core Maude. Basically, if Full Maude cannot find a module in its own database, it looks into Core Maude’s module database to find it.

When metaprogramming, the system behaves differently. In Core Maude, a metamodule (that is, the metarepresentation of a module) can include a module at the object level. In Full Maude, however, metamodules cannot import modules entered into Full Maude and can only import modules entered into Core Maude. Note that Full Maude is implemented using reflection, and that in the end all modules are handled by Core Maude, which is not aware of Full Maude’s database.

Notice also that loading a Core Maude module once Full Maude is running will break the read-eval-print loop (see Section 13.1). Therefore, one should enter such modules before starting Full Maude. Assuming there is a file path.maude containing the Core Maude module PATH, we will have the following behavior if we enter it into Full Maude.

  Maude> load path.maude  
 
  Maude> (red in PATH : b ; (c ; d) .)  
  Warning: no loop state.  
  Advisory: attempting to reinitialize loop.  
  Warning: "full-maude.maude", line 13692: bad token init  
  Warning: "full-maude.maude", line 13692: no parse for term.  
  Advisory: unable to reinitialize loop.

As said above, when the loop gets broken, as in this case, we must select the FULL-MAUDE module and restart the loop. We may now do the following:

  Maude> select FULL-MAUDE .  
  Maude> loop init .  
 
              Full Maude 2.7.1 Jun 30th 2016  
 
  Maude> (red in PATH : b ; (c ; d) .)  
  reduce in PATH :  
    b ;(c ; d)  
  result Path :  
    b ;(c ; d)

Notice that with a loop init command Full Maude is restarted with an empty database. That is, any Full Maude module entered before the reinitialization will have to be reentered again. In this case, PATH is a Core Maude module, which is being executed in Full Maude. Since it is not in Full Maude’s database, Full Maude looks into Core Maude’s database and then executes the command in it. This functionality is useful for using any of the predefined modules, but also other modules which are not part of Maude’s prelude. For example, for using inside Full Maude the model checker, which although predefined is not part of the prelude.maude file, we just need to load the model-checker.maude file before starting the loop. For example, we can do the following:

  ~/maude-linux/bin$ ./maude.linux model-checker.maude full-maude.maude  
                     \||||||||||||||||||/  
                   --- Welcome to Maude ---  
                     /||||||||||||||||||\  
                Maude 2.7.1 built: Jun 27 2016 16:43:23  
            Copyright 1997-2016 SRI International  
               Tue Jun 28 09:25:34 2016  
 
              Full Maude 2.7.1 Jun 30th 2016  
 
  Maude> (mod CHECK-RESP is  
            protecting MODEL-CHECKER .  
            ...  
          endm)  
 
  Maude> (red p(0) |= (<> Qstate) .)

See Section 17.7 for a concrete example of the use of Maude’s model checker with Full Maude modules.

15.3 Additional module operations in Full Maude

As for Core Maude, in Full Maude we can use the keywords protecting, extending, and including (or pr, ex, and inc in abbreviated form) to define structured specifications, as well as summation, renaming, and instantiation operations on parameterized modules (see Chapter 6). All the predefined modules introduced in Chapter 7, plus the module META-LEVEL and its submodules, described in Chapter 11, are also available in Full Maude.2

In addition to the module operations available in Core Maude, Full Maude supports the following extensions:

As in Core Maude, a module or theory importing some combination of modules or theories, given by module expressions, can be seen as a structured module with more or less complex relationships among its component submodules. For execution purposes, however, we typically want to convert this structured module into an equivalent unstructured module, that is, into a “flattened” module without submodules; this flattened module will then be compiled into the Maude rewrite engine. By systematically using the metaprogramming capabilities of Maude, we can both evaluate module expressions into structured module hierarchies and flatten such hierarchies into unstructured modules for execution. All such module operations are defined by equations that operate on the metalevel term representations of modules. This is essentially the idea behind the implementation of Full Maude in Maude.

In Full Maude, the use of module expressions is somewhat more general than in Core Maude. A Full Maude module expression can be used in any place where a module name is expected. Thus, as in Core Maude, in Full Maude, module expressions can be used as:

Furthermore, in Full Maude, they can also be used, e.g., to express the module in which a red or rew command will be executed,

  Maude> (red in BOOL * (op true to T, op false to F) : T or F .)  
  result Bool :  
    T

or as argument of any other command requiring a module name,

  Maude> (show ops LIST{Nat} .)  
    op $reverse : List{Nat}List{Nat}-> List{Nat}.  
    op $size : List{Nat}Nat -> Nat .  
    op append : List{Nat}List{Nat}-> List{Nat}.  
    op append : List{Nat}NeList{Nat}-> NeList{Nat}.  
    op append : NeList{Nat}List{Nat}-> NeList{Nat}.  
    ...

Of course, this works with any module, and not only with predefined modules. For example, let us do the same with the instantiation of the SET-MAX module presented in Section 6.3.4 (which we assume is in file set-max.maude) with the view IntAsToset described in Section 6.3.2. Although we can use Core Maude modules in Full Maude, we do not have access to user-defined Core Maude views from Full Maude. Any such view must be entered into Full Maude before it is used in a module instantiation. Note that although Core Maude modules are implicitly entered into Full Maude’s database, they are recompiled, and therefore, any view required for recompiling the corresponding module must also be entered. The evaluation of the module expression SET-MAX{IntAsToset} requires views TOSET and IntAsToset.

  Maude> load set-max.maude  
  Maude> select FULL-MAUDE .  
  Maude> loop init .  
 
              Full Maude 2.7.1 Jun 30th 2016  
 
  Maude> (view TOSET from TRIV to TOSET is  
            sort Elt to Elt .  
          endv)  
  Introduced view TOSET  
 
  Maude> (view IntAsToset from TOSET to INT is  
            sort Elt to Int .  
          endv)  
  Introduced view IntAsToset  
 
  Maude> (red in SET-MAX{IntAsToset} : max((5, 4, 8, 4, 6, 5)) .)  
  result NzNat :  
    8

Similarly, after entering the Full Maude version of the RingToRat view, we can reduce the same expression we reduced in Section 6.3.4 as follows:

  Maude> (red in RAT-POLY{Qid} :  
            (((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)

As we will see below, a module expression can also be used as the parameter of a view, provided the top level is a theory.

15.3.1 The tuple and power module expressions

The evaluation of an n-tuple module expression consists in the generation of a parameterized functional module with the number of TRIV parameters specified by the argument n. A sort for tuples of such size, and the corresponding constructor (_,…,_) and selector operators p1_, …, pn_, are also defined. For example, the module expression TUPLE[2] automatically generates as result the following module (notice the backquotes in the declaration of the tuple constructor).

 (fmod TUPLE[2]{C1 :: TRIV, C2 :: TRIV} is  
    sorts Tuple{C1, C2} .  
    op ‘(_‘,_‘) : C1$Elt C2$Elt -> Tuple{C1, C2} [ctor].  
    op p1_ : Tuple{C1, C2} -> C1$Elt .  
    op p2_ : Tuple{C1, C2} -> C2$Elt .  
    var E1 : C1$Elt .  
    var E2 : C2$Elt .  
    eq p1(E1, E2) = E1 .  
    eq p2(E1, E2) = E2 .  
  endfm)

In the Clear [18] and OBJ [73] family of languages, module operations take theories, modules, and views, and return new theories and modules (see Chapter 6); on the other hand, the TUPLE[_] operation takes a nonzero natural number n and returns a parameterized TUPLE[n] module; this is impossible to achieve with the Clear/OBJ repertoire of module operations. Even though an n-tuple module expression is in principle of a completely different nature from the usual Clear/OBJ module operations, the way Full Maude handles it is the same as the way it handles any other module expression. Its evaluation produces a new unit, a parameterized functional module in this case, with the module expression as its name.

Suppose that we want to specify a library in which we have the information on the books in a record structure with the title, author, year of publication, publisher, and number of copies available. We may use a specification beginning as follows:

 (fmod LIBRARY is  
    pr TUPLE[5]{String, String, Nat, String, Nat}  
         * (op p1_ to title,  
            op p2_ to author,  
            op p3_ to year,  
            op p4_ to publisher,  
            op p5_ to copies) .  
    ---- ...  
  endfm)

The particular case of a tuple in which all component sorts are equal is provided by the n-power module expression. For example, the module expression POWER[5] automatically generates as result the following module:

 (fmod POWER[5]{X :: TRIV} is  
    protecting TUPLE[5]{X, X, X, X, X}  
      * (sort Tuple{X, X, X, X, X} to Power{X}) .  
  endfm)

We can use the power module expression in any place where a module name is expected, like in a reduction

  Maude> (red in POWER[10]{Nat} : p5 (0, 1, 2, 3, 4, 5, 6, 7, 8, 9) .)  
  result NzNat :  
    4

or in an importation to build other modules:

 (fmod PERSON-RECORD is  
    pr POWER[3]{String}  
         * (sort Tuple{String, String, String} to PersonRecord,  
            op p1_ to firstname,  
            op p2_ to lastname,  
            op p3_ to address) .  
    op fullName : PersonRecord -> String .  
    vars F L A : String .  
    eq fullName((F, L, A)) = F + " " + L .  
  endfm)

  Maude> (red fullName(("John", "Smith", "Maude Ave")) .)  
  result String :  
    "John Smith"

15.3.2 Parameterized views

Suppose we have defined modules LIST{X :: TRIV} and SET{X :: TRIV}, specifying, respectively, lists and sets, and suppose that we need, e.g., the data type of lists of sets of natural numbers. Typically, we would first instantiate the module SET with a view, say Nat, from TRIV to the module NAT mapping the sort Elt to the sort Nat, thus getting the module SET{Nat} of sets of natural numbers. Then, we would instantiate the module specifying lists with a view, say NatSet, from TRIV to SET{Nat}, obtaining the module LIST{NatSet}. But, what if we need now the data type of lists of sets of Booleans? Should we repeat the whole process again? One possibility is to define a combined module SET-LIST{X :: TRIV}. But what if we later want stacks of sets instead of lists of sets?

We can greatly improve the reusability of specifications by using parameterized views. Let us consider the following parameterized view Set from TRIV to SET, which maps the sort Elt to the sort Set{X}.

 (view Set{X :: TRIV} from TRIV to SET{X} is  
    sort Elt to Set{X} .  
  endv)

With this kind of views we can keep the parameter part of the target module still as a parameter. We can now have lists of sets, stacks of sets, and so on, for any instance of TRIV, by instantiating the appropriate parameterized module with the appropriate view. For example, given the view Nat above, we can have the module LIST{Set{Nat}} of lists of sets of natural numbers, or lists of sets of Booleans with LIST{Set{Bool}}, given a view Bool from TRIV to the predefined module BOOL. Similarly, we can have STACK{Set{Nat}} or STACK{Set{Bool}}.

We can also link the parameter of a module like LIST{Set{X}} to the parameter of the module in which it is being included. That is, we can, for example, declare a module of the form

 (fmod GENERIC-SET-LIST{X :: TRIV} is  
    protecting LIST{Set{X}} .  
  endfm)

Then, instantiating the parameterized module GENERIC-SET-LIST with a view V from TRIV to another module or theory results in a module with name GENERIC-SET-LIST{V}, which includes the module LIST{Set{V}}. Note that even with parameterized views we still follow conventions for module interfaces and for sort names (see Section 6.3). The only difference is that now, instead of having simple view names, we must consider names of views which are parameterized.

The use of parameterized views in the instantiation of parameterized modules allows very reusable specifications. For example, a very simple way of specifying (finite) partial functions is to see a partial function as a set of input-result pairs. Of course, for such a set to represent a function there cannot be two pairs associating different results with the same input value. We show later in this section (in the module PFUN below) how this property can be specified by means of appropriate membership axioms. Note, however, that since membership axioms cannot be given on associative operators over sorts (see Section 14.2.8), we cannot use either the specification of sets described in Section 6.3.3 or the predefined module in Section 7.12.2. Let us consider instead the following module:3

  (fmod SET-KIND{X :: TRIV} is  
    sorts NeKSet{X} KSet{X} .  
    subsort X$Elt < NeKSet{X} < KSet{X} .  
    op empty : -> KSet{X} [ctor] .  
    op _‘,_ : KSet{X} KSet{X} ~> KSet{X} [ctor assoc comm id: empty] .  
    mb NS:NeKSet‘{X‘}, NS’:NeKSet‘{X‘} : NeKSet{X} .  
 
    var E : X$Elt .  
 
    *** idempotency  
    eq E, E = E .  
   endfm)

Here the operator _,_ is declared at the kind level (notice the different form of the arrow in its declaration) together with a membership axiom, that is logically equivalent to the declaration

  op _‘,_ : NeKSet{X} NeKSet{X} -> NeKSet{X} .

at the sort level.

We can then specify sets of pairs by instantiating this SET-KIND module with a parameterized view from TRIV to the parameterized module TUPLE[2]{X, Y} defining pairs of elements. The appropriate parameterized view can be defined as follows:

 (view Tuple{X :: TRIV, Y :: TRIV} from TRIV to TUPLE[2]{X, Y} is  
    sort Elt to Tuple{X, Y} .  
  endv)

A partial function can be lifted to a total function by adding a special value to its codomain, to be used as the result for the input elements for which the function is not defined. For this we make good use of the parameterized module MAYBE, introduced in Section 6.3.3, which adds a supersort and a new element maybe to this supersort; in this application, the constant maybe is renamed to undefined.

We are now ready to give the specification of partial functions. The sets representing the domain and codomain of the function are given by TRIV parameters, and then the set of tuples is provided by the imported module expression SET-KIND{Tuple{X, Y}} with sorts KSet{Tuple{X, Y}} and NeKSet{Tuple{X, Y}}. We define operations dom and im returning, respectively, the domain and image of a set of pairs. The dom operation will be used for checking whether there is already a pair in a set of pairs with a given input value. With these declarations we can define the sort PFun{X, Y} as a subsort of KSet{Tuple{X, Y}}, by adding the appropriate membership axioms specifying those sets that satisfy the required property. Finally, we define operators _[_] and _[_->_] to evaluate a function at a particular element, and to add or redefine an input-result pair, respectively. We use the Core Maude predefined module SET (see Section 7.12.2) for representing the sets of elements in the domain and image of a partial function.

 (fmod PFUN{X :: TRIV, Y :: TRIV} is  
    pr SET-KIND{Tuple{X, Y}} .  
    pr SET{X} + SET{Y} .  
    pr MAYBE{Y} * (op maybe to undefined) .  
 
    sort PFun{X, Y} .  
    subsorts Tuple{X, Y} < PFun{X, Y} < KSet{Tuple{X, Y}} .  
 
    vars A D : X$Elt .  
    vars B C : Y$Elt .  
    var  F : PFun{X, Y} .  
    var  S : KSet{Tuple{X, Y}} .  
 
    op dom : KSet{Tuple{X, Y}} -> Set{X} .         *** domain  
    eq dom(empty) = empty .  
    eq dom((A, B), S) = A, dom(S) .  
    op im : KSet{Tuple{X, Y}} -> Set{Y} .          *** image  
    eq im(empty) = empty .  
    eq im((A, B), S) = B, im(S) .  
 
    op empty : -> PFun{X, Y} [ctor] .  
    cmb (A, B), (D, C), F : PFun{X, Y}  
      if (D, C), F : PFun{X, Y} /\ not(A in dom((D, C), F)) .  
 
    op _‘[_‘] : PFun{X, Y} X$Elt -> Maybe{Y} .  
    op _‘[_->_‘] : PFun{X, Y} X$Elt Y$Elt -> PFun{X, Y} .  
    ceq ((A, B), F)[ A ] = B if ((A, B), F) : PFun{X, Y} .  
    eq F [ A ] = undefined [owise] .  
    ceq ((A, B), F)[ A -> C ] = (A, C), F  
      if ((A, B), F) : PFun{X, Y} .  
    eq F [ A -> C ] = (A, C), F [owise] .  
  endfm)

Now, we can instantiate the PFUN module with, for example, the view Nat, in order to get the finite partial functions from natural numbers to natural numbers by means of the module expression PFUN{Nat, Nat}.

15.4 Moving up and down between reflection levels

The functions provided by Core Maude for moving up and down reflection levels (see Section 11.5.1) are not very useful in Full Maude. Although they are available as part of the module META-LEVEL, they take as one of their arguments the name of a module entered into Core Maude. Since the databases of modules are different, these functions work in Full Maude only for Core Maude predefined modules. Full Maude provides its own functions upTerm and upModule for moving, respectively, terms and modules up reflection levels, and an additional down command which allows moving terms down reflection levels.

Let us consider the following module for the examples in the coming sections.

 (fmod NAT-PLUS is  
    sort Nat .  
    op 0 : -> Nat .  
    op s_ : Nat -> Nat .  
    op _+_ : Nat Nat -> Nat [assoc comm id: 0] .  
    vars N M : Nat .  
    eq s N + s M = s s (N + M) .  
  endfm)

In what follows we will use the notation t and M to refer to the metarepresentations of a term t and a module M, respectively. For example, we will write the metarepresentation of 0 + s 0 as 0 + s 0 instead of

  ’_+_[’0.Nat, ’s_[’0.Nat]]

15.4.1 Up

As in Core Maude, in Full Maude we can use the upModule and upTerm functions to avoid the cumbersome task of explicitly writing, respectively, the metarepresentation of a module or the metarepresentation of a term in a given module. The Full Maude upModule function takes as a single argument the name of a module and returns its metarepresentation;4 upTerm takes two arguments, the name of a module and a term in such a module, and returns the corresponding metarepresentation of the term.

Therefore, by evaluating in any module importing the module META-LEVEL the upModule function with the name of any module in the system—either in Core Maude or in Full Maude—as argument, we obtain the metarepresentation of such a module. For example, assuming that the previous module NAT-PLUS has been entered into Full Maude, and therefore it is in its database, we can get its metarepresentation, which we denoted by NAT-PLUS, as follows:

  Maude> (red in META-LEVEL : upModule(NAT-PLUS) .)  
  result FModule :  
    fmod ’NAT-PLUS is  
    nil  
    sorts ’Bool ; ’Nat .  
    none  
    op ’0 : nil -> ’Nat [none] .  
    op ’_+_ : ’Nat ’Nat -> ’Nat [assoc comm id(’0.Nat)] .  
    ...

We can use the metarepresentation obtained in this way in any place where a term of sort Module is expected. For example, we can apply the function getOps in META-LEVEL (see Section 11.3) to upModule(NAT-PLUS) as follows:

  Maude> (red in META-LEVEL : getOps(upModule(NAT-PLUS)) .)  
  result OpDeclSet :  
    op ’0 : nil -> ’Nat [none] .  
    op ’_+_ : ’Nat ’Nat -> ’Nat [assoc comm id(’0.Nat)] .  
    op ’_=/=_ : ’Universal ’Universal -> ’Bool  
         [poly(1 2)  
          prec(51)  
          special(  
            id-hook(’EqualitySymbol,nil)  
            term-hook(’equalTerm,’false.Bool)  
            term-hook(’notEqualTerm,’true.Bool))] .  
    ...

Similarly, we can use it with descent functions as discussed in Section 11.5.

  Maude> (red in META-LEVEL :  
            metaReduce(upModule(NAT-PLUS), ’_+_[’0.Nat, ’s_[’0.Nat]]) .)  
  result ResultPair :  
    {’s_[’0.Nat],’Nat}

But, instead of explicitly writing the metarepresentation 0 + s 0 in the above reduction we can also make good use of the upTerm function, that allows us to get the metarepresentation of a term in a given module.

  Maude> (red in META-LEVEL :  
            metaReduce(upModule(NAT-PLUS), upTerm(NAT-PLUS, 0 + s 0)) .)  
  result ResultPair :  
    {’s_[’0.Nat], ’Nat}

As another example, to obtain the metarepresentation of the term s 0 in the module NAT-PLUS above, which we denoted by s 0, we can write

  Maude> (red in META-LEVEL : upTerm(NAT-PLUS, s 0) .)  
  result GroundTerm :  
    ’s_[’0.Nat]

The module name is the first argument of the upTerm function, with the term of that module to be metarepresented as the second argument. Since the same term can be parsed in different ways in different modules, and therefore can have different metarepresentations depending on the module in which it is considered, the module to which the term belongs has to be used to obtain the correct metarepresentation. Note also that the above reduction only makes sense at the metalevel, that is, either in the META-LEVEL module itself or in a module importing it.

15.4.2 Down

The result of a metalevel computation, that may use several levels of reflection, can be a term or a module metarepresented one or more times, which may be hard to read. Therefore, to display the output in a more readable form we can use the down command, which is in a sense inverse to upTerm, since it gives us back the original term from its metarepresentation. Notice that down is not a function, but a command instead, because it is more general, taking other commands as arguments, as we are going to explain.

The down command takes two arguments. The first argument is the name of the module to which the term to be returned belongs. The metarepresentation of the desired output term should be the result of the command given as second argument. The syntax of the down command is as follows:

  down ModuleExpression : Command

Thus, we can give the following command.

  Maude> (down NAT-PLUS :  
            red in META-LEVEL :  
              getTerm(  
                metaReduce(upModule(NAT-PLUS),  
                           upTerm(NAT-PLUS, 0 + s 0))) .)  
  result Nat :  
    s 0

Notice that this is equivalent to what we may write using the overline notation as:

  Maude> red getTerm(metaReduce(NAT-PLUS, 0 + s 0)) .
  result Term: s 0

The use of upTerm and down can be iterated with as many levels of reflection as we wish. For example, we can give the command

  Maude> (red in META-LEVEL :  
              getTerm(  
                metaReduce(upModule(META-LEVEL),  
                  upTerm(META-LEVEL,  
                    getTerm(  
                      metaReduce(upModule(NAT-PLUS),  
                                 upTerm(NAT-PLUS, 0 + s 0)))))) .)  
  result GroundTerm :  
    ’_‘[_‘][’’s_.Sort, ’’0.Nat.Constant]

This is equivalent to what we would have written using the overline notation as

  Maude> red getTerm(metaReduce(META-LEVEL,
                       metaReduce(NAT-PLUS, 0 + s 0))) .
  result Term: s 0

We can write expressions involving simultaneously down, upModule, and upTerm:

  Maude> (down NAT-PLUS :  
            down META-LEVEL :  
              red in META-LEVEL :  
                  getTerm(  
                    metaReduce(upModule(META-LEVEL),  
                      upTerm(META-LEVEL,  
                        getTerm(  
                          metaReduce(upModule(NAT-PLUS),  
                                     upTerm(NAT-PLUS, 0 + s 0)))))) .)  
  result Nat :  
    s 0

The metalevel function downTerm can also be used, but it is a Core Maude function, and therefore can only be used on Core Maude modules.

  Maude> (down NAT-PLUS :  
            red in META-LEVEL :  
              downTerm(  
                getTerm(  
                  metaReduce(upModule(META-LEVEL),  
                    upTerm(META-LEVEL,  
                      getTerm(  
                        metaReduce(upModule(NAT-PLUS),  
                                   upTerm(NAT-PLUS, 0 + s 0)))))),  
                ’T:Term) .)  
  result Nat :  
    s 0

15.5 Ax-coherence completion

As pointed out in Section 12.9.1, the equations used for variant generation in an admissible equational theory must be confluent, terminating, sort-decreasing, and explicitly Ax-coherent. The confluence, termination, and sort-decreasingness of equational Maude specifications are the typical executability requirements for equational specifications, and can be checked using Maude’s Church-Rosser Checker (CRC) [5052] and Termination Checker (MTT) [43].

Regarding the Ax-coherence requirement, the situation is different for different purposes. Ax-coherence is not currently required for rewrite theories written in Maude because specifications are implicitly completed for Ax-coherence within Maude (see Section 4.8). It is not required either for tools like the CRC or the Coherence Checker (ChC), or for narrowing (see Chapter 16) which also automatically complete the specifications provided. However, rewrite theories are assumed to be explicitly Ax-coherent for variant generation and variant-based unification (Section 12.10), the reason being that there is a different treatment of extension variables in rewriting and narrowing (see [120] for more details). Indeed, we require coherence rather than ground coherence, since the latter is weaker and sufficient for rewriting but insufficient for narrowing or critical pair analysis.

For theories Ax that are combinations of associativity, commutativity, and identity axioms, we can make any specification explicitly Ax-coherent by using a procedure which adds Ax-extensions and always terminates (see [105], and Section 4.8 for a more informal explanation). The procedure followed to automatically complete for Ax-coherence for rewriting and for narrowing, or in the CRC or ChC tools is carried on differently. Whilst for rewriting the completion is performed by (Core) Maude, in the other cases the completion is performed by Maude code provided by Full Maude.

Full Maude provides the following axCohComplete operation in its module AX-COHERENCECOMPLETION.

  op axCohComplete : Module -> Module .

This operation takes (the metarepresentation of) a module which defines an order-sorted specification (i.e., no memberships are allowed) and returns (the metarepresentation of) another module whose equations and rules are modified to complete them modulo associativity and commutativity (AC), associativity, commutativity, and identity (ACU), associativity and identity (AU), associativity and left identity (AUl), associativity and right identity (AUr), and associativity (A).

More specifically, for each operator f : S S S and equation/rule f(t1,,tn) r if  C in the module,

if f is AC add f(t1,,tn,x:[S]) f(r,x:[S]) if  C
if f is ACUreplace by f(t1,,tn,x:[S]) f(r,x:[S]) if  C
if f is AU replace by f(x:[S],t1,,tn,y:[S]) f(x:[S],r,y:[S]) if  C
if f is AUl replace by f(x:[S],t1,,tn,y:[S]) f(x:[S],r,y:[S]) if  C
add f(x:[S],t1,,tn) f(x:[S],r) if  C
if f is AUr replace by f(x:[S],t1,,tn,y:[S]) f(x:[S],r,y:[S]) if  C
add f(t1,,tn,y:[S]) f(r,y:[S]) if  C
if f is A add f(x:[S],t1,,tn,y:[S]]) f(x:[S],r,y:[S]) if  C
add f(x:[S],t1,,tn) f(x:[S],r) if  C
add f(t1,,tn,y:[S]) f(r,y:[S]) if  C
  

To deal with collapses, those rules/equations of the form l r if  C that do not match any of the above cases, and such that there is an operator f : S S S with identity and with S and leastSort(l) in the same kind, are completed following the above cases as if it were the equation/rule f(l) r if  C.

Ax-completion is available in Full Maude through the following command:

  (ax coherence completion [ ModuleExpression ] .)

where ModuleExpression is any module expression. As usual, if no module expression is given the default current module is completed.

For example, let us consider the following non-coherent version of the equational theory for exclusive or (see Section 12.9).

  mod EXCLUSIVE-OR-NOT-COHERENT is  
    sorts Nat NatSet .  
    op 0 : -> Nat [ctor] .  
    op s : Nat -> Nat [ctor] .  
 
    subsort Nat < NatSet .  
    op mt : -> NatSet .  
    op _*_ : NatSet NatSet -> NatSet [ctor assoc comm] .  
 
    vars X Y Z : [NatSet] .  
    eq [idem] : X * X = mt [variant] .  
    eq [id] : X * mt = X [variant] .  
  endm

The module EXCLUSIVE-OR-NOT-COHERENT is not AC-coherent. The command

  Maude> (ax coherence completion EXCLUSIVE-OR-NOT-COHERENT .)

shows the completed version of the EXCLUSIVE-OR-NOT-COHERENT module. Specifically, the following equation is added:

  eq [idem] : X:[NatSet] * X:[NatSet] * X@@@:[NatSet]  
    = mt * X@@@:[NatSet] [variant] .

Notice the new variable X@@@:[NatSet]. The resulting module is equivalent to the module EXCLUSIVE-OR in Section 12.9.

As another example, the Ax-completion of the VENDING-MACHINE module in Section 5.1 results in a module with the same definitions but with the change rule replaced by the rule

  rl [change] : q q q q X@@@:[Marking] => $ X@@@:[Marking] .

In general, of course, a module can have operators with any combination of associativity, commutativity, and identity, with associated equations and rules. In that case the ax coherence completion command will add or replace the corresponding completion equations and rules.

The narrowing command (see Section 16.3) and the CRC and ChC tools use the metalevel operation axCohComplete to complete the modules before using them. As any other function in Full Maude, it is available for its direct use in other tools or commands. We can illustrate the use of this metalevel function with the coherence completion of the EXCLUSIVE-OR-NOT-COHERENT module:

  Maude> reduce in FULL-MAUDE :  
           axCohComplete(upModule(’EXCLUSIVE-OR-NOT-COHERENT, false)) .  
 
  result SModule :  
    mod ’EXCLUSIVE-OR-NOT-COHERENT is  
    including ’BOOL .  
    sorts ’Nat ; ’NatSet .  
    subsort ’Nat < ’NatSet .  
    op ’0 : nil -> ’Nat [ctor] .  
    op ’mt : nil -> ’NatSet [ctor] .  
    op ’_*_ : ’NatSet ’NatSet -> ’NatSet [assoc comm ctor] .  
    op ’s : ’Nat -> ’Nat [ctor] .  
    none  
    eq ’_*_[’X:‘[NatSet‘],’mt.NatSet]  
      = ’X:‘[NatSet‘] [label(’id) variant] .  
    eq ’_*_[’X:‘[NatSet‘],’X:‘[NatSet‘]]  
      = ’mt.NatSet [label(’idem) variant] .  
    eq ’_*_[’X:‘[NatSet‘],’X:‘[NatSet‘],’X@@@:‘[NatSet‘]]  
      = ’_*_[’mt.NatSet,’X@@@:‘[NatSet‘]] [label(’idem) variant] .  
    none  
  endm

The following example shows the completion of rules that require changing the top operator of the left-hand side term.

  mod NARROWING-VM-NOTOP is  
    sorts Coin Item Marking Money State .  
    subsort Coin < Money .  
    op empty : -> Money .  
    op __ : Money Money -> Money [assoc comm id: empty] .  
    subsort Money Item < Marking .  
    op __ : Marking Marking -> Marking [assoc comm id: empty] .  
    subsort Marking < State .  
    ops $ q : -> Coin . ops a c : -> Item .  
    var M : Marking .  
    rl [buy-c] : $ => c .  
    rl [buy-a] : $ => a q .  
    eq [change]: q q q q = $ [variant] .  
  endm  
 
  Maude> reduce in FULL-MAUDE :  
           axCohComplete(upModule(’NARROWING-VM-NOTOP, false)) .  
 
  result SModule:  
    mod ’NARROWING-VM-NOTOP is  
      including ’BOOL .  
      sorts ’Coin ; ’Item ; ’Marking ; ’Money ; ’State .  
      subsort ’Coin < ’Money .  
      subsort ’Item < ’Marking .  
      subsort ’Marking < ’State .  
      subsort ’Money < ’Marking .  
      op ’$ : nil -> ’Coin [none] .  
      op ’__ : ’Marking ’Marking -> ’Marking [assoc comm id(’empty.Money)] .  
      op ’__ : ’Money ’Money -> ’Money [assoc comm id(’empty.Money)] .  
      op ’a : nil -> ’Item [none] .  
      op ’c : nil -> ’Item [none] .  
      op ’empty : nil -> ’Money [none] .  
      op ’q : nil -> ’Coin [none] .  
      none  
      eq ’__[’q.Coin,’q.Coin,’q.Coin,’q.Coin,’X@@@:‘[State‘]]  
        = ’__[’$.Coin,’X@@@:‘[State‘]]  
        [variant label(’change)] .  
      rl ’__[’$.Coin,’X@@@:‘[State‘]]  
        => ’__[’c.Item,’X@@@:‘[State‘]]  
        [label(’buy-c)] .  
      rl ’__[’$.Coin,’X@@@:‘[State‘]]  
        => ’__[’a.Item,’q.Coin,’X@@@:‘[State‘]]  
        [label(’buy-a)] .  
    endm

15.6 Differences between Full Maude and Core Maude

Apart from those features available in Full Maude that are not supported in Core Maude (discussed above in Sections 15.3-15.5 and later in Chapters 16 and 17), we find a number of differences between Full Maude and Core Maude. There are some obvious ones, like the fact that any input enclosed in parentheses is handled by Full Maude. Thus, Full Maude modules, theories, views, and commands can refer to modules, theories, and views in both Core Maude and Full Maude’s databases. There are also differences in pretty-printing, tracing, debugging, etc. Moreover, there are also other differences that impose certain limitations on the specifications themselves:

1.
Operator and message names have to be given in their equivalent single-identifier form when they are declared (see below), but they can later be written in the usual way in statements and in terms for evaluation.
2.
Sort names used in term qualifications, membership assertions, and on-the-fly declarations of variables have to be in their equivalent single-identifier form.
3.
The continue, show component, show path, and show search graph commands are not supported in Full Maude.
4.
Full Maude does not support external objects.

In the rest of the section we explain the first two restrictions in some detail and give some hints on how to avoid them.

An operator name has to be given as a single identifier; multi-identifier operators have to be declared in their single-identifier form, that is, each identifier in a multi-identifier name has to be preceded by a backquote. For example, to define an operator with name _less than or equal_, we have to declare it in its single identifier form _less‘than‘or‘equal_. Except for having to use the single-identifier form in the operator name, the declaration of operators is exactly as in Core Maude. For example, the declaration of this operator on sort, say, Int is as follows.

    op _less‘than‘or‘equal_ : Int Int -> Bool .

Remember that not only blank spaces, but also the special characters ‘{’, ‘}’, ‘(’, ‘)’, ‘[’, ‘]’ and ‘,’ break the identifiers. Therefore, to declare in Full Maude an operator such as {_} taking an element of sort, say, Int and with value sort Set, we should add appropriate backquotes, as follows:

    op ‘{_‘} : Int -> Set .

As in Core Maude, several operators with the same arity and coarity can be defined in the same declaration using the keyword ops, but, again, each operator name has to be given in its single-identifier form. We could have for example the following declaration.

    ops _‘{_‘} _‘,_ : Foo Bar -> Baz .

Since each operator name is a single identifier, parentheses are not needed to indicate the boundaries between the syntactic forms of the different operators.

As for operator names, message names can be mixfix, but they have to be declared in single-identifier form. Thus, to define a message credit in an object-oriented module (see Chapter 17) with syntax, say, (_)credit_ the declaration has to be given as follows.

    msg ‘(_‘)credit_ : Oid Nat -> Msg .

And the same applies to declarations of multiple message names:

    msgs ‘(_‘)credit_ ‘(_‘)debit_ : Oid Nat -> Msg .

The second problem mentioned at the beginning of this section affects the qualification of terms by sort names, on-the-fly declarations of variables, and membership assertions. In these three situations, the user must use the names of parameterized sorts, not as he or she has defined them, but in their equivalent single-identifier form. Thus, if we have, for example, a sort List{Nat} and a constant nil in it, if necessary, it should be qualified as (nil).List‘{Nat‘}. A variable L of sort List{Nat} being declared on the fly should be written L:List‘{Nat‘}. Similarly, to check whether a term T has sort List{Nat} we have to write T : List‘{Nat‘} or T :: List‘{Nat‘}, depending on the kind of sort check we wish to perform.