Maude-help mailing list

[Jeff Thompson <jeff AT thefirst.org>]

Thanks for the prompt and illuminating answer!  Would it be possible to write 
a Maude specification
of the search command such that questions like "What information does search have 
to preserve?" have
a formal answer, and such that optimizing the search command is a process of 
refinement within this
specification?

Steven Eker wrote:
> 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
>
>
>