[Maude-help] Fwd: Error message: associative operators
craigugoretz at gmail.com
Fri Nov 25 11:53:37 CST 2005
I apologize, the declaration for the operator * should read:
op _*_ : Elt KI -> KI [assoc comm prec 2] .
---------- 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
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)) .
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,
What does this error message mean? Am I not modelling the problem
Additionally, how would a person add an identity element and an inverse
element to the above model?
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Maude-help