Terms and preregularity

A term is either a constant, a variable, or the application of an operator to a list of argument terms. The sort of a constant or variable is its declared sort. In the application of an operator, the argument list must agree with the declared arity of the operator. That is, it must be of the same length, and each term must have sort (or at least kind) in the connected component of the corresponding declared argument sort. Using prefix form--which can always be used for any operator, regardless of having been declared with either prefix or mixfix syntax--the syntax of operator application is the operator's name followed by `(', followed by a list of argument terms separated by commas, followed by `)'. Here are some examples of prefix notation from our numbers module.

  s_(zero)
  s_(sd(N:Nat, M:Nat))
  p(s_(zero))
  _+_(N:Nat, M:Nat)

The application of an operator declared with mixfix form also has a mixfix syntax: the operator's mixfix name with each underscore replaced by the corresponding term from the argument list. The mixfix form of the above examples is

  s zero
  s sd(N:Nat, M:Nat)
  p(s zero)
  N:Nat + M:Nat

The kind of a term is the result kind of its topmost operator. For example, the kind of p(s zero) is [Nat], since Nat is the result sort of p. If a module's grammar is unambiguous (see the discussion on parsing in the following section), then each term has a single kind. But we can also associate sorts to terms. In general, even if the grammar is unambiguous, a term may have several sorts, due to the subsort ordering. Specifically, constants have the sort they are declared with and any supersort of it. Given a term of the form $f(t_1,\ldots,t_n)$, if $t_i$ has sort $s_i$ for $i=1,\ldots,n$ and there is an operator declaration $f : s_1\ldots s_n \rightarrow s$, then the term $f(t_1,\ldots,t_n)$ has sort $s$ and any of its supersorts. For example, in our example NUMBERS module the term s s 0 has sorts NzNat and Nat.

A very desirable property of a module is that each term has a least sort

that can be assigned to it. Such a least sort gives us the most detailed information on how to classify such a term as a data element. For example, the least sort of the term s s 0 is NzNat, and this gives us the most precise classification of such a term in the sort hierarchy. Given an arbitrary signature $\Sigma$, we can have terms that fail to have a least sort. However, if $\Sigma$ satisfies a simple syntactic property called preregularity [43], we can guarantee that any $\Sigma$-term will have a least sort. We call $\Sigma$ preregular if for each $n$, given an $n$-argument function symbol $f$ and sorts $s_{1},\ldots,s_{n}$ such that $f(x_{1}:s_{1},\ldots,x_{n}:s_{n})$ is a well-formed $\Sigma$-term, then there is a least sort $s$ among all the sorts $s'$ appearing in (possibly overloaded) operator declarations of the form $f:s'_{1},\ldots,s'_{n}\longrightarrow s'$ in $\Sigma$ such that for $1 \leq i \leq n$ we have $s_{i} \leq s'_{i}$. For example, the signature

  sorts A B C D .
  subsorts A < B C < D .
  op a : -> A .
  op f : B -> B .
  op f : C -> C .

fails to be preregular, because for the sort A the term f(X:A) is a well-formed term, but there is no least sort for the result of f with arguments greater or equal to A, since either B or C can be chosen as result sorts, and they are incomparable in the sort hierarchy. As a consequence, both f(X:A) and f(a) do not have a least sort: they have sorts B, C, and D, and B and C are minimal sorts among those sorts.

As already mentioned in Section 3.4 for the assoc attribute and further explained in Section 4.4.1, operators can be declared with equational axioms such as associativity (assoc), commutativity (comm), and identity (id:). This means that, if we denote by $A$ the corresponding associativity and/or commutativity, and/or identity equations, we are not really interested in syntactic terms $t$, but rather in equivalence classes modulo $A$, that is, in the equivalence class $[t]_{A}$ of each term $t$, since all representatives of the class are viewed as equivalent representations. Preregularity modulo $A$ now means that we can assign a least sort not just to any well-formed term $t$, but also to its equivalence class $[t]_{A}$. As further explained in Section 13.2.5, Maude assumes that modules are preregular modulo whatever axioms such as assoc, comm, and id: have been declared for operators, checks syntactic conditions ensuring preregularity modulo $A$, and generates warnings when a module fails to satisfy such preregularity conditions.

A ground term is a term containing no variables: only constants and operators. Intuitively, ground terms denote either data in case no equations apply to the term (for example, s zero is data) or functional expressions indicating how an equationally defined function is applied to data (for example, (s zero) + (s zero)). Ground terms modulo equations constitute the initial algebra associated with a specification, as discussed later in Section 4.3.