We first explain the syntactic conventions about Maude identifiers, which must be followed when declaring module, sort, and operator names. Then we explain the notions of order-sorted signature and overloading that are key for understanding the syntax of expressions in functional and system modules.
In Core Maude, the name of a module or a sort must be an identifier. For example, PATH, Edge, and Path are identifiers. In general, an identifier in Maude is any finite string of ASCII characters such that:
The conventions for the syntactic form of operators allow great flexibility in their user-definable syntax. An operator declared using a single identifier has automatically a prefix form, in which it can be displayed before its arguments enclosed in parentheses; but if such an operator contains underscore characters `_' then it must contain exactly as many underscores as the number of sorts in its arity, and in that case it has also a mixfix form. For example, _+_(2,3) and 2 + 3 are the prefix and mixfix ways of displaying the same arithmetic expression8.
An operator can also be declared using several identifiers. This can be due to the presence of special characters, or to blank spaces, or both. Consider for example the operator declaration
that may allow a natural language style in the syntax of a programming language. It uses eight identifiers in the Maude sense, but declares a single binary operator, with the underscores indicating the place of the arguments in the mixfix notation. Internally, Maude also associates to this operator a corresponding single identifier variant by using backquotes. This is the form in which we could have equivalently defined the operator using a single identifier, namely,op [_] and then [_] : Command Command -> Command .
Of course, both variants are equivalent and have the same mixfix display, but the version without backquotes is obviously more convenient.op `[_`]and`then`[_`] : Command Command -> Command .
The declaraton of an operator requires an extra pair of parentheses if we already use parentheses as part of the syntax of the operator. Suppose we had in a programming language another binary operator (_ only after _). We have to declare it as follows.
op ((_ only after _)) : Command Command -> Command .
Since an operator may be declared using several identifiers, in an ops declaration involving several operators each operator declaration can be enclosed in parentheses if necessary, to indicate where the syntax of each operator begins and ends. Then, we could have declared both operators together as follows.
op ([_] and then [_]) ((_ only after _)) :
Command Command -> Command .
We now turn to order-sorted signatures. As the GRAPH example shows, the sorts declared in a functional module (and the same will hold for system modules) can be related by a subsort inclusion ordering. At the level of the corresponding algebras this subsort ordering is interpreted as set-theoretic inclusion of the data in a subsort into the data in a supersort. For example, every Edge is a Path, and every Path is a Path?. In general, we can declare arbitrary long chains of subsort inclusions, not only between individual sorts, but between sets of sorts. For example, if sorts A, B, and C are each of them subsorts of sorts D and E, and these in turn are subsorts of sorts F, G, and H, we can specify all these inclusions with a single declaration
subsorts A B C < D E < F G H .
Another feature of order-sorted signatures is that the function symbols declared in the signature can be overloaded, that is, we can have several operator declarations for the same operator with different arities and coarities. Consider for example the module
fmod NUMBERS is
sorts Nat NzNat Nat3 .
subsort NzNat < Nat .
op zero : -> Nat .
op s_ : Nat -> NzNat .
op p_ : NzNat -> Nat .
op _+_ : Nat Nat -> Nat .
op _+_ : NzNat NzNat -> NzNat .
ops 0 1 2 : -> Nat3 .
op _+_ : Nat3 Nat3 -> Nat3 [comm] .
vars N M : Nat .
var N3 : Nat3 .
eq p s N = N .
eq N + zero = N .
eq N + s M = s (N + M) .
eq (N3 + 0) = N3 .
eq 1 + 1 = 2 .
eq 1 + 2 = 0 .
eq 2 + 2 = 1 .
endfm
declaring the natural numbers in Peano notation with a subsort NzNat
of nonzero natural numbers and with successor, predecessor and addition
functions, and declaring also the integers modulo 3 with their addition
as a commutative (comm) operator.
The addition operator has three declarations and is therefore overloaded. However, there are two different kinds of overloading present in the example. The signature of the example is an order-sorted signature [26] in which overloaded operators related in the subsort ordering, such as the two additions for natural numbers and for nonzero natural numbers, are supposed to have the exact same behavior, in the sense that the bigger operator restricts to the smaller one on the subsorts; such operators are called subsort overloaded. Addition in the number hierarchy of naturals, integers, rationals, and so on, provides a very familiar example of subsort overloading, of which the present overloading of natural number addition is a special case (see Section 2.3).
By contrast, the sorts Nat and NzNat on the one hand, and the sort Nat3 on the other form two different connected components in the subsort ordering and therefore natural number addition and addition modulo-3 are semantically unrelated. This form of overloading is called ad-hoc overloading. Both subsort and ad-hoc overloading of operators are allowed in Maude. However, to avoid ambiguous expressions we require that if the sorts in the arities of two operators with the same syntactic form are pairwise in the same connected components, then the sorts in the coarities must likewise be in the same connected component.
In particular, this rules out ad-hoc overloaded constants. Therefore, we have declared two different constants zero and 0 for the corresponding zero elements. However, this requirement can be relaxed, and it is often natural to do so. For example, the constants of a parameterized module can appear in many different connected components for different instances of the module, and it may be cumbersome to qualify them all. To allow this relaxation, constants--and, more generally, terms--can be qualified by their sort, by enclosing them in parentheses followed by a dot and the sort name. In this way, we could have instead declared 0 as an ad-hoc overloaded constant for naturals and for integers modulo-3, and could then disambiguate the expression 0 + 0 by writing, for example, 0 + (0).Nat and 0 + (0).Nat3, or (0 + 0).Nat and (0 + 0).Nat3.
Note that in an order-sorted signature a term can have several sorts. For example, the term s s 0 in the NUMBERS module has sorts NzNat and Nat. An order-sorted signature is called preregular [26] when the set of sorts that can be assigned to a term according to the signature has always a least element. The order-sorted signatures in functional and system modules are assumed to be preregular.
Note that, as already mentioned, Maude will extend the signature given by the user in a module by adding the error supersorts above each connected component of sorts, and by adding an additional subsort overloaded operator with all its arities and coarities in the corresponding error supersorts for each family of subsort overloaded operators in the original signature for the purpose of dealing with error terms. Other operators such as equality predicates, sort predicates, and if-then-else, as well as the above-mentioned sort qualification operators are also added. See Section 2.7.2 for more details about this extended signature.