Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

On Friday 25 November 2005 09:51, Craig Ugoretz wrote:
> WARNING:  sort declarations for the associative operator (operator) are
> non-associative on 18 out of 125 sort triples.  First such triple is (KI,
> Elt, Elt).
>
>      What does this error message mean?  Am I not modelling the problem
> correctly?

When you give sort declarations for an operator, Maude requires that they be 
preregular. Informally this means that for each possible combination of 
argument sorts there is a unique least type (usually a sort but might be the 
kind).

For an operator that is declared to be associative, a there is an addition 
requirement - the least type of a term should not depend on the way nested 
operators are associated. It turns out that it is enough to check this 
property on each triple of types, and when if fails to hold Maude returns the 
first such triple.

Note that when you declare an operator to be commutative, Maude computes the 
commutative completion of your sort declarations before checking 
preregularity and associativity.

In your case  X:Elt + X:Elt  has sort KI, X:KI + X:Elt has sort KI and X:KI + 
X:KI has type [KI]. Thus X:KI + X:Elt + X:Elt could have sort KI or type [KI] 
depending on how you group the arguments. Thus the sort structure for _+_ is 
not associative.

>      Additionally, how would a person add an identity element and an
> inverse element to the above model?

Identity elements can be added by an attibute (say id: 0) or an equation
(say eq X:KI + 0 = X:KI .). Equations are only used left to right for 
rewriting where as identity attributes can be used either way during matching 
which is often useful but can sometimes be surprising and lead to 
nontermination. Inverses can be defined by equations (say eq inv(X:KI) + X:KI 
= 0 .).

Steven