Maude-help mailing list

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

On Monday 09 January 2006 05:29, Marc Boyer wrote:
> I am a new maude user. I was wondering if overloading and membership
> could do the same job, and if there is any pb with the assoc label.
>
> Let be the following code:
>  sort S .
>  op _ + _ : S S -> S [assoc comm ctor] .
>  sort S' .
>  subsort S' < S .
>
> What is the best solution ?
>   op _ + _ : S' S' -> S' [ditto] .
> or
>   vars x y : S' .
>   mb x + y : S' .
>
> I am wondering if the assoc property will be lost by the membership
> equation or not ?

Extra operator declarations have esssentially zero runtime cost while mbs and 
in particular cmbs can be very expensive since they end up being tried on 
every reduced subterm with the right top symbol.

Also non-uniform operator declarations do not work correctly with mbs on 
assoc 
and iter symbols - this is to avoid an exponential time consideration of all 
possible op declaration/mb interleavings.

So the bottom line is that mbs should be used only as a last resort.

Steven