Maude-help mailing list

[Razvan Diaconescu <Razvan.Diaconescu AT ymail.com>]

Dear Friends,

Consider the following Maude program (the comments explain what it does).
I do not understand why when running both search and rewrite on the same 
example, although the number of rewrites is about ther same, the former runs 
about 20 times faster than the latter. Somehow I thought the opposite, that
in principle rewrite is always faster than search.

I apologise if the question may be a bit stupid, but my knowledge of the 
Maude engine is very low. 

Thanks,
Razvan

==========================================

--- ------------------------------------------
--- counts the number of the sub-sequences 123
--- in the sequence of all digits obtained by
--- concatenating all numbers from 1 to 2016
--- ------------------------------------------


--- generates the list of the numbers from m to n

mod LIST-OF-NUMBERS-FROM-TILL is 
  protecting LIST{Nat} .
  op from_till_ : Nat Nat -> List{Nat} .
  vars n m : Nat .
  ceq from m till n = m (from (m + 1) till n) if m <= n .
  ceq from m till n = nil                   if n < m .
endm

--- concatenates the numbers of a list of numbers
--- then builds the list of digits of the obtained number

mod SEQUENCE-OF-DIGITS is
  protecting LIST-OF-NUMBERS-FROM-TILL .
  var n : Nat .
  var L : List{Nat} .
  op sequence-of-digits : List{Nat} -> List{Nat} .
  eq sequence-of-digits(nil) = nil .
  ceq sequence-of-digits(n L) = (n sequence-of-digits(L))
    if  n < 10 .
  ceq sequence-of-digits(n L) =
      sequence-of-digits((n quo 10) (n rem 10) sequence-of-digits(L))
    if 10 <= n .
endm

***(
reduce in SEQUENCE-OF-DIGITS : sequence-of-digits(from 1 till 2016) .
)

--- the main program, by traversing a list of digits

mod SEQUENCE123-TRAVERSE is
  protecting SEQUENCE-OF-DIGITS .
  sort Config .
  op <_|_|_> : List{Nat} List{Nat} Nat -> Config .
  vars L L' : List{Nat} .
  vars m n k c : Nat .
  rl < nil | (n L) | c > => <     n | L | c > .
  rl < m   | (n L) | c > => < (m n) | L | c > .
  rl  < (1 2) | (3 L) | c > => < (2 3) | L | c + 1 > .
  crl < (m n) | (k L) | c > => < (n k) | L | c     >
    if k =/= 3 or m =/= 1 or n =/= 2 .
endm

***(
search in SEQUENCE123-TRAVERSE :
  < nil | sequence-of-digits(from 1 till 2016) | 0 > =>*
  <   L | nil                                  | c > .
rewrite in SEQUENCE123-TRAVERSE :
  < nil | sequence-of-digits(from 1 till 2016) | 0 > .
)