Maude-help mailing list

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

Actually the effects of memo are rather more complicated.

First off you are just doing ground rewriting (your equations have no 
variables). In fact your patterns consist of free constants. What you 
really need is hash consing however, Maude does not provide that for 
equational rewriting because the expected cost is greater than the 
expected benefit form more normal rewriting systems.

If you apply the memo attribute to your constants then the second time 
Maude comes to rewrite the constant, it will find the result from fully 
rewriting it the first time, and partly share it. The reason it only 
partly shares the previous result, is that is uses in-place replacement, 
and the top symbol from the previous result must be copied to overwrite 
the symbol being rewritten. Ironically the rationale for in-place 
replacement, is sharing of unevaluated subterms - when such a subterm is 
evaluated, all terms which have a pointer to the original see the 
replacement, because it is done in-place.

However if you consider the cost of the extra copied node to be 
amortized with the cost of the pointer, I believe memo on every symbol 
that appears as a top symbol in the left hand side will prevent 
exponential blow up in your case. It's still not as good as hash consing 
since it won't get cases where two identical subterms are generated by 
two different rewrites.

Steven

On 3/16/12 9:35 AM, Marc Boyer wrote:
> Le 16/03/2012 13:48, Iago Abal a écrit :
> > 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.
> I am not sure to fully understand your needs, but, did you consider
> the memo attribute ? It does not save space bu save time. You can also
> consider the evaluation strategy ?
>
> Regards,
>      Marc Boyer