On compilation of Maude specifications.

[Massimo Dentico]

Apparently, looking through Maude sources and documentation, Alexis Read
was  right  wrt  the  existence of  an  experimental  compiler  of Maude
specifications but via a C/C++  compiler, not directly to machine  code.
Evidence of this in the source is, for example, this file:

  Maude2.0/FullCompiler/compilationContext.cc
  
Also mentioned in the Maude 2.0 Manual - v. 1.0. An excerpt from p. 8:

  - http://maude.cs.uiuc.edu/manual/

--------------------------------------------------------------------------
  1.1.3 Performance
  
  [..]
  
  These figures must be qualified by the observation that, until recently,
  the cost  of an  associative or  associative-commutative rewriting  step
  depended polynomially  on the  size of  the subject  term, even with the
  most efficient  algorithms. In  practice this  meant that  this kind  of
  rewriting was not practical for  large applications, in which the  lists
  or  multisets to  be rewritten  would have  millions of  elements.  This
  situation has been drastically altered by a recent result of Steven Eker
  [28]   providing  new   algorithms  for   associative  and   associative
  -commutative  rewriting  that,  for  patterns  typically  encountered in
  practice,  can perform  one step  of associative  rewriting in  constant
  time,   and   one  associative-commutative   rewriting   step  in   time
  proportional to  the logarithm  of the  subject term's  size. Maude  2.0
  supports equational rewriting with these new algorithms. The reason  why
  the  Maude interpreter  achieves high  performance is  that the  rewrite
  rules are carefully  analyzed and are  then semicompiled into  efficient
  matching  and   replacement  automata   [27]  with   efficient  matching
  algorithms. One  important advantage  of semicompilation  is that  it is
  possible to trace  every single rewriting  step. More performance  is of
  course possible by full compilation. Maude has an experimental  compiler
  for a  subset of  the language  which can  typically achieve  a fivefold
  speedup over the interpreter.
  
  [..]
--------------------------------------------------------------------------


Bibliographic references in the excerpt:

--------------------------------------------------------------------------
  [27] Steven Eker.  Fast matching  in combination  of regular  equational
       theories. In  J. Meseguer,  editor, Proc.  First Intl.  Workshop on
       Rewriting Logic and its Applications, volume 4 of Electronic  Notes
       in Theoretical Computer Science. Elsevier, 1996.
  
    - http://maude.cs.uiuc.edu/papers/abstract/tcs4007.html
  
  [28] Steven Eker. Associative-commutative  rewriting on large  terms. In
       Rewriting Techniques  and Applications  (RTA'03), Lecture  Notes in
       Computer Science, to appear. Springer-Verlag, 2003.
  
    - http://www.dsic.upv.es/~rdp03/rta/abstracts.html#rta13
--------------------------------------------------------------------------

I think that [28] will  never be available on-line because  of copyright
restrictions, so we need to wait until a technical report or  equivalent
will be written.

>From what I understand [27] explain the compilation from rewriting rules
(simplified  with the  technique in  [28]?) to  Binary Decision  Diagram
(BDD).

Unfortunately right now I'm  quite busy with a  job and I have  not much
time to  devote to  Maude. If  someonelse is  examining Maude source and
docs I will be glad to hear his discoveries.

Best regards.

--
Massimo Dentico