Maude's functional modules are theories in membership equational logic [41, 4], a Horn logic whose atomic sentences are equalities t=t' and membership assertions of the form t:s, stating that a term t has sort s. Such a logic extends order-sorted equational logic [26], and supports sorts, subsort relations, subsort polymorphic overloading of operators, and definition of partial functions with equationally defined domains. Maude's functional modules are assumed to be Church-Rosser; they are executed by the Maude engine according to the rewriting techniques and operational semantics developed in [4].
Membership equational logic is a sublogic of rewriting logic [37]. A rewrite theory is a pair (T,R) with T a membership equational theory, and R a collection of labeled and possibly conditional rewrite rules involving terms in the signature of T. Maude's system modules are rewrite theories in exactly this sense. The rewrite rules r: t --> t' in R are not equations. Computationally, they are interpreted as local transition rules in a possibly concurrent system. Logically, they are interpreted as inference rules in a logical system. As already mentioned, this makes rewriting logic both a general semantic framework to specify concurrent systems and languages [40], and a general logical framework to represent and execute different logics [33].
Rewriting in (T,R) happens modulo the equational axioms in T. Maude supports rewriting modulo most of the different combinations of associativity, commutativity, identity, and idempotency axioms. The rules in R need not be Church-Rosser and need not be terminating. Many different rewriting paths are then possible; therefore, the choice of appropriate strategies is crucial for executing rewrite theories.
In Maude, such strategies are not an extra-logical part of the language. They are instead internal strategies defined by rewrite theories at the metalevel. This is because rewriting logic is reflective [10] in the precise sense of having a universal theory U that can represent any finitely presented rewrite theory T (including U itself) and any terms t,t' in T as terms |¯T¯| and |¯t¯| , |¯t'¯| in U, so that we have the following equivalence:
T |- t --> t' <=> U |- < |¯T¯| , |¯t¯| > --> < |¯T¯| , |¯t'¯| >.Since U is representable in itself, we can then achieve a "reflective tower" with an arbitrary number of levels of reflection. Maude efficiently supports this reflective tower through its META-LEVEL module, which makes possible not only the declarative definition and execution of user-definable rewriting strategies, but also many other applications, including an extensible module algebra of parameterized module operations that is defined and executed within the logic.
This extensibility by reflection is exploited in Maude's design and implementation, so that the basic functionalities of the language, Core Maude, are extended by reflection to Full Maude. Core Maude supports module hierarchies consisting of (unparameterized) functional and system modules and provides the META-LEVEL module. Full Maude is an extension of Core Maude written in Core Maude itself that supports a module algebra of parameterized modules, views, and module expressions in the OBJ style [27] as well as object-oriented modules with convenient syntax for object-oriented applications.