Maude-help mailing list

[Craig Ugoretz <craigugoretz AT gmail.com>]

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