Dear Maude Abusers,

A new alpha release can be accessed at SRI-CSL in:

~eker/public_html/Maude/Alpha91c/

or downloaded from:

http://www.csl.sri.com/~eker/Maude/Alpha91c/

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

This adds an optimization for AC/ACU matching with extension for a
case reported in practice by  "Nishant Sinha" <nishants@nec-labs.com>

Consider:

fmod FOO is
  sort Foo .
  ops a b c d e a1 b1 c1 d1 e1 a2 b2 c2 d2 e2 1 : -> Foo .
  ops a3 b3 c3 d3 e3 a4 b4 c4 d4 e4 : -> Foo .
  op f : Foo Foo -> Foo [assoc comm] .
  op f' : Foo Foo -> Foo [assoc comm id: 1] .
  ops g h : Foo -> Foo .
  vars X Y Z : Foo .
endfm

xmatch f(X, g(f(X, Y))) <=?
f(
  a,
  g(f(b, c, d, e, a1, b1, c1, d1, e1,  a2, b2, c2, d2, e2,
      a3, b3, c3, d3, e3, a4, b4, c4, d4, e4))
) .

Here Maude91b would examine all 2^n - 2 solutions to the inner AC
matching problem even though X must take a from the outer AC matching
problem. This situation is now special cased and the unique binding to
X from the outer AC matching problem takes place immediately causing
the inner one to fail without examining the exponentially many
alternatives.

In fact a couple of slightly more general situations can be handled:

xmatch f(X, g(f(X, Y)), h(Z)) <=?
f(
  a,
  g(f(b, c, d, e,    a1, b1, c1, d1, e1,  a2, b2, c2, d2, e2,
      a3, b3, c3, d3, e3,  a4, b4, c4, d4, e4)),
  h(a)
) .

Here, having an extra subpattern that can only match one thing in the
subject has no effect on the forced binding of X to a.

xmatch f'(X, g(f'(X, Y))) <=?
f'(
  a,
  g(f'(b, c, d, e,    a1, b1, c1, d1, e1,  a2, b2, c2, d2, e2,
      a3, b3, c3, d3, e3,  a4, b4, c4, d4, e4))
) .

Here, even though X could take 1, this is not allowed since it would
cause a collapse "out of theory" and the binding of X to a is still
forced.

However the following case cannot be handled efficiently using the new
optimization:

xmatch f'(X, g(f'(X, Y)), h(Z)) <=?
f'(
  a,
  g(f'(b, c, d, e,    a1, b1, c1, d1, e1,  a2, b2, c2, d2, e2,
      a3, b3, c3, d3, e3,  a4, b4, c4, d4, e4)),
  h(a)
) .

Here X can take either 1 or a and in fact there is a solution with
X |-> 1
It might seem that this case could be handled by examining the
possibilities for the outer AC matching problem first, but of course
with a slight rearrangement the exponential branching could be moved
to the outer AC matching problem.

Steven