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, Full Maude supports three different types of theories: functional theories, system theories, and object-oriented theories. Their structure is the same as that of their module counterparts. All of them can have sorts, subsort relationships, operators, variables, membership assertions and equations, and can import other theories or modules. System theories can have rules as well, and object-oriented theories can have classes, subclass relationships and messages.
Theories are rewriting logic theories with a loose interpretation. Theories are then allowed to contain rules and equations with variables in their righthand sides or conditions that may not appear in their corresponding lefthand sides. Similarly, conditional membership axioms may have variables in their conditions that do not appear in their membership assertions. Also, the lefthand side may be a single variable. In the current version, theories are not executed and cannot be parameterized.
Functional theories are declared with the keywords fth ... endfth, system theories with the keywords th ... endth, and object-oriented theories with the keywords oth ... endoth. The syntax for the declaration of theories is as follows.
op fth_is_endfth : ModuleName FDeclList -> PreModule . op th_is_endth : ModuleName SDeclList -> PreModule . op oth_is_endoth : ModuleName ODeclList -> PreModule .
Let us begin by introducing the functional theory TRIV, which requires just a sort.
(fth TRIV is
sort Elt .
endfth)
The theory of partially ordered sets with an anti-reflexive and transitive binary operator can be expressed in the following way.
(fth POSET is
protecting BOOL .
sort Elt .
op _<_ : Elt Elt -> Bool .
vars X Y Z : Elt .
eq X < X = false .
ceq X < Z = true if X < Y and Y < Z .
endfth)
The theory of totally ordered sets, that is, posets in which all pairs of distinct elements have to be related, can be given as follows.
(fth TOSET is
including POSET .
vars X Y : Elt .
eq X < Y or Y < X or X == Y = true .
endfth)
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 semantics35, then that initial semantics is maintained by the importation. For example, in the definition of the POSET theory, the declaration protecting BOOL ensures that the initial semantics of the functional module for the Booleans is preserved, which is in fact a crucial requirement36. This requirement is then preserved by TOSET when POSET is included. In fact, we are dealing with a structure in which part of it, not only the top theory, has a loose semantics, while other parts contain modules with an initial semantics. The kind of semantics of a module or theory is determined by the keyword used in its definition and the importation mode.
As an example of a system theory, let us consider the theory CHOICE of multisets of elements with a choice operator defined on the multisets by a rewrite rule that nondeterministically picks up one of the elements in the multiset. We can express this theory as indicated below, where we have a sort MSet declared as a supersort of the sort Elt.
(th CHOICE is
sort MSet Elt .
subsort Elt < MSet .
op __ : Elt Elt -> Elt [assoc comm] .
var E : Elt .
var L : MSet .
rl [choice] : E L => E .
endth)
Our last example is an object-oriented theory, namely, the theory of classes with at least one attribute of any sort. It is defined as follows.
(oth CELL is
sort Elt .
class Cell | contents : Elt .
endoth)
This last theory could have been more naturally expressed as a parameterized theory. We could have defined CELL with a parameter TRIV to capture the idea of defining cells in a generic way. However, the present Full Maude implementation does not support parameterized theories. We plan to extend the language to support not only parameterized theories, but also parameterized views.