Kinds

The equational logic underlying Maude is membership equational logic [60,7]. In this logic sorts are grouped into equivalence classes called kinds. For this purpose, two sorts are grouped together in the same equivalence class if and only if they belong to the same connected component. Maude sorts are user-defined, while kinds are implicitly associated with connected components of sorts and are considered as ``error supersorts.'' Terms (see Section 3.8) that have a kind but not a sort are understood as undefined or error terms.

In Maude modules, kinds are not independently and explicitly named. Instead, a kind is identified with its equivalence class of sorts and can be named by enclosing the name of one or more of these sorts in square brackets [...]; when using more than one sort, they are separated by commas.

For example, suppose we add a partial predecessor function to our NUMBERS module,

  op p : NzNat -> Nat .

Then Maude will parse the term p(zero) and assign it the kind [Nat], or equivalently [NatSeq] or also [Nat, NatSeq], since the sorts Nat and NatSeq belong to the same connected component. Although any sort, or list of sorts in the connected component, can be enclosed in brackets to denote the corresponding kind, Maude uses a canonical representation for kinds; specifically, Maude prints the kind using a comma-separated list of the maximal elements of the connected component.

The Maude system also lifts automatically to kinds all the operators involving sorts of the corresponding connected components to form error expressions. Such error expressions allow us to give expressions to be evaluated the benefit of the doubt: if, when they are simplified, they have a legal sort, then they are okay; otherwise, the fully simplified error expression is returned, which the user can interpret as an error message. Equational simplification can also occur at the kind level, so that operators can map error terms to defined terms, which may be useful for error recovery.

It is also possible to explicitly declare operators at the kind level. This corresponds to declaring a partial operation, which is defined for those argument values for which Maude can determine that the resulting term has a sort. Note that the operation is considered to be total at the kind level. As an example, consider the following fragment of a graph specification:

  sorts Node Edge .
  ops source target : Edge -> Node .
  sort Path .
  subsort Edge < Path .
  op _;_ : [Path] [Path] -> [Path] .

The sorts Node and Edge, along with the source and target operators mapping edges to nodes, axiomatize the basic graph concepts. The sort Path is intended to be the paths through the graph, sequences of edges with the target of one edge being the source of the next edge. Edges are singleton paths, and _;_ denotes the partial concatenation operation, indicated by giving kinds rather than sorts in the argument list. Later, in Section 4.3, we will see how to specify when a sequence of edges has sort Path.

To emphasize the fact that an operator defined at the kind level in general defines only a partial function at the sort level, Maude also supports a notational variant in which an (always total) operator at the kind level can equivalently be defined as a partial operator between sorts in the corresponding kinds, with syntax `~>' instead of `->' to indicate partiality. For example, the above operator declaration can be equivalently specified by

  op _;_ : Path Path ~> Path .

More generally, the partial operator declaration

  op $\langle$OpName$\rangle$ : $\langle$Sort-1$\rangle$ ... $\langle$Sort-k$\rangle$ ~> $\langle$Sort$\rangle$ .

is equivalent to the total operator declaration at the kind level

  op $\langle$OpName$\rangle$ : [$\langle$Sort-1$\rangle$] ... [$\langle$Sort-k$\rangle$] -> [$\langle$Sort$\rangle$] .