Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha89/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

This is a pure alpha release and so I have not bothered with a FreeBSD
binary. At the moment I can't build a Intel Darwin binary because of a
problem with our Intel Mac server.

Bug fixes
==========
(1) The unification code doesn't look for another unsorted solution if
the current unsorted solution fails to have at least one sorted
solution; provoked by:

fmod COMM is
  sorts Foo Bar Baz .
  subsort Foo < Bar .
  op g : Baz -> Bar .
  op h : Baz -> Foo .
  op f : Bar Bar -> Bar [comm] .
endfm

unify f(X:Foo, Y:Bar) =? f(g(A:Baz), h(B:Baz)) .

(2) The unification code can lose track of smaller unification
problems generated in highly nested examples and produce
non-unifiers; provoked by:

fmod COMM2 is
  sort Foo .
  ops a b c d : -> Foo .
  op f : Foo Foo -> Foo [comm] .
  op g : Foo Foo -> Foo .
  vars W X Y Z A B C D E F : Foo .
endfm

unify
g(f(g(X, Y), W),
  f(g(X, Y), Z))
=?
g(f(g(f(A, B), f(C, D)), E),
  f(g(f(a, b), f(c, d)), F))
.

Here

Solution 1
W --> #1:Foo
X --> f(#2:Foo, #3:Foo)
Y --> f(#4:Foo, #5:Foo)
Z --> #6:Foo
E --> #1:Foo
A --> #2:Foo
B --> #3:Foo
C --> #4:Foo
D --> #5:Foo
F --> #6:Foo

is not a unifier.

(3) Files on the command line were ignored if the -no-prelude flag was
given. Bug reported by Christiano Braga <cbraga@fdi.ucm.es>.

New feature
============
Unification modulo AC is supported. Because of concerns about
termination, I have converted all the unification algorithms to use
"dag solved form" and do a topological sort and instantiation
postprocessing phase to extract actual unifiers and detect occurs
failure. Some examples:

fmod AC+C is
  sort Elt Set .
  subsort Elt < Set .
  ops a b c d e z : -> Elt .
  op f : Set Set -> Set [assoc comm] .
  op g : Set Set -> Set [comm] .
  vars U V W X Y Z : Set .
  vars A B C D E F : Elt .
endfm

unify f(g(X, Y), g(X, Z), U) =? f(g(Y, Z), V) .

unify g(f(X, Y), f(X, U, Z)) =? g(f(U, V), f(W, A)) .

reduce in META-LEVEL :
metaUnify(['AC+C],
'g['f['X:Set, 'Y:Set], 'f['X:Set, 'U:Set, 'Z:Set]],
'g['f['U:Set, 'V:Set], 'f['W:Set, 'A:Elt]],
0) .

From Lincoln & Christian 1994:

fmod AC-BENCH is
  sort Foo .
  ops a b c d e  : -> Foo .
  op __ : Foo Foo -> Foo [assoc comm] .
  vars T U V W X Y Z : Foo .
endfm

unify X a b =? U c d e .  *** 2 solutions
unify X a b =? U c c d .  *** 2 solutions
unify X a b =? U c c c .  *** 2 solutions
unify X a b =? U V c d .  *** 12 solutions
unify X a b =? U V c c .  *** 12 solutions
unify X a b =? U V W c .  *** 30 solutions
unify X a b =? U V W T .  *** 56 solutions

unify X a a =? U c d e .  *** 2 solutions
unify X a a =? U c c d .  *** 2 solutions
unify X a a =? U c c c .  *** 2 solutions
unify X a a =? U V c d .  *** 8 solutions
unify X a a =? U V c c .  *** 8 solutions
unify X a a =? U V W c .  *** 18 solutions
unify X a a =? U V W T .  *** 32 solutions

unify X Y a =? U c d e .  *** 28 solutions
unify X Y a =? U c c d .  *** 20 solutions
unify X Y a =? U c c c .  *** 12 solutions
unify X Y a =? U V c d .  *** 88 solutions
unify X Y a =? U V c c .  *** 64 solutions
unify X Y a =? U V W c .  *** 204 solutions
unify X Y a =? U V W T .  *** 416 solutions

unify X Y Z =? U c d e .  *** 120 solutions
unify X Y Z =? U c c d .  *** 75 solutions
unify X Y Z =? U c c c .  *** 37 solutions
unify X Y Z =? U V c d .  *** 336 solutions
unify X Y Z =? U V c c .  *** 216 solutions
unify X Y Z =? U V W c .  *** 870 solutions
unify X Y Z =? U V W T .  *** 2161 solutions

As seen from these last examples, the growth in most general unifiers
is explosive. Furthermore, in the non-elementary case Maude can
generate redundant unifiers.

Steven