Maude-help mailing list

[Jeff Thompson <jeff AT thefirst.org>]

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).