4.1 Membership Equational Logic and Functional Modules

Maude is a declarative language based on rewriting logic. But rewriting logic has its underlying equational logic as a parameter. There are, for example, unsorted, many-sorted, and order-sorted versions of rewriting logic, each containing the previous version as a special case. The underlying equational logic chosen for Maude is membership equational logic [41, 5], a conservative extension of both order-sorted equational logic and partial equational logic with existence equations [41]. It supports partiality, subsort relations, operator overloading, and error specification.

A signature in membership equational logic is a triple Omega= (K,Sigma,S) with K a set of kinds, (K,Sigma) a many-sorted (although it is better to say "many-kinded") signature, and S={S_k}_k e K a K-kinded set of sorts.

An Omega-algebra is then a (K,Sigma)-algebra A together with the assignment to each sort s e S_k of a subset A_s c A_k. Intuitively, the elements in sorts are the good, or correct, or nonerror, or defined, elements, whereas the elements without a sort are error or undefined elements.

Atomic formulas are either Sigma-equations, or membership assertions of the form t : s, where the term t has kind k and s e S_k. General sentences are Horn clauses on these atomic formulae, quantified by finite sets of K-kinded variables. That is, they are either conditional equations

(forall X) t=t' if ( /\ _i u_i=v_i) /\ ( /\ _j w_j:s_j)

(forall X) t:s if ( /\ _i u_i=v_i) /\ ( /\ _j w_j:s_j).

In Maude, functional modules are equational theories in membership equational logic satisfying the additional requirement of being Church-Rosser and (preferably) terminating. Functional theories are also membership equational logic theories, but they do not need to be Church-Rosser; they have a loose interpretation, in the sense that any algebra satisfying the equations and membership axioms in the theory is an acceptable model³⁹.

The semantics of an unparameterized functional module is the initial algebra specified by its theory. The semantics of a parameterized functional module is the free functor associated to the inclusion of the parameter theory⁴⁰ into the body of the parameterized module [41]. For example, a parameterized list module LIST[X :: TRIV] forms lists of models of the trivial parameter theory TRIV with one sort Elt, whose models are sets of elements and its semantics is the functor sending each set to the algebra of lists of the set. Similarly, a sorting module SORTING[Y :: POSET] sorts lists whose elements belong to a model of the POSET functional theory, that is, the data type of elements must have a partial order and its semantics is the functor sending each poset to the algebra of lists for that poset with a sorting function⁴¹. All this is entirely similar to the semantics of "objects" (that correspond to modules in our sense) and theories in OBJ [27]. Indeed, since membership equational logic conservatively extends order-sorted equational logic, Maude's functional modules extend OBJ modules.

Maude does automatic kind inference from the sorts declared by the user and their subsort relations. There is no need to declare kinds explicitly. The convenience of order-sorted notation is retained as syntactic sugar. Thus, an operator declaration

 
  op push : Nat Stack -> NeStack . 

(forall x,y) push(x,y):NeStack if x:Nat /\ y: Stack.

(forall x) x:Stack if x:NeStack.

Computation in a functional module is accomplished by using the equations as rewrite rules until a canonical form is found. Therefore, the equations must satisfy the additional requirements of being Church-Rosser, terminating, and sort-decreasing [5]. This guarantees that all terms in an equivalence class modulo the equations will rewrite to a unique canonical form, and that this canonical form can be assigned a sort that is smaller than all other sorts assignable to terms in the class. For a module satisfying such conditions any reduction strategy will reach a normal form; nevertheless, as explained in Section 2.1.3, the user can assign to each operator a functional evaluation strategy in the OBJ style [27] to control the reduction for efficiency purposes. If no such strategies are declared, a bottom-up strategy is chosen. Since Maude supports rewriting modulo equational theories such as associativity or associativity/commutativity, all that we say has to be understood for equational rewriting modulo such axioms.

In membership equational logic the Church-Rosser property of terminating and sort-decreasing equations is indeed equivalent to the confluence of their critical pairs [5]. Furthermore, both equality and membership of a term in a sort are then decidable properties [5]. That is, the equality and membership predicates are computable functions. We can then use the metatheorem of Bergstra and Tucker [1] to conclude that such predicates are themselves specifiable by Church-Rosser and terminating equations as Boolean-valued functions. This has the pleasant consequence of allowing us to include inequalities t =/= t' and negations of sort tests not(t:s) in conditions of equations and of membership axioms, since such seemingly negative predicates can also be axiomatized inside the logic in a positive way, provided that we have a subspecification of (not necessarily free) constructors in which to do it, and that the specification is indeed Church-Rosser, terminating, and sort decreasing. Of course, in practice they do not have to be explicitly axiomatized, since they are built into the implementation of rewriting deduction in a much more efficient way (see Section 2.4.1).

Let us denote membership equational logic by MEqtl and its associated rewriting logic by MRWLogic. Regarding an equational theory as a rewrite theory whose sets of rules are empty defines a conservative map of logics [32]

MEqtl --> MRWLogic .