Maude-help mailing list

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

The problem is that your term rewriting system is non-terminating. For example you define X + Y in terms of a complex _expression_ that contains X + Y

You are probably better off constructing the complex numbers over some more abstract structure such as a field; or perhaps just a signature that contains the operators you need to use. For example:

fth FIELD is
  sort Number .
  op 0 : -> Number .
  op -_ : Number -> Number [prec 15] .
  op _+_ : Number Number -> Number [prec 33 gather (E e)] .
  op _-_ : Number Number -> Number [prec 33 gather (E e)] .
  op _*_ : Number Number -> Number [prec 31 gather (E e)] .
  op _/_ : Number Number -> Number [prec 31 gather (E e)] .
endfth

Then the complex number operations are defined using pattern matching to pull numbers out of pairs:

fmod COMPLEX{X :: FIELD} is
  sort Complex{X} .
  op <_,_> : X$Number X$Number -> Complex{X} [ctor] .

var A B C D : X$Number .
  op -_ : Complex{X} -> Complex{X} .
  eq - < A, B > = < - A, - B > .

  op _+_ : Complex{X} Complex{X} -> Complex{X} [prec 33 gather (E e)] .
  eq < A, B > + < C, D > = < A + C, B + D > .

  op _-_ : Complex{X} Complex{X} -> Complex{X}  [prec 33 gather (E e)] .
  eq < A, B > - < C, D > = < A - C, B - D > .

  op _*_ : Complex{X} Complex{X} -> Complex{X} [prec 31 gather (E e)] .
  eq < A, B > * < C, D > = < A * C - B * D, B * C + A * D > .

  op _/_ : Complex{X} Complex{X} -> Complex{X} [prec 31 gather (E e)] .
  ceq < A, B > / < C, D > = < (A * C + B * D) / (C * C + D * D),
                              (B * C - A * D) / (C * C + D * D) >
      if < C, D > =/= < 0, 0 > .
endfm

The advantage of using a parametrized module is that you can then instantiate it on module that provides the operators mentioned in the parameter theory; for example FLOAT:

view FloatField from FIELD to FLOAT is
  sort Number to Float .
  op 0 to term 0.0 .
endv


fmod TEST is
  pr COMPLEX{FloatField} .
endfm

red - < 1.0, 2.0 > .
red < 1.0, 2.0 > + < 3.0, 4.0 > .
red < 1.0, 2.0 > - < 3.0, 4.0 > .
red < 1.0, 2.0 > * < 3.0, 4.0 > .
red < 1.0, 2.0 > / < 3.0, 4.0 > .

or RAT:

view RatField from FIELD to RAT is
  sort Number to Rat .
endv

fmod TEST2 is
  pr COMPLEX{RatField} .
endfm

red - < 1, 2 > .
red < 1, 2 > + < 3, 4 > .
red < 1, 2 > - < 3, 4 > .
red < 1, 2 > * < 3, 4 > .
red < 1, 2 > / < 3, 4 > .

Since the complex numbers themselves are a perfectly good field you can use them to instantiate fmod COMPLEX:

view ComplexRatField from FIELD to COMPLEX{RatField} is
  sort Number to Complex{RatField} .
  op 0 to term < 0, 0 > .
endv

fmod TEST3 is
  pr COMPLEX{ComplexRatField} .
endfm

red - < < 1, 2 >, < 3, 4 > > .
red < < 1, 2 >, < 3, 4 > > + < < 5, 6 >, < 7, 8 > > .
red < < 1, 2 >, < 3, 4 > > - < < 5, 6 >, < 7, 8 > > .
red < < 1, 2 >, < 3, 4 > > * < < 5, 6 >, < 7, 8 > > .
red < < 1, 2 >, < 3, 4 > > / < < 5, 6 >, < 7, 8 > > .

Say hello to the Rational Quaternions!

Steven

On 5/23/13 12:25 PM, Vlad Avram wrote:

Hi,

I'm trying to implement a module for complex numbers in Maude and here's what I got for now:

fmod COMPLEX is

  protecting FLOAT .

  sort Complex .

op complex : Float Float -> Complex .

op realpart : Complex -> Float .

op imagpart : Complex -> Float .

op _+_ : Complex Complex -> Complex [assoc comm] .

op _-_ : Complex Complex -> Complex .

op _*_ : Complex Complex -> Complex .

op _/_ : Complex Complex -> Complex .

vars X Y : Complex .

vars R1 R2 : Float .

eq realpart(complex(R1,R2)) = R1 .

eq realpart(X + Y) = realpart(X) + realpart(Y) .

eq realpart(X - Y) = realpart(X) - realpart(Y) .

eq realpart(X * Y) = realpart(X) * realpart(Y) - imagpart(X) * imagpart(Y) .

ceq realpart(X / Y) = (realpart(X) * realpart(Y) + imagpart(X) * imagpart(Y)) / (realpart(Y) ^ 2.0 + imagpart(Y) ^ 2.0) if realpart(Y) =/= 0.0 and imagpart(Y) =/= 0.0 .  

eq imagpart(complex(R1,R2)) = R2 .

eq imagpart(X + Y) = imagpart(X) + imagpart(Y) .

eq imagpart(X - Y) = imagpart(X) - imagpart(Y) .

eq imagpart(X * Y) = imagpart(X) * realpart(Y) + realpart(X) * imagpart(Y) .

ceq imagpart(X / Y) = (imagpart(X) * realpart(Y) - realpart(X) * imagpart(Y)) / (realpart(Y) ^ 2.0 + imagpart(Y) ^ 2.0) if realpart(Y) =/= 0.0 and imagpart(Y) =/= 0.0 .

eq X + Y = complex(realpart(X + Y),imagpart(X + Y)) .

eq X - Y = complex(realpart(X - Y),imagpart(X - Y)) .

eq X * Y = complex(realpart(X * Y),imagpart(X * Y)) .

eq X / Y = complex(realpart(X / Y),imagpart(X / Y)) .

endfm

The parsing works but when I try something like "red complex(2.0,1.0) + complex(3.0,1.0)", Maude crashes. Can I please get an answer of what I'm doing wrong?

Thanks!

_______________________________________________
Maude-help mailing list
Maude-help AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/maude-help