In Maude the user can
specify each operator with its own syntax, which can be prefix, postfix,
infix, or any ``mixfix'' combination. This is done by indicating with
underscores the places where the arguments appear in the mixfix syntax. For
example, the infix list cons operator above is specified by
_._, the (empty syntax) multiset union operator by __,
and the if-then-else operator by if_then_else_fi. In practice,
this improves readability (and therefore understandability) of programs and data.
In particular, for metalanguage uses, in which another
language or logic is represented in Maude, this can make a big difference for
understanding large examples, since the Maude representation can keep
essentially the original syntax. The combination of user-definable syntax
with equations and equational attributes for matching leads to a very
expressive capability for specifying any user-definable data. It is
well known that any computable data type can be equationally specified
[4]. Maude gives users full support for this equational style of
defining data which is not restricted to syntactic terms (trees) but can also
include lists (modulo associativity), multisets (modulo associativity and
commutativity), sets (adding an idempotency equation), and other
combinations of equational attributes that can then be used in matching. This
great expressiveness for defining data is further enhanced by Maude's rich
type structure, as explained below.