maude-help AT lists.cs.illinois.edu

Subject: Maude-help mailing list

List archive

Re: [Maude-help] how to use the traditional polynomials example in manual

From: Mandy Martin <tesleft AT hotmail.com>
To: Francisco Durán <duran AT lcc.uma.es>
Cc: "maude-help AT cs.uiuc.edu" <maude-help AT cs.uiuc.edu>
Subject: Re: [Maude-help] how to use the traditional polynomials example in manual
Date: Sat, 13 Jun 2015 06:53:56 +0800
Importance: Normal
List-archive: <http://lists.cs.uiuc.edu/pipermail/maude-help/>
List-id: <maude-help.cs.uiuc.edu>

Hi Francisco,

i tried many ways , no matter doing simple addition or polynomials, the code from manual got error

Maude> red in QID-RAT-POLY : '2 + '6 .

Warning: <standard input>, line 159: bad token +.

Warning: <standard input>, line 159: no parse for term.

Maude> red in QID-RAT-POLY : 2 + 6 .

Warning: <standard input>, line 160: bad token +.

Warning: <standard input>, line 160: no parse for term.

Maude> red in QID-RAT-POLY : 2 ++ 6 .

Warning: <standard input>, line 161: bad token ++.

Warning: <standard input>, line 161: no parse for term.

Warning: unusable view Qid while evaluating module instantiation RAT-POLY{Qid}.

Maude> red in QID-RAT-POLY : 'X ++ 'X .

Warning: <standard input>, line 153: bad token ++.

Warning: <standard input>, line 153: no parse for term.

Maude> red in QID-RAT-POLY : 'X + 'X .

Warning: <standard input>, line 154: bad token +.

Warning: <standard input>, line 154: no parse for term.

Maude> red in QID-RAT-POLY : 'A + 'A .

Warning: <standard input>, line 155: bad token +.

Warning: <standard input>, line 155: no parse for term.

Maude> red in QID-RAT-POLY : 'B + 'B .

Warning: <standard input>, line 156: bad token +.

Warning: <standard input>, line 156: no parse for term.

Maude> red in QID-RAT-POLY : 'B ++ 'B .

Warning: <standard input>, line 157: bad token ++.

Warning: <standard input>, line 157: no parse for term.

Maude> red in QID-RAT-POLY : 'A ++ 'A .

Warning: <standard input>, line 158: bad token ++.

Warning: <standard input>, line 158: no parse for term.

fmod NAT is

sorts Nat NzNat Zero .

subsorts Zero NzNat < Nat .

op 0 : -> Zero .

op s_ : Nat -> NzNat .

op p_ : NzNat -> Nat .

op _+_ : Nat Nat -> Nat [comm] .

op _*_ : Nat Nat -> Nat [comm] .

op _*_ : NzNat NzNat -> NzNat [comm] .

op _>_ : Nat Nat -> Bool .

op d : Nat Nat -> Nat [comm] .

op quot : Nat NzNat -> Nat .

op gcd : NzNat NzNat -> NzNat [comm] .

vars N M : Nat .

vars N' M' : NzNat .

eq p s N = N .

eq N + 0 = N .

eq (s N) + (s M) = s s (N + M) .

eq N * 0 = 0 .

eq (s N) * (s M) = s (N + (M + (N * M))) .

eq 0 > M = false .

eq N' > 0 = true .

eq s N > s M = N > M .

eq d(0, N) = N .

eq d(s N, s M) = d(N, M) .

ceq quot(N, M') = s quot(d(N, M'), M') if N > M' .

eq quot(M', M') = s 0 .

ceq quot(N, M') = 0 if M' > N .

eq gcd(N', N') = N' .

ceq gcd(N', M') = gcd(d(N', M'), M') if N' > M' .

endfm

fmod INT is

sorts Int NzInt .

protecting NAT .

subsort Nat < Int .

subsorts NzNat < NzInt < Int .

op -_ : Int -> Int .

op -_ : NzInt -> NzInt .

op _+_ : Int Int -> Int [comm] .

op _*_ : Int Int -> Int [comm] .

op _*_ : NzInt NzInt -> NzInt [comm] .

op quot : Int NzInt -> Int .

op gcd : NzInt NzInt -> NzNat [comm] .

vars I J : Int .

vars I' J' : NzInt .

vars N' M' : NzNat .

eq - - I = I .

eq - 0 = 0 .

eq I + 0 = I .

eq M' + (- M') = 0 .

ceq M' + (- N') = - d(N', M') if N' > M' .

ceq M' + (- N') = d(N', M') if M' > N' .

