Maude-help mailing list

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

Hi,

I don't know of any symbolic computation systems of the kind you want
written in Maude 2 - the system has only been out a month. However it
should not be hard to convert your existing TRS to Maude.

Here are a few hints:

For simplifying expressions it is useful to define expressions as a
sort above the builtin arithmetic so that rewrite rules can use the
sort system to distinguish between, say, rational numbers and rational
expressions; for example you might want to distribute over expressions
but gather like terms when only the coefficients differ. Here is a
simple TRS for polynomials with rational coefficients:

fmod SIMPLIFY is
  protecting RAT .
  sort RatExp .
  subsort Rat < RatExp .

*** extend  builtin operators to rational expressions
  op -_ : RatExp -> RatExp [ditto] .
  op _+_ : RatExp RatExp -> RatExp [ditto] .
  op _-_ : RatExp RatExp -> RatExp [ditto] .
  op _*_ : RatExp RatExp -> RatExp [ditto] .
 
  vars P Q R : Rat .
  vars E F G : RatExp .

*** binary minus is a defined operator
  eq E - F = E + - F .

*** collapse axioms
  eq E + 0 = E .
  eq E * 1 = E .
  eq E * 0 = 0 .
  eq E * -1 = - E .
  eq - - E = E .
  eq E + - E = 0 .

*** do arithmetic when we can
  eq P * E + E = (P + 1) * E .
  eq P * E + - E = (P - 1) * E .
  eq P * E + Q * E = (P + Q) * E .
  eq -(P * G) = - P * G .

*** distribute (push + outwards) when we can't do arithmetic
  ceq E * (F + G) = E * F + E * G if not(F :: Rat and G :: Rat) .
  ceq -(F + G) = - F + - G if not(F :: Rat and G :: Rat) .

*** push - outwards when we can't do arithmetic
  ceq - F * G = -(F * G) if not(F :: Rat) .
endfm

red (E - 1) * (E + 1) .
red (E - F) * (E + F) .
red E * (4 + 3 * (G + F)) - (E - 1) * (E + 1) .
red (E * (4 + 3 * (G + F)) - (E - 1) * (E + 1)) *
(E * (4 + 3 * (G + F)) - 3 * F * (E + 1)) .

red 2 * X:RatExp + X:RatExp .

Substitution is really a higher order operation and it is painful to
do at the object level since Maude is a first order language -
essentially you would end up giving a rule for traversing each
operator. The usual way of handling this in Maude is to go to the
metalevel. One problem with the metalevel is that there is currectly
no syntactic sugar to hide the zero-successor represention of numbers
so -3 becomes the metarepresentation of - s_^3(0) or
'-_['s_^2['0.Nat]]

Substitution might be defined thus:

fmod SUBSTITUTE is
  protecting META-TERM .
  op _[_/_] : TermList Term Variable -> TermList .

vars T R : Term .
var V V' : Variable .
var C : Constant .
var F : Qid .
var TL : TermList .

  eq C[R / V] = C .
  eq V'[R / V] = if V' == V then R else V' fi .
  eq (F[TL]) [R / V] = F[ TL[R / V] ] .
  eq (T, TL) [R / V] = T[R / V], TL[R / V] .
endfm

red
'_+_['_*_['s_^2['0.Nat], 'X:RatExp, 'X:RatExp],
     'Y:RatExp,
     's_['0.Nat]] ['_+_['Z:RatExp, 's_^3['0.Nat]] / 'X:RatExp]
.

Of course you can combine meta and object level computations via the
descent functions:

fmod COMBINE is
  protecting META-LEVEL .
  protecting SUBSTITUTE . 
endfm

red metaReduce(['SIMPLIFY], 
'_+_['_*_['s_^2['0.Nat], 'X:RatExp, 'X:RatExp],
     'Y:RatExp,
     's_['0.Nat]] ['_+_['Z:RatExp, 's_^3['0.Nat]] / 'X:RatExp]
) .

This first does the substitution at the metalevel and then calls
metaReduce() to do the simplification of the resulting term at the
object level.

Best regards,

Steven Eker
http://www.csl.sri.com/people/eker/