Maude-help mailing list

[rusu AT irisa.fr]

>On Sunday 19 November 2006 10:26, rusu at irisa.fr wrote:
>>  - there is a simple way to limit the depth of the search command
>>   (the argument in [] limits the number of solutions, not the depth?)
>
>Not in the current release. Maude 2.3 (due early december) will allow an 
>extra
>argument for this.
>
>>  - whether the "object/message fair rewriting" also applies to the
>>   search command, as it does to the rewrite command.
>
>No - object-message fair rewriting doesn't make sense for the search command
>as it explores all paths breadth-first. If instead you are only executing a
>single path, then you might want some fairness guarantees on that path which
>is what frewrite does.
>
>Steven

Steven,

Thanks for the quick answer.

 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