eq (- I) + (- J) = - (I + J) .

eq I * 0 = 0 .

eq I * (- J) = - (I * J) .

eq quot(0, I') = 0 .

eq quot(- I', J') = - quot(I', J') .

eq quot(I', - J') = - quot(I', J') .

eq gcd(- I', J') = gcd(I', J') .

endfm

fth TRIV is

sort Elt .

endfth

fth RING is

sort Ring .

ops z e : -> Ring .

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] .

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 RAT is

sorts Rat NzRat .

protecting INT .

subsort Int < Rat .

subsorts NzInt < NzRat < Rat .

op _/_ : Rat NzRat -> Rat .

op _/_ : NzRat NzRat -> NzRat .

op -_ : Rat -> Rat .

op -_ : NzRat -> NzRat .

op _+_ : Rat Rat -> Rat [comm] .

op _*_ : Rat Rat -> Rat [comm] .

op _*_ : NzRat NzRat -> NzRat [comm] .

vars I' J' : NzInt . vars R S : Rat .

vars R' S' : NzRat .

eq R / (R' / S') = (R * S') / R' .

eq (R / R') / S' = R / (R' * S') .

ceq J' / I'

= quot(J', gcd(J', I')) / quot(I', gcd(J', I'))

if gcd(J', I') > s 0 .

eq R / s 0 = R .

eq 0 / R' = 0 .

eq R / (- R') = (- R) / R' .

eq - (R / R') = (- R) / R' .

eq R + (S / R') = ((R * R') + S) / R' .

eq R * (S / R') = (R * S) / R' .

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} .

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 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 V) = (A B) (U V) .

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

view Qid from TRIV to QID is

sort Elt to Qid .

endv

fmod QID-RAT-POLY is

pr RAT-POLY{Qid} .

endfm

red in QID-RAT-POLY : 'X ++ 'X .

Regards,

Martin Lee

Subject: Re: [Maude-help] how to use the traditional polynomials example in manual
From: duran AT lcc.uma.es
Date: Fri, 12 Jun 2015 09:41:39 +0200
CC: maude-help AT cs.uiuc.edu
To: tesleft AT hotmail.com

Mandy,

What is X suppose to be? A variable? The only X I can see is the label of one of the parameters. The terms to be rewritten should be ground, but you can still use variables, but need to be in the module, or defined on the fly, something like X:Ring.

Cheers,

Paco

On 11/6/2015, at 20:51, Mandy Martin <tesleft AT hotmail.com> wrote:

Hi,

Maude> rew in MYPOLY : X + X . Warning: <standard input>, line 60: bad token X. Warning: <standard input>, line 60: no parse for term.

fth TRIV is 
 sort Elt .
endfth

fth RING is  
    sort Ring .  
    ops z e : -> Ring .  
    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] .  
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} .  
    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 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 V) = (A B) (U V) .  
    eq A B = A * B .  
    eq A ++ B = A + B .  
endfm

fmod MYPOLY is 
 inc POLYNOMIAL{RING, TRIV2PACKET} .
endfm

rew in MYPOLY : X + X

Regards,

Martin Lee

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

[Maude-help] how to simulate this natural numbers system, Mandy Martin, 06/10/2015
- Re: [Maude-help] how to simulate this natural numbers system, Mandy Martin, 06/10/2015
  - Re: [Maude-help] how to simulate this natural numbers system, Mandy Martin, 06/10/2015
    - [Maude-help] how to use the traditional polynomials example in manual, Mandy Martin, 06/11/2015
      - Re: [Maude-help] how to use the traditional polynomials example in manual, Francisco Durán, 06/12/2015
        
        Re: [Maude-help] how to use the traditional polynomials example in manual, Mandy Martin, 06/12/2015
        
        [Maude-help] how to use predicates.maude in Igor2.3 and how to get the result from Rewrite Result, Mandy Martin, 06/12/2015
        
        [Maude-help] bad token ^ when using default code in prelude.maude and redefine again, Mandy Martin, 06/14/2015
        
        Re: [Maude-help] how to use the traditional polynomials example in manual, Mandy Martin, 06/13/2015
        
        Re: [Maude-help] how to use the traditional polynomials example in manual, Mandy Martin, 06/13/2015
        [Maude-help] why minus result is wrong and how to return understandable result from haskell maude, Mandy Martin, 06/13/2015
        
        [Maude-help] why sign of two terms exchanged in minus case, Mandy Martin, 06/13/2015
        
        Re: [Maude-help] why sign of two terms exchanged in minus case, Mandy Martin, 06/13/2015