The extended signature of a module

In addition to the signature defined by the user, parsing of terms takes place in an extended grammar in which information for handling parentheses, sort and equality predicates, if_then_else_fi, and qualification operators are included. These structures belong to the so-called extended signature of a module. The main structures added in the extended signature of a module are:

• Sort disambiguation. For each sort S in the signature of a module, Maude adds to the signature the operator

    op (_).S : S -> S .
  

  This helps in the disambiguation of ad-hoc overloaded constants and terms. As an example, remember from Section 3.6 that if we declare 0 as an ad-hoc overloaded constant for natural numbers and for natural numbers modulo 3, then we can disambiguate the expression 0 + 0 by writing, for example, 0 + (0).Nat and 0 + (0).Nat3, or (0 + 0).Nat and (0 + 0).Nat3. As another example, in the module META-MODULE (see Section 11.3), the term none is ambiguous, since the operator none is used as the empty set of operator declarations, equations, rules, etc. We can disambiguate it by writing (none).OpDeclSet. Of course, these disambiguation operators can be used not only for constants, but for any term. For example, we can write (2 + 3).Nat as a valid term in the predefined module NAT.

• Parentheses. The extended signature of a module contains the operator

    op (_) : S -> S .
  

  for each sort S in its signature. These operators allow the use of parentheses without having to declare a parentheses operator for each sort. For example, (2 + 3), (2 + 3) + 5, (2 + (3) + 5), (((2 + 3)) + 5), are all valid terms in NAT, thanks to these declarations.

• Equivalent single-identifier form for all operators. Each declared operator, including those in mixfix form, may also be used in their equivalent single-identifier prefix form. For example, in the NAT module, the term _+_(2, 3) is equivalent to 2 + 3, and the terms if true then 2 + 3 else - 3 fi and if_then_else_fi(true, _+_(2, 3), -_(3)) are equivalent; any combination is possible so if_then_else_fi(true, 2 + 3, - 3) is also valid.

• Flattened associative argument lists. Operators with the attribute assoc may be used in Maude in a nonparenthesized flattened form (see Section 4.8). This is possible thanks to the precedence-gathering values in mixfix notation, but it is also possible in prefix syntax. For example, gcd(2, 3, 4) is a valid term in NAT, where gcd is the greater common divisor operator, which is declared as a binary associative operator. Of course, this term can always be written in the standard format as gcd(2, gcd(3, 4)) or gcd(gcd(2, 3), 4). Furthermore, we can combine this possibility with the single-identifier form to write things like _+_(2, 3, 4) instead of _+_(_+_(2, 3), 4) or _+_(2, _+_(3, 4)), but of course, since _+_ is declared with the assoc attribute in the predefined module NAT, we can just write 2 + 3 + 4.

• Polymorphic operators and the BOOL module. All the information contained in the predefined modules TRUTH-VALUE, TRUTH, and BOOL is included in the extended signature of each module (unless this inclusion is explicitly disabled). In particular, appropriate instances of the polymorphic operators contained in TRUTH (that is, if_then_else_fi, _==_, and _=/=_) are generated for each sort in the module; in addition, for each sort S, a sort predicate _:: S is also added. All these modules and operators are fully explained in Section 7.1.