Maude-help mailing list

[Mandy Martin <tesleft AT hotmail.com>]

Hi  Francisco,

when run maude with red in QID-RAT-POLY : ('X ^ 2) ('X ^ 3) .

it is correct, but use haskell to run the result is non-understandable.

how to make it return a understand result which is X^5 ?

    martin@ubuntu:~/mal$ ghc -o a a.hs

    [1 of 1] Compiling Main             ( a.hs, a.o )

    Linking a ...

    martin@ubuntu:~/mal$ ./a

    RewriteResult {resultTerm = Term {termSort = "Pow`{Qid`}", termOp = "_^_", termChildren = [Term {termSort = "Qid", termOp = "'X", termChildren = []},IterTerm {termSort = "NzNat", termOp = "s_", termChildren = [Term {termSort = "Zero", termOp = "0", termChildren = []}], iterations = 5}]}, rewriteStatistics = MaudeStatistics {totalRewrites = 2, realTime = 0, cpuTime = 0}}

haskell code to run the X^2*X^3 , but above result is not understandable

    module Main where

    

    import Language.Maude.Exec

    import Data.Text

    

    addSpace xs = if Prelude.length xs <= 1

                  then xs

                  else Prelude.take 1 xs ++ " " ++ addSpace (Prelude.drop 1 xs)

    

    main :: IO Int

    main = do

      --print $ addSpace "2+3"

      print =<< rewrite ["man3.maude"] (pack "('X ^ 2) ('X ^ 3)")

Regards,

Martin Lee

---

From: tesleft AT hotmail.com
To: duran AT lcc.uma.es
Date: Sun, 14 Jun 2015 01:05:50 +0800
CC: maude-help AT cs.uiuc.edu
Subject: Re: [Maude-help] how to use the traditional polynomials example in manual

Hi  Francisco,

i succeed by  including  1  into  the equation,  now  it can do addition and  multiplication  of  monomials

but  i discover  that  it  got  wrong  answer  when  doing  minus.

do you know why  result in  this ?

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

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

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

-versus-

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

Arbitrarily taking the first as correct.

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

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

result Poly{RingToRat,Qid}: -6 'X ^ 10

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

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

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

result Poly{RingToRat,Qid}: -6 'X ^ 10

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

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

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

-versus-

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

Arbitrarily taking the first as correct.

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

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

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

Regards,

Martin Lee

---

From: tesleft AT hotmail.com
To: duran AT lcc.uma.es
Date: Sun, 14 Jun 2015 00:47:18 +0800
CC: maude-help AT cs.uiuc.edu
Subject: Re: [Maude-help] how to use the traditional polynomials example in manual

Hi  Francisco,

i know how  to  run this  code  now.  It  do not use  *  and use  space,  but  use  ++  got  error.

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

Warning: <standard input>, line 84: didn't expect token ++:

( ( 'X ^ 2 ) ( 'X ^ 3 ) ) ++ <---*HERE*

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

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

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

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

result Pow{Qid}: 'X ^ 5

Maude> 

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

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

red in QID-RAT-POLY : ('X ^ 2) ('X ^ 3) .

Regards,

Martin Lee

---

From: tesleft AT hotmail.com
To: duran AT lcc.uma.es
CC: 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

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 mailing list Maude-help AT cs.uiuc.edu http://lists.cs.uiuc.edu/mailman/listinfo/maude-help

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