A Maude program containing only equations is called a functional module.
It is a functional program defining one or more functions by means of
equations, used as simplification rules. For example, if we build lists of
quoted identifiers (which are sequences of characters starting with the
character `'' and belong to a sort1.1 Qid) with a ``cons'' operator
denoted by an infix period,
op nil : -> List . op _._ : Qid List -> List .
then we can define a length function and a membership predicate by means of the operators and equations
op length : List -> Nat . op _in_ : Qid List -> Bool . vars I J : Qid . var L : List . eq length(nil) = 0 . eq length(I . L) = s length(L) . eq I in nil = false . eq I in J . L = (I == J) or (I in L) .
where s_ denotes the successor function on natural numbers,
_==_ is the equality predicate on quoted identifiers, and
_or_ is the usual disjunction on Boolean values. Such
equations (specified in Maude with the keyword eq and ended with a
period) are used from left to right as equational
simplification rules. For example, if we want to evaluate the expression
length('a . 'b . 'c . nil)
we can apply the second equation for length to simplify the expression three times, and then apply the first equation once to get the final value s s s 0:
length('a . 'b . 'c . nil)
= s length('b . 'c . nil)
= s s length('c . nil)
= s s s length(nil)
= s s s 0
This is the standard ``replacement of equals by equals'' use of equations in elementary algebra and has a very clear and simple semantics in equational logic. Replacement of equals by equals is here performed only from left to right and is then called equational simplification or, alternatively, equational rewriting. Of course, the equations in our program should have good properties as ``simplification rules'' in the sense that their final result exists and should be unique. This is indeed the case for the two functional definitions given above.
In Maude, equations can be conditional; that is, they may only be applied if a certain condition holds. For example, we can simplify a fraction to its irreducible form using the conditional equation
vars I J : NzInt .
ceq J / I = quot(J, gcd(J, I)) / quot(I, gcd(J, I))
if gcd(J, I) > s 0 .
where ceq is the Maude keyword introducing conditional equations, NzInt is the sort of nonzero integers, and where we assume that the integer quotient (quot) and greatest common divisor (gcd) operations have already been defined by their corresponding equations.
A Maude program containing rules and possibly equations is called a system module. Rules are also computed by rewriting from left to right, that is, as rewrite rules, but they are not equations; instead, they are understood as local transition rules in a possibly concurrent system. Consider, for example, a distributed banking system in which we envision the account objects as floating in a ``soup,'' that is, in a multiset or bag of objects and messages. Such objects and messages can ``dance together'' in the distributed soup and can interact locally with each other according to specific rewrite rules. We can represent a bank account as a record-like structure with the name of the object, its class name (Account) and a bal(ance) attribute, say, a natural number. The following are two different account objects in our notation:
< 'A-001 : Account | bal : 200 > < 'A-002 : Account | bal : 150 >
Accounts can be updated by receiving different messages and changing their state accordingly. For example, we can have debit and credit messages, such as
credit('A-002, 50)
debit('A-001, 25)
We can think of the ``soup'' as formed just by ``juxtaposition'' (with empty syntax) of objects and messages. For example, the above two objects and two messages form the soup
< 'A-001 : Account | bal : 200 >
< 'A-002 : Account | bal : 150 >
credit('A-002, 50)
debit('A-001, 25)
in which the order of objects and messages is immaterial. The local interaction rules for crediting and debiting accounts are then expressed in Maude by the rewrite rules
var I : Qid .
vars N M : Nat .
rl < I : Account | bal : M > credit(I, N)
=> < I : Account | bal : (M + N) > .
crl < I : Account | bal : M > debit(I, N)
=> < I : Account | bal : (M - N) >
if M >= N .
where rules are introduced with the keyword rl and conditional rules (like the above rule for debit that requires the account to have enough funds) with the crl keyword.
Note that these rules are not equations at all: they are local transition rules of the distributed banking system. They can be applied concurrently to different fragments of the soup. For example, applying both rules to the soup above we get the new distributed state:
< 'A-001 : Account | bal : 175 > < 'A-002 : Account | bal : 200 >
Note that the rewriting performed is multiset rewriting, so that, regardless of where the account objects and the messages are placed in the soup, they can always come together and rewrite if a rule applies. In Maude this is specified in the equational part of the program (system module) by declaring that the (empty syntax) multiset union operator satisfies the associativity and commutativity equations:
X (Y Z) = (X Y) Z X Y = Y X
This is not done by giving the above equations explicitly. It is instead done by declaring the multiset union operator with the assoc and comm equational attributes (see Section 4.4.1 and Section 1.1.2 below), as follows, where Configuration denotes the multisets or soups of objects and messages.
op __ : Configuration Configuration -> Configuration [assoc comm] .
Maude then uses this information to generate a multiset matching algorithm, in which the multiset union operator is matched modulo associativity and commutativity.
Again, a program involving such rewrite rules is intuitively very simple, and has a very simple rewriting semantics. Of course, the systems specified by such rules can be highly concurrent and nondeterministic; that is, unlike for equations, there is no assumption that all rewrite sequences will lead to the same outcome. For example, depending on the order in which debit or credit messages are consumed, a bank account can end up in quite different states, because the rule for debiting can only be applied if the account balance is big enough. Furthermore, for some systems there may not be any final states: their whole point may be to continuously engage in interactions with their environment as reactive systems.