Sorts and subsorts

The first thing a specification needs to declare are the types (that in the algebraic specification community are usually called sorts) of the data being defined and the corresponding operations. Sorts can be partially ordered via a subsort relation.

A sort is declared using the sort keyword followed by an identifier (the sort name), followed by white space and a period, as follows:

  sort $\langle$Sort$\rangle$ .

and multiple sorts may be declared using the sorts keyword, as follows:

  sorts $\langle$Sort-1$\rangle$ ... $\langle$Sort-k$\rangle$ .

The period at the end of the sort declaration, as for the other types of declarations, is crucial. Note that if either the period is missing or no space is left before and after the period, there can be parsing problems or unintended behavior. For example, the following declaration is syntactically correct but causes an unintended interpretation because of a missing `.', since this way sorts A, B, sort, and C are declared.

  sorts A B
  sort C .

Note also that the keywords sort and sorts are synonyms. One may use sort for multiple sort declarations and sorts for single ones, although we do not encourage this style.

For example, we can declare sorts Zero, NzNat, and Nat in the NUMBERS module, either one at a time

  sort Zero .
  sort NzNat .
  sort Nat .

or all at once

  sorts Zero Nat NzNat .

The identifiers <, ->, and ~> cannot be used as sort names. Moreover, identifiers used for sorts cannot contain any of the characters `:', `.', `[', or `]'. The reasons for these restrictions will become clear below in this section and in Sections 3.4, 3.5, and 11.2.1. The use of `{', `}', and `,' is only allowed in structured sort names (see below). Although any so restricted identifier is a legal sort name, the preferred style is to capitalize the first letter of the name. Furthermore, in the case of a compound name, such as a sort of nonzero naturals, the names (each with the first letter capitalized) or suitable abbreviations will be juxtaposed without spaces or hyphens, like, for example, NzNat.

A sort name can also be structured. Structured sort names are used in parameterized modules; for example, we may use List{X} for a parameterized list sort with parameter X and List{Nat} for its instantiation to lists of natural numbers (see Section 6.3.3). A structured sort name contains at least one pair of curly brace symbols `{' and `}', and is constructed according to the following BNF grammar, without any white space between terminals:

  $\langle$Sort$\rangle$     ::= $\langle$sort identifier$\rangle$
                $\langle$Sort$\rangle$ { $\langle$SortList$\rangle$ }
  $\langle$SortList$\rangle$ ::= $\langle$Sort$\rangle$
                $\langle$SortList$\rangle$ , $\langle$Sort$\rangle$

Notice that structured sorts are allowed to contain `{', `,' and `}' but only in accordance with the above grammar. Thus all the following are structured sort names:

  a{X}
  a{X, Y}
  a{b, c{d}}{e}
  a{(}

while the following are not legal sort names:

	{X}	(lacks sort identifier prefix)
	a(X, Y)	(`,' not inside braces)
	a{b, {d}}{e}	({d} lacks sort identifier prefix)
	a({)	(`{' without closing `}')

Structured sort names can be written in an equivalent single-identifier form by using backquotes. For example, the sort a{b, c{d}}{e} may be written as a`{b`,c`{d`}`}`{e`}. Hybrid notation such as in a{b`,c} is not allowed. When backquotes are omitted, the sort name becomes a sequence of tokens according to Maude's usual tokenization rules and arbitrary white space may be inserted between tokens. For example, Foo`{X`,Y`}, Foo{X,Y}, and Foo{X, Y}Ê are three equivalent forms for the same structured sort name.

Structured sort names must be written in their equivalent single-identifier form inside operator hooks (see Chapter 7) or in metasyntax (see Chapter 11).

Apart from their special syntax and their use as parameterized sorts in parameterized modules (see Section 6.3.3), structured sort names behave just like sort identifiers.

The subsort relation on sorts parallels the subset relation on the sets of elements in the intended model of these sorts. Subsort inclusions are declared using the keyword subsort. The declaration

  subsort $\langle$Sort-1$\rangle$ < $\langle$Sort-2$\rangle$ .

states that the first sort is a subsort of the second. For example, the declarations

  subsort Zero < Nat .
  subsort NzNat < Nat .

specify that the sorts Zero (containing only the constant 0) and NzNat (the nonzero natural numbers) are subsorts of Nat, the natural numbers. More than one subsort relationship can be declared using the keyword subsorts, as follows:

  subsorts $\langle$Sort-1$\rangle$ ... $\langle$Sort-j$\rangle$ < ... < $\langle$Sort-k$\rangle$ ... $\langle$Sort-l$\rangle$ .

Then, the above declarations can be given in a single declaration as follows:

  subsorts Zero NzNat < Nat .

If we extend NUMBERS with sorts Int and NzInt we can express the additional subsort relationships compactly by

  sorts NzInt Int .
  subsorts NzNat < NzInt Nat < Int .

A set of subsort declarations must define a partial order among the set of sorts. For this to be true, the user is required to avoid cycles in the subsort declarations. For example, if a sort A is declared as a subsort of B, and B is declared as a subsort of A, we would have a cycle.

Note that the partial order of subsort inclusions partitions the set of sorts into connected components, that is, into sets of sorts that are directly or indirectly related in the subsort ordering. For example, all the above sorts Zero, Nat, NzNat, NzInt, and Int belong to the same connected component in the subsort ordering, whereas a sort Bool would clearly belong to a different connected component and could have other sorts, for example a supersort Prop of propositions, related to it in the same component. Intuitively, connected components gather together related sorts of data such as numerical data, truth-value data, and so on. Graphically, we can visualize the partial order of subsort inclusions as an acyclic graph (the corresponding Hasse diagram), and then the connected components are exactly those of the underlying graph, as in the following example: