Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha106/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

This is an alpha quality release, to allow users to experiment with a
revised implementation of linear associative unification.

This version uses a number of transformations to linearize nonlinear
associative unification problems. This is principly useful for removing
nonlinearities that were introduced by the other theories for the
purpose purifying and expressing unifiers, when unifying in a
combination of theories.

Also nonlinear element variables (i.e. variables whose sort is too
low to take the associative symbol in question) are now fully handled.
Thus the algorithm can be compete for quite complex examples:

fmod A-UNIF is
  sorts List Elt .
  subsort Elt < List .
  op __ : List List -> List [assoc] .
  op f : List List -> List [assoc] .
  op g : List List -> List .
  op h : List List -> List [assoc comm] .
  op i : List -> List .
  op j : List List -> List [assoc comm id: 1] .
  op 1 : -> List .
  ops a b c d e : -> Elt .
  vars A B C D
       G H I J K L M N
       P Q R S T U V W X Y Z : List .
  vars E F : Elt .
endfm

unify A E B F C E D =? W F X E Y F Z .

unify j(A, f(B, E, C), f(D, E, j(G, H), I)) =? j(U, f(V, W), f(X, j(Y, Z), S)) .

I don't have a good description of the exact class of unification
problems handled. The current algorithm is a step along the path to
a much more sophisticated approach which I hope will have a concise
description.

The current algorithm has problems with variables under an associative
symbol f not being linear, unless they are of element sort for f or it can
determine in some other way that they cannot take a term f(...).

Another case that causes problems is more than 2 subterms f(...) being
unified against the same variable X unless one of the subterms has
all of its arguments as element variables, or collapse-free aliens.
This situation can arise indirectly from a non-linear problem passed
to the AC unification algorithm:

unify h(A, A, A) =? h(f(B, C), f(I, J), f(X, Y)) .

However if one of the f subterms satisfies the above conditions it works:

unify h(A, A, A) =? h(f(B, C), f(I, J), f(i(B), E)) .

My belief is that this algorithm is complete for linear unification in
combination with all the theories supported by Maude - however,
I'm punting on trying to prove this, as it should be easier to prove
for the next version.

When the algorithm does encounter a problematic variable, it
prints a warning about incompleteness and pretends the variable
is an element variable. It does not give the name of the variable,
because due to transformations, the variable that is detected
as causing the problem, might be linear in the original problem
or might not even occur in the original problem.

I'm very interested to hear from Maude Abusers who are using
associative unification in anger, whether the new algorithm is
works on examples of practical interest that couldn't be handled by
the previous version, and especially, where it prints an
incompleteness warning on examples of practical interest. 

Steven