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 controled 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 .
  endfth

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] .
  endfth

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.^6.1On 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] .
  endfth

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] .
  endfth

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.^6.2For 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] .
  endfth

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] .
  endfth

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] .
  endfth

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] .
  endfth

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:

• from $a < b$, one can define $a \leq b$ as equivalent to $a < b$ or $a = b$; and
• from $a \leq b$, one can define $a < b$ as equivalent to $a \leq b$ and $a \neq b$.

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] .
  endfth

  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] .
  endfth

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] .
  endfth

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

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

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 .
  endth