Maude-help mailing list

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

There is an ambiguity in Maude about what it the length of a rewrite sequence 
to a given final term - in general there could many infinitely many such 
sequences, each of a different length. One choice would be to admit a 
solution if there is *any* sequence to it of an appropriate length - this is 
reasonable in theory but might be expensive in practice. Currently Maude uses 
the length of the shortest sequence - easy to find since search is currently 
breadthfirst - however this might change in the future.

Steven

On Monday 10 July 2006 19:18, Jittisak Senachak wrote:
> I wrote two specifications as below and, then, applied rewrite, frewrite
> and search commands to a starting term "a". Two results from
> rewrite/frewrite seem to be reasonable, but I don't understand the
> result from search one.
>
> fmod TEST is
> sort Test1 .
> op a : -> Test1 .
> op b : -> Test1 .
> op c : -> Test1 .
> op d : -> Test1 .
> endfm
>
> mod TEST2 is
> inc TEST .
> rl a => b .
> rl b => a .
> endm
>
> rew in TEST2 : a . *** INFINITY LOOP
> frew in TEST2 : a . *** INFINITY LOOP
> search in TEST2 : a =>+ a . *** No Solutions (2 rewrites applied)