Maude-help mailing list

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

Hi,

You're right, the seach command is rather slow. Maude is highly optimized for 
equational rewriting, less so for rule rewriting while searching is not 
currently optimized at all.

Probably the biggest issue is the huge amount of information that is stored 
in 
each state. Some of this information is useful for model checking (the state 
generation code does double duty) and path generation (the show path command) 
but most of it exists just because I used existing classes that serve much 
more general roles in the interpreter rather that writing compact, custom 
ones.

This might change in the future (it's item 24 on a todo list that currently 
has 966 items and has been there since Oct 8, 2002 so don't hold your 
breath), but until then search is very memory hungry and spends most of its 
time in the memory management system.

Best regards,

Steven Eker

On Saturday 21 March 2009 14:01, Jeff Thompson wrote:
> Here is a simple search test that doesn't run as quickly as I would expect:
> mod TEST is
>    protecting INT .
>
>    vars X : Int .
>
>    op f : Int -> Int .
>    rl f(X) => X + 1 .
>    rl f(X) => X .
>
>    op sum : -> Int .
>    rl sum => f(f(f(f(f(f(f(f(f(f(f(f(0)))))))))))) .
> endm
>
> The rule "f" first rewrites X to X + 1, then to X.  The rule "sum" sums
> over all possible combinations.
>
> Maude> search in TEST : sum =>* 0 .
>
> This search looks for the one solution where all "f" just return the
> initial 0. If "sum" has N of "f", this searches through 2^N solutions.  In
> this case, 212 = 4096 solutions.
>
> A search space of 4096 is not very large, but it takes Maude more than one
> second to search it (on my 1.3 GHz Pentium).
> The same tests in Curry and Prolog (below) return right away, and can
> search a much larger space within one second.
>
> Am I using Maude correctly to do this kind of a search?
>
> Thanks,
> - Jeff (new Maude user)
>
> The same test in Curry:
> f X = X + 1
> f X = X
> sum = f(f(f(f(f(f(f(f(f(f(f(f(0))))))))))))
>
> search term: sum =:= 0
>
> The same test in Prolog:
> f(X, Y) :- Y is X + 1.
> f(X, Y) :- Y is X.
> sum(X) :- f(0,  X1), f(X1, X2), f(X2, X3), f(X3, X4), f(X4, X5),
>         f(X5, X6), f(X6, X7), f(X7, X8), f(X8, X9), f(X9, X10),
>         f(X10, X11), f(X11, X).
>
> search term: sum(0).
>
> _______________________________________________
> Maude-help mailing list
> Maude-help AT maude.cs.uiuc.edu
> http://maude.cs.uiuc.edu/cgi-bin/mailman/listinfo/maude-help