Maude-help mailing list

[Iago Abal <iago.abal AT gmail.com>]

Hi,

We have been working on a project whose purpose is to solve problems of this form:

  input i1, i2

  a = i1 + i2

  b = a + i1

  c = a * b

  output c 

Note that these programs are in SSA (static single assignment) form. In our first steps we have tried to use Maude to solve these problems by using a translation process illustrated next: 

  fmod EXAMPLE is

   sort S .

   ops _+_ _*_ : S S -> S .

   ops i1 i2 : -> S .

   ops a b c : -> S .

   eq a = i1 + i2 .

   eq b = a + i1 .

   eq c = a * b .

  endfm

  red c

Our problems often contain thousands of intermediate definitions, so it is crucial to share common subterms because otherwise computing the output of the program rises memory usage due to duplication of definitions. In the above example, during the reduction of c the equation «a = i1 + i2» is applied twice (no sharing), so Maude constructs the term «(i1+i2) * ((i1+i2)+i1)» containing two duplicated occurrences of «(i1+i2)». When this happens on a larger scale the result is a very high memory consumption.

   c 

   -> a * b                            [ c = a * b ]

   -> (i1+i2) * b                   [ a = i1 + i2 ]

   -> (i1+i2) * (a+i1)           [ b = a + i1 ]

   -> (i1+i2) * ((i1+i2)+i1)  [ a = i1 + i2 ]

Given that our definitions are specified as Maude equations, in the above reduction there is no oportunity for sharing. Of course, ideally we would like Maude to provide a way to specify "definitions" ensuring perfect sharing of those definitions. Anyway, Maude could still be suitable for our purpose if it were able to exploit sharing when there is some opportunity during the reduction process as in

   c 

   -> a * b                            [ c = a * b ]

   -> a * (a+i1)                    [ b = a + i1 ]

   -> (i1+i2) * (a+i1)           [ a = i1 + i2 ]

   -> (i1+i2) * ((i1+i2)+i1)  [ a = i1 + i2 ]

Unfortunately, when reducing the term «a * (a+i1)» Maude is going to apply the equation «a = i1 + i2» twice, duplicating the definition of «a». Here we would need Maude to dynamically detect sharing opportunities, but as far as we know this is not possible. Due to this limitation we are considering implementing our own term-graph rewriting engine. 

We would appreciate any feedback about this problem, and any possible workaround that we could use to address it to some extent. The use of Full Maude to implement a custom Maude interpreter was presented as a possible alternative, but we ignore how complex and time consuming it could be to develop such interpreter and if it worths the effort.

Thanks in advance,

Iago Abal Rivas