Maude-help mailing list

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

Hi,

Formal specification and analysis sounds a little overkill to me. Basically 
optimization of search is a space vs time time trade off, once you decide 
what features you need (depthfirst/double depthfirst/breathfirst, incemental 
state generation, witness path recovery, shortest path recovery etc), since 
pretty much everything could be recomputed rather than stored (thus you get 
techniques such as bounded depthfirst search with iterative deepening).

Maude's current search mechanism is very general and keeps everything - 
included stuff that will never be used for search but just happens to reside 
in a class I reused. Which brings us to another trade off - implementation 
effort vs runtime. Highly optimized code is more time consuming (but fun!) to 
write and debug and is therefore only worthwhile for heavily used features.

Best regards,

Steven Eker

On Sunday 22 March 2009 10:38, Jeff Thompson wrote:
> 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
>
> _______________________________________________
> Maude-help mailing list
> Maude-help AT maude.cs.uiuc.edu
> http://maude.cs.uiuc.edu/cgi-bin/mailman/listinfo/maude-help