Another functional module example is provided by the following SET-HIERARCHY functional module, that defines the set hierarchy of all finite sets whose most basic elements are machine integers. Comments on the meaning of operations and equations are included in the text. Such comments must begin with *** or --.
fmod SET-HIERARCHY is
protecting MACHINE-INT .
sorts Set Elt Magma .
subsorts Set < Elt < Magma .
subsorts MachineInt < Elt .
op mt : -> Set . *** empty set
op _,_ : Magma Magma -> Magma [assoc comm] .
op {_} : Magma -> Set .
*** set constructor
ops _U_ _I_ : Set Set -> Set [assoc comm] .
*** union, intersection
op _\_ : Set Set -> Set . *** difference
op _in_ : Elt Set -> Bool .
op P : Set -> Set . *** power set
op augment : Set Set -> Set .
op |_| : Set -> MachineInt . *** cardinality
vars L M : Magma .
vars E F : Elt .
vars S T : Set .
*** equations between constructors to eliminate
*** duplicate elements
eq { L , L , M } = { L , M } .
eq { L , L } = { L } .
*** set union
eq S U mt = S .
eq { L } U { M } = { L , M } .
*** set membership
eq E in mt = false .
eq E in { F } = (E == F) .
eq E in { F , L }
= if E == F then true else E in { L } fi .
*** set intersection
eq mt I S = mt .
eq { E } I S = if E in S then { E } else mt fi .
eq { E , L } I S = ({ E } I S) U ({ L } I S) .
*** set difference
eq mt \ S = mt .
eq { E } \ S = if E in S then mt else { E } fi .
eq { E , L } \ S = ({ E } \ S) U ({ L } \ S) .
*** power set (defined using auxiliary function "augment")
eq P(mt) = { mt } .
eq P({ E }) = { mt , { E } } .
eq P({ E , L }) = P({ L }) U augment(P({ L }), { E }) .
eq augment(mt, T) = mt .
eq augment({ S } , T) = { S U T } .
eq augment({ S , L } , T)
= { S U T } U augment({ L }, T) .
*** cardinality
eq | mt | = 0 .
eq | { E } | = 1 .
eq | { E , L } |
= | { L } | + if E in { L } then 0 else 1 fi .
endfm
A finite set is represented using the standard notation {E1,...,En} as an (associative and commutative) collection of elements E1,...,En (here called a Magma) that is then enclosed in curly brackets by applying the constructor {_} , that builds a set out of a magma. Since Set is a subsort of Magma, sets can contain other sets as elements, and therefore we get the entire hierarchy of finite sets. The meaning of each operation symbol is explained either in its declaration or in the comments that precede the equations for that symbol. Notice that now several operators such as element concatenation, set union, and set intersection are declared to be associative and commutative with the assoc and comm attributes. The Maude engine then performs multiset matching and rewriting on those symbols; that is, neither association of parentheses nor the order of elements matter at all when finding a match. In general, the Maude engine can rewrite modulo most of the different combinations of associativity, commutativity, identity (left-, right-, or two-sided) and idempotency for different operators in the given specification. This of course gives the effect of rewriting the equivalence classes modulo such axioms of the terms in question, instead or rewriting just the terms themselves.
Note that the equational axioms declared as attributes of operators should not be written explicitly as equations in the specification. There are two reasons for this. Firstly, this is redundant, since they have already been declared as attributes. Secondly, although declaring such equations either only explicitly as equations, or twice--one time as attributes, and another as explicit equations--does not affect the mathematical semantics of the specification, that is, the initial algebra that the specification denotes (see Section 4.1) it does however drastically alter the specification's operational semantics. Indeed, Maude uses the equations from left to right as simplification rules, matching the equations modulo the axioms declared as attributes in operators. The equations in a Maude specification are assumed to be Church-Rosser and terminating modulo such axioms. But they may fail to have such properties if the axioms are instead added as ordinary equations. For example, a commutativity equation for set union such as
eq S U T = T U S .would make the above specification nonterminating.
Here are several sample reductions of set expressions.
Maude> red P({ 1 , 2 , 3 }) \ P({ 1 , 2 }) .
result Set: {{3}, {1, 3}, {2, 3}, {1, 2, 3}}
Maude> red | P(P({ 1 , 2 , 3 })) | .
result NzMachineInt: 256
Maude> red | (P(P({1 , 2 , 3 })) \ P(P({ 1 , 2 }))) | .
result NzMachineInt: 240