Preregularity and equational attributes

We recall from Section 3.8 that Maude assumes that modules are preregular and generates warnings when a module contains operator declarations that do not satisfy this property. This means that for each possible combination of argument sorts the resulting term has a unique least type, which is usually a sort but might also be the kind, depending on the operator declarations. However, as also explained in Section 3.8, in the presence of equational attributes, such as assoc, comm, id:, and idem (see Section 4.4.1), preregularity must be understood modulo the axioms $A$ declared by such attributes. That is, we want not just each term $t$, but also each equivalence class $[t]_{A}$ to have a least sort. Therefore, there is an additional requirement for an operator that is declared associative, namely, that the least type of a term should not depend on the way nested operators are associated. Let us explain this situation in some detail.

The assoc attribute, stating that a binary operator is associative, appears usually associated with declarations of operators whose arguments are both of the same sort, like, for example,

   op _+_ : Nat Nat -> Nat [assoc] .

However, in the presence of subsorts and overloaded operators it also makes sense to have binary operators whose arguments are not the same, but are related via subsorting; for example, to make it explicit that the addition of a natural number to a nonzero natural number produces a nonzero natural number, we can have an additional declaration

   op _+_ : NzNat Nat -> NzNat [assoc] .

or also (see Section 4.4.6)

   op _+_ : NzNat Nat -> NzNat [ditto] .

Thus, in general, the assoc attribute is allowed for binary operators such that the two argument sorts and the result sort all belong to the same connected component. Therefore, it is possible to consider a module like the following:

  fmod NON-ASSOCIATIVE-EX is
    sorts s1 s2 .
    subsort s1 < s2 .
    op f : s1 s2 -> s2 [assoc] .
    op a : -> s1 .
    eq f(a,a) = a .
  endfm

If we try to reduce the term f(a,a), we get the following warning:

  Maude> red f(a, a) .
  Warning: sort declarations for associative operator f are
    non-associative on 2 out of 27 sort triples. First such triple is
    (s1, s1, s2).
  reduce in NON-ASSOCIATIVE-EX : f(a, a) .
  rewrites: 1 in 0ms cpu (0ms real) (~ rews/sec)
  result s1: a

Maude has checked the preregularity property on the associative operator f. It is enough to check this property on each triple of types, and when it fails to hold Maude returns the first such triple. In this example we have three possible types for each one of the two arguments and also for the result, namely, the sorts s1 and s2, and the corresponding kind [s2], and therefore we have $3^3 = 27$ possible triples. Among those, the triple (s1, s1, s2) does not satisfy the preregularity checking, because f(X:s1, X:s1) has sort s2, f(X:s1, X:s2) has sort s2, and f(X:s2, X:s2) has kind [s2], but no sort; thus the flattened term f(X:s1, X:s1, X:s2) could have either sort s2, by grouping the arguments as f(X:s1, f(X:s1, X:s2)), or kind [s2], by grouping the arguments as f(f(X:s1, X:s1), X:s2)). To sum up, the sort structure for the operator f is said to be non-associative on the triple (s1, s1, s2).

Two ways of avoiding this undesirable situation are the following: either having a unique declaration at the top sort with both arguments of the same sort,

   fmod ASSOCIATIVE-EX1 is
     sorts s1 s2 .
     subsort s1 < s2 .
     op f : s2 s2 -> s2 [assoc] .
     op a : -> s1 .
     eq f(a,a) = a .
   endfm

   Maude> red f(a, a) .
   reduce in ASSOCIATIVE-EX1 : f(a, a) .
   rewrites: 1 in 0ms cpu (0ms real) (~ rews/sec)
   result s1: a

or adding enough declarations to cover all possible combinations of arguments; in this case only one more declaration is enough, as follows:

   fmod ASSOCIATIVE-EX2 is
     sorts s1 s2 .
     subsort s1 < s2 .
     op f : s2 s2 -> s2 [assoc] .
     op f : s1 s2 -> s2 [assoc] .
     op a : -> s1 .
     eq f(a,a) = a .
   endfm

   Maude> red f(a, a) .
   reduce in ASSOCIATIVE-EX2 : f(a, a) .
   rewrites: 1 in 0ms cpu (0ms real) (~ rews/sec)
   result s1: a

When an associative operator is also declared to be commutative using the comm atribute, Maude computes the commutative completion (switching the order of the argument sorts) of the given operator declarations before checking preregularity.

In the case of the id: and idem attributes, preregularity modulo those axioms requires that all collapses, that is, all passages from a term $f(t,e)$ to an equivalent term $t$ by application of an identity equation $f(x,e)=x$; or from a term $f(t,t)$ to an equivalent term $t$ by application of an idempotency equation $f(x,x)=x$ (where in both cases the top function symbol $f$ disappears), should be such that the least sort of the resulting term $t$ is smaller than or equal to the least sort of $f(t,e)$ (resp. $f(t,t)$). A term that can collapse from one sort to a greater or incomparable sort breaks the sort calculations and violates preregularity modulo such axioms. Therefore, syntactic conditions ensuring that a collapse is also into a lesser or equal sort are checked by Maude for both the id: and idem attributes.