Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha96c/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

Bug fixes
--------
(1) Two related bugs in the unification code. One is trigged when two variables are unified, one of which is
already bound:

fmod FOO is
  sort Foo .
  op f : Foo -> Foo .
  vars X Y Z : Foo .
endfm

unify X =? f(f(Y)) /\ Y =? X  /\ Y =? f(X) .

The problem is that X =? f(f(Y)) is considered a solved form X |-> f(f(Y)) in the free theory. Unifying Y =? X
notionally replaces Y with X (though in fact virtual variable replacement is done using chains of variables),
generating an occurs check failure local to the f-theory. Finally Y =? f(X) causes non-termination since the
free theory assumes it can solved problems sequentially leaving any solved forms such as X |-> f(f(Y))
undisturbed. The other is triggered when both variables are already bound:

unify X =? f(Y) /\ Y =? f(f(X)) /\  X =? Y .

Here the free theory considers both X |-> f(Y) /\ Y |-> f(f(X)) to be solved forms (and relies on the
inter-theory cycle detection to detect the cycle). But notionally replacing X with Y only un-solves X |-> f(Y)
while creating an occurs check failure in Y |-> f(f(X)). Solving the resulting f(f(X)) =? f(Y) loops forever
without every getting a complete set of solved forms to do inter-theory cycle detection on.

(2) A bug in the way AC is combined with the free theory:

fmod FOO is 
  sort Foo .
  op a : -> Foo .
  op f : Foo Foo -> Foo [assoc comm] .
  op g : Foo -> Foo .
vars A X Y : Foo .
endfm

unify  f(a, A) =? f(a, X) /\ f(a, Y) =? f(a, X)
/\     f(a, g(A)) =? f(a, g(X)) /\ f(a, g(Y)) =? f(a, g(X))
.

What is happening is that the second pair of unifications bind A |-> X and Y |-> X under the nose of the ACU
unification algorithm. Then X gets bound to a fresh variable, #3. Then f(a, Y) =? f(a, X) binds the current
representative of Y (#3) to the current representative of X (#3) forming a cycle in the substitution.
Finally f(a, A) = ? f(a, X) tries to bind the current representative of A to the current representative of X; but
finding the last variable in either chain leads to the infinite cycle #3 |-> #3.
In a related problem:

unify  f(a, Y) =? f(a, X)
/\     f(a, g(A)) =? f(a, g(X)) /\ f(a, g(Y)) =? f(a, g(X))
.

fails to find the single unifier.

(3) Another bug in the way AC is combined with other theories:

fmod FOO is 
  sort Foo .
  op a : -> Foo .
  op f : Foo Foo -> Foo [assoc comm] .
  op g : Foo -> Foo .
vars A B C D X Y Z : Foo .
endfm

unify  f(a, X) =? f(a, g(X)) /\ f(a, X) =? f(a, g(g(X))) .

Here the solution to the simultaneous AC unification results in X |-> g(g(X)) with the g(X) =? g(g(X)) problem still
to be resolved. But then the free theory cycles because of the occur check. The same bug show up in a slightly
more suble form with:

unify Y =? X /\ f(a, X) =? f(a, g(Y)) /\ f(a, X) =? f(a, g(g(Y))) .

(4) A performance bug provoked by

fmod FOO is
  sort Foo .
  op f : Foo Foo -> Foo [assoc comm] .
  ops a b c d e : -> Foo .
  vars W X Y Z : Foo .
endfm

unify  f(a, Y) =? f(a, X) .

where the AC unification algorithm creates a Diophantine variable for the subterm "a" even though it is eliminated
before the Diophantine basis is computed.

(5) A performance bug provoked by degenerate AC unification problem such as:

unify f(X, a) =? f(X, a) .
unify f(a, b) =? f(a, b) .
unify f(X, Y) =? f(X, Y) .

Here the test for degeneracy was incorrect and so Diophantine systems were being constructed and solved 
even though the subterms cancel.

(6) A bug in AC/ACU unification where the wrong substitution was being protected from garbage collection.

(7) A bug in loop mode where printing the empty Quoted Indentifier was causing an out-of-bound memory read. Found
while searching for the following bug, while running the Maude NPA.

(8) A critical bug in the compilation of variant equation left hand sides whose top symbol lies in the free theory.
These are compiled twice - once for checking variant reducibility and once as the part of the free theory
discrimination net for their free theory top symbol. Each compiler expects to recieve the pattern in pristine condition
but leaves some extra data behind in the pattern, resulting in bad compilation of the discrimination net and memory
corruption. Provoked by an example from Cathy.

New feature
----------
Unification is now supported in the CU, U, Ul and Ur theories.

Also the Mac version (including the statically linked libraries) is now compiled with the
  -mmacosx-version-min=10.5
flag, since Jose wasn't able to run alpha96b under Mac OS X 10.5.8 (Leopard). I don't have an old enough machine
to test this.

Steven