Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha110/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

This version is close to what we are intending to release as Maude 2.7.1 once
the documentation is updated.

Bug fixes
==========

Three related bugs where terms were being converted to DAGs for SMT rewriting
without their hash values being filled in - at the object level, at
the metalevel and in the SMT condition. This results in uninitialized
memory reads which are probably benign since if the hash values are bad
all that happens is we fail to combine common subterms.

Changes
========

(1) The handling of non-strict-left-linear associative unification equations is
more sophisticated. Previously such a problem would be made strict-left-linear
by turning some unrestricted variables into element variables, potentially losing
unifiers in the process, and flagging incompleteness. We illustrate the
new implementation with the following module:

fmod FOO is
  sorts Elt Foo .
  subsort Elt < Foo .
  op __ : Foo Foo -> Foo [assoc] .

*** free constants
  ops a b c d e f g h i j : -> Elt .

*** element variables
  vars E F G H I J K L M N : Elt .

*** unconstrained variables
  vars P Q R S T U V W X Y Z : Foo .
endfm

The new approach is to use the general PIG-PUG (aka Plotkin) procedure which
is complete, but non-terminating, and force termination using one of two
techniques:

(a) If no unrestricted variable occurs more than twice in the equation, the
states generated by PIG-PUG cannot get bigger and hence the state-space is
finite. The well known method of PIG-PUG + cycle detection is used.
Several outcomes are possible:

(i) No cycles are seen; there are either no unifiers or finitely many unifiers.

*** no unifiers
unify X X =? Y a Y .
unify X X =? E Y a b Y E .

*** 1 unifier
unify X X =? Y Y .
unify X X =? Y a Y a .
unify X X =? E Y F E Y F .
unify X X =? E Y a b Y F .
unify X X =? E Y F b Y E .
unify X X =? E Y b b Y E .

(ii) Cycles are seen but all paths exiting a cycle lead to failure; so far the
only examples I've found exhibiting this behavior require either element variables
or free constants. For example:

*** no unifiers
unify P P =? Q Q R R H .
unify P P Q =? Q R H R .
unify a Q =? Q c .
unify P P =? Q Q c d .

*** 1 unifier
unify P Q R R =? H H Q I I .
unify P Q c S =? e Q c f g .

(iii) Cycles are seen and there is a successful path exiting at least one cycle;
there is an infinite family of unifiers. In practice the cycles are often compound
and the set of sequences of PIG-PUG steps that generate a unifier form a regular language.
In this case, since I have no way to combine or return such infinite sets of
unifiers, the algorithm will flag incompleteness and just return the acyclic solutions.
For example:

*** incomplete
unify X Y =? Y X .
unify X Y X =? Z Z .
unify X X =? Y a a Y .

(b) If there are non-linear unrestricted variables on both sides of the equation and at least
such one variable occurs more than twice, a depth bound is imposed, and if any branches
of the search hit it, incompleteness is flagged.

*** 1 unifier
unify X X =? Y Y Y .
unify X Y X =? Y X Y .
unify X X X =? Y Y Y Y .
unify X Y X =? Y Y Y Y .

*** incomplete
unify X Y X =? Z Z Z Z .
unify X Y X =? Y Y Z Y .
unify X Y X =? Y Z Z Y .
unify X X X =? Y Y Z Y .
unify X X Z =? Y Y Z Y .
unify X Y Z =? Y Y Z Y .

If verbose mode is switched on:
  set verbose on.
then a message is printed when either cycle detection or a depth bound is used and
another message is printed when a live cycle is found or a depth bound it hit.

The situation with simultaneous associative unification is more complicated. As
before each equation is solved on its own with forward and backwards substitution
to solve the system. Non-strict-left-linear equations are only solved after all
strict-left-linear equation have been solved. Currently the heuristic of preferring
equations with disjoints sets of unrestricted variables on the lhs and rhs is
used. This enables the following example to return a unique identifier, regardless
of the order in which the equations are presented:

unify X Y =? Y X  /\ X X X =? Y Y Y Y .
unify X X X =? Y Y Y Y  /\ X Y =? Y X .

Here X Y =? Y X has an infinite family of most general unifiers,
X --> #1^n, Y --> #1^m, for n, m relatively prime but X X X =? Y Y Y Y
only has a single unifier that makes X Y =? Y X an identity after substitution.

In more general problems with symbols from other theories, the outcome
is harder to predict. As before, associative subproblems are solved
as late as possible, with aliens subterms headed by collapse free symbols
being treated almost like constants and aliens subterms headed by a
collapse symbol being abstracted by an unrestricted variable.

(2) The way unification sort computations are done is now minizes the use
of less efficient calls to BuDDy. Also the central unification code has
been reorganized to make the regular and narrowing unification classes
congruent to each other and avoid unnecessary work. Quantify shows that
unification is now about 15% faster on Jose's finite variant examples.
I'm interested to know whether there is a noticeable performance improvement
on real word problems.

(3) There is a new command line flag:
  -print-to-stderr flag
that causes the output of the print attribute to be set to stderr rather than
stdout. Added at Carolyn's request.

Steven