[Maude-help] Fwd: Error message: associative operators

[Craig Ugoretz]

I apologize, the declaration for the operator * should read:

     op _*_  : Elt KI -> KI [assoc comm prec 2] .

                                                      Craig

---------- Forwarded message ----------
From: Craig Ugoretz <craigugoretz at gmail.com>
Date: Nov 25, 2005 11:51 AM
Subject: Error message: associative operators
To: maude-help at maude.cs.uiuc.edu


Hello,

     After my last two emails, I have made progress on the issue of sorts to
the point where I have written a functional module that depends on them.
The fmod NSFIELD is supposed to implement a form of numbers similar to
complex numbers, with the exception that I squared is equal to I instead of
I squared equal to negative one.  The fmod is given below:

fmod NSFIELD is
     protecting FLOAT .

     sort K I KI Elt .
     subsort K I < Elt < KI .

     op K : Float -> K [ctor] .
     op I  : Float -> I [ctor] .
     op _+_ : Elt KI -> KI [assoc comm prec 1] .
     op _*_  : Elt KI -> KI [assoc comm prec 1] .

     vars A B C : Float .
     var M : KI .

     eq K(A) + K(B) = K(A + B) .
     eq I(A) + I(B) = I(A + B) .
     eq K(A) + K(B) + M = K(A + B) + M .
     eq I(A) + I(B) + M = I(A + B) + M .

     eq K(A) * K(B) = K(A * B) .
     eq I(A) * I(B) = I(A * B) .
     eq K(A) * I(B) = I(A * B) .
     eq K(A) * K(B) * M = K(A * B) * M .      eq I(A) * I(B) * M = I(A * B)
* M .
     eq K(A) * I(B)* M = I(A * B) * M .

     eq K(A) * (K(B) + I(C)) = (K(A) * K(B)) + (K(A) * I(C)) .
     eq I(A) * (K(B) + I(C)) = (I(A) * K(B)) + (I(A) * I(C)) .
endfm

As you can see, I use the notion of a list to gather K terms and I terms, K
being the field of real numbers, and I being the field of indeterminate
numbers.  KI is the union of the K and I fields, and Elt stands for element
of KI.  The problem is that when I try to rewrite the following: K( 2.0) *
I(3.0) + K(4.0)  + I(5.0) * I(6.0), I get the correct answer, I(144.0), but
I also get this error message for the + and * operators:

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?
     Additionally, how would a person add an identity element and an inverse
element to the above model?


Thanks,

Craig Ugoretz
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.cs.uiuc.edu/mailman/private/maude-help/attachments/20051125/1075ad26/attachment.html