Maude-help mailing list

[Mandy Martin <tesleft AT hotmail.com>]

Hi  Francisco,

i fix  it  now.  

op _--_ : Poly{R, X} Poly{R, X} -> Poly{R, X} [assoc] .

I  discover this  definition can  not be commutative.

Regards,

Martin Lee

---

From: tesleft AT hotmail.com
To: duran AT lcc.uma.es
Date: Sun, 14 Jun 2015 05:00:26 +0800
CC: maude-help AT cs.uiuc.edu
Subject: [Maude-help] why sign of two terms exchanged in minus case

Hi  Francisco,

i  discover that it miss  minus  definition, i add  back  minus  definition, 

but it reverse  sign  of  two  terms make   3 x^5 -1 x^5  become  1 x^5-3  x^5 

expect  2*x^5  ,  but  it  return  -2*x^5

Maude> red in QID-RAT-POLY : ((3) ('X ^ 2) ('X ^ 3)) -- ((1) ('X ^ 5)) .

Warning: <standard input>, line 82: ambiguous term, two parses are:

(3 ('X ^ 2) 'X ^ 3) -- (1 'X ^ 5)

-versus-

(3 ('X ^ 2) 'X ^ 3) -- (1 'X ^ 5)

Arbitrarily taking the first as correct.

reduce in QID-RAT-POLY : (1 'X ^ 5) -- (3 ('X ^ 2) 'X ^ 3) .

rewrites: 5 in 0ms cpu (0ms real) (~ rewrites/second)

result Poly{RingToRat,Qid}: -2 'X ^ 5

fth RING is  

    sort Ring .  

    ops z e : -> Ring .  

    op _+_ : Ring Ring -> Ring [assoc comm id: z] .

    op _-_ : Ring Ring -> Ring [assoc comm id: z] .    

    op _*_ : Ring Ring -> Ring [assoc comm id: e] .  

    op -_ : Ring -> Ring .  

    vars A B C : Ring .  

    eq A + (- A) = z [nonexec] .  

    eq A * (B + C) = (A * B) + (A * C) [nonexec] .

    eq A * (B - C) = (A * B) - (A * C) [nonexec] .    

endfth

fmod MONOMIAL{X :: TRIV} is  

    protecting NAT .

    sorts Pow{X} Mon{X} .  

    subsorts Pow{X} < Mon{X} .  

    *** multiplication  

    op __ : Mon{X} Mon{X} -> Mon{X} [assoc comm] .  

    op _^_ : X$Elt NzNat -> Pow{X} .  

    var  X : X$Elt .  

    vars N M : NzNat .  

    eq (X ^ N) (X ^ M) = X ^ (N + M) .  

endfm

fmod POLYNOMIAL{R :: RING, X :: TRIV} is  

    protecting MONOMIAL{X} .  

    sorts Poly{R, X} .  

    subsorts R$Ring < Poly{R, X} .  

    *** multiplication  

    op __ : Poly{R, X} Poly{R, X} -> Poly{R, X} [assoc comm] .  

    *** addition  

    op _++_ : Poly{R, X} Poly{R, X} -> Poly{R, X} [assoc comm] .  

    op _--_ : Poly{R, X} Poly{R, X} -> Poly{R, X} [assoc comm] .

    op --_ : Poly{R, X} -> Poly{R, X} . 

    op __ : R$Ring Mon{X} -> Poly{R, X} .  

 

    vars A B : R$Ring .  

    vars U V : Mon{X} .  

    vars P Q R : Poly{R, X} .  

    eq P ++ z = P .  

    eq P ++ (-- P) = z .  

    eq P e = P .  

    eq -- (P ++ Q) = (-- P) ++ (-- Q) .  

    eq -- (A U) = (- A) U .  

    eq P (Q ++ R) = (P Q) ++ (P R) .

    eq P (Q -- R) = (P Q) -- (P R) .    

    eq z U = z .  

    eq z P = z .  

    eq A (B U) = (A B) U .  

    eq (A U) ++ (B U) = (A ++ B) U .

    eq (A U) -- (B U) = (A -- B) U .    

    eq (A U) (B V) = (A B) (U V) .  

    eq A B = A * B .  

    eq A ++ B = A + B .

    eq A -- B = A - B .    

endfm

view RingToRat from RING to RAT is  

  sort Ring to Rat .  

  op e to term 1 .  

  op z to 0 .  

endv

fmod RAT-POLY{X :: TRIV} is  

  protecting POLYNOMIAL{RingToRat, X} .  

endfm

fmod QID-RAT-POLY is  

  pr RAT-POLY{Qid} .  

endfm

Regards,

Martin Lee

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