Operator overloading

Operators in Maude can be overloaded, that is, we can have several operator declarations for the same operator with different arities and coarities. Consider extending our number module with a new sort Nat3 (of natural numbers modulo 3), constants 0, 1, and 2 of sort Nat3, and two further operator declarations for _+_.

  op _+_ : NzNat Nat -> NzNat .
  sort Nat3 .
  ops 0 1 2 : -> Nat3 .
  op _+_ : Nat3 Nat3 -> Nat3 .

Now _+_ is overloaded, having three declarations. However, there are two different kinds of overloading present in the example. The additional declaration of _+_ with first argument NzNat is an example of subsort overloading. Here the two _+_ operators on Nat and NzNat are supposed to have the same behavior on their shared argument values, that is, the operator on the subsort NzNat is the restriction of the operator on the larger sort Nat. The main point of such declarations is to give more sort information, for example that the result of adding a nonzero natural number to any natural number is nonzero. Many more examples of this form of overloading can be found in the predefined data modules for the number hierarchy (Chapter 7) and in other modules throughout the manual.

In contrast, the sorts Nat and NzNat on the one hand, and the sort Nat3 on the other belong to 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.

Strictly speaking, this requirement would rule out ad-hoc overloaded constants. For this reason, 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 (see Chapter 6.3) can appear in many different connected components for different instances of the module, and it may be cumbersome to rename them all. To allow this relaxation, constants--and, more generally, terms (see Section 3.8)--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 natural numbers and for natural numbers 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.