Maude-help mailing list

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

Hi Vlad,

This time I have to apologize for a very late reply - it looks like the 
maude-help mailing list hasn't been forwarding messages for several months. 
search uses the same approach as rewrite - after every rule execution the 
resulting term is fully reduced by equations - i.e. coherence is assumed. If 
you can't meet coherence then you need to convert some of your equations to 
rules sot that it is met.

Steven

On Monday 27 November 2006 23:11, 
rusu AT irisa.fr
 wrote:
>  I have another newbie question regarding "search" and "rewrite". The Maude
> manual says that "rewrite" works as follows: it first reduces according to
> equations, then applies a rewrite rule, then reduces the result with the
> equations, and so on; and that this process is correct, i.e., no terms are
> lost, under certain executability conditions. My question is: does "search"
> operate in the same way? That is, does it perform a breadth-first
> exploration of terms *reduced* modulo the equations, or just of the set of
> terms? The two are equivalent if the executability requirements are met, I
> guess, but I need to use "search" in a context where executability may not
> be satisfied a priori.
>
> Thanks,
>
>  Vlad
>
>
>
> _______________________________________________
> Maude-help mailing list
> Maude-help AT maude.cs.uiuc.edu
> http://maude.cs.uiuc.edu/cgi-bin/mailman/listinfo/maude-help