Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha108/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

The is an alpha quality release, mainly to allow experimentation with a new associative unification
implementation. Note that the Darwin version doesn't support rewriting modulo SMT (see below).

Bug fixes
=======

(1) A bug were metaGetIrredundantVariant() can generate garbage variants. For example:

fmod CI-SEMIGROUP is
sort Elt .
op f : Elt Elt -> Elt [assoc comm] .

vars A B C D E U V W X Y Z : Elt .

eq f(X, X) = X [variant] .
endfm

get irredundant variants f(A, B, A) .

produces:

rewrites: 2 in 0ms cpu (0ms real) (~ rewrites/second)

Variant #1
Elt: f(#1:Elt, #2:Elt)
A --> #1:Elt
B --> #2:Elt

Variant #2
Elt: %1:Elt
A --> %1:Elt
B --> %1:Elt

No more variants.

while

reduce in META-LEVEL : metaGetIrredundantVariant(['CI-SEMIGROUP], 'f['A:Elt, 'B:Elt, 'A:Elt], empty, 0, 1) .

produces:

rewrites: 2 in 0ms cpu (0ms real) (~ rewrites/second)
result Variant: {'%1:Elt,
'A:Elt <- '%1:Elt,1}

with no assignment to 'B:Elt. This was because the irredudant flag was being passed as
the unification mode argument and the variant generation code was trying to do variant
unification on something that wasn't a unification problem.

(2) A bug where variant narrowing (and unification) at a collapse redex could apply a
variant equation belonging to the wrong kind resulting in an internal error when the
BDD based sort computations were done. Provoked by the following example:

fmod FOO is
sorts Foo Bar Quux .
subsort Foo < Bar .
op 1 : -> Foo .
op f : Bar Bar -> Bar [assoc comm id: 1] .

op g : Bar -> Quux .
op a : -> Quux .
eq g(A:Foo) = a [variant] .
endfm

get variants f(X:Bar, Y:Bar) .

Reported by Jose.

New features
=========

(1) A new associative unification algorithm based on a modified PIG-PUG (aka Plotkin's algorithm).
Systems of pure associative equations are solved one at a time with forward (bindings from
a solved equation percolate into later equations) and backwards (bindings from a solved
equation percolate into solutions to previously solved equations) substitution.

There is now partial support for nonlinear variables and in the future more cases will be handled.
My hope is that this is currently complete in two cases (but I'm no where near being able to prove
this, even in the abstract, because of the complexities of combining algorithms):

(a) All nonlinear variables are confined to one side of the problem; OR

(b) No nonlinear variable occurs directly under an associative symbol nor indirectly under
an associative symbol via collapse.

Note that variables that are element variables for the associative symbol they occur under
(i.e. their sort is too low to take an expression headed by the associative symbol) don't count
as nonlinear as long as they don't have an occurrence under an associative symbol for
which they are not element variables.

I would be interested to know of any examples falling into cases (a) or (b) where Maude reports
incompleteness.

(2) The unification infrastructure now supports the notion of incomplete unification algorithms.
This has two major components. Firstly the algorithm for combining unification algorithms
now prioritizes theories that have complete algorithms and amongst those, prioritizes
theories that are expected to have fewer partial solutions. The idea of this heuristic is to
minimize branching and when an unification problem with an incomplete unification algorithm
has to be solved, to have more information on shared variables (ideally they would be bound
to terms in collapse-free theories), in order to minimize the likelihood of encountering
an incomplete case.

Secondly, when incompleteness does occur it is tracked though the various users of
unification so that appropriate warnings (and at the metalevel, meta-warnings) can be issued.

This idea is extended to variant narrowing and variant unification. One issue not addressed here
whether incomplete unification algorithms, as well as losing variants, might change the
termination properties of variant narrowing since the lost variants might have subsumed
later variants.

Consider the example of bands (idempotent semigroups):

fmod BAND is
sort Elt .
op f : Elt Elt -> Elt [assoc] .

vars A B C D E U V W X Y Z : Elt .

eq f(X, X) = X [variant] .
endfm

Here
get variants f(A, B) .
works because the unification problems formed have nonlinearity on one side only and the new
associative unification algorithm can handle them. But
get variants f(A, B, A) .
gives a warning each time a unification problem that can't be completely solved is encountered
and a warning after the last variant to say the list of variants may be incomplete.
Likewise
variant unify f(A, B) =? f(C, D) .
works but
variant unify f(A, B, A) =? f(C, D) .
generates gives warnings.

Support for incomplete unification algorithms has been omitted from the old narrowing code
since this code will hopefully soon be replaced by a more principled notion of narrowing.

Theses changes are reflected at the metalevel with 3 new constants.

metaUnify() and metaVariantUnify() use:
op noUnifierIncomplete : -> UnificationPair? [ctor] .
to indicate that there are no more unifiers but unifiers may have been missed.

metaDisjointUnify() and metaVariantDisjointUnify() use:
op noUnifierIncomplete : -> UnificationTriple? [ctor] .
to indicate that there are no more unifiers but unifiers may have been missed.

metaGetVariant() and metaGetIrredundantVariant() use:
op noVariantIncomplete : -> Variant? [ctor] .
to indicate that there are not more variant but variants may have been missed.

Other changes
==========

Apple (as of Mavericks) has withdrawn support for gcc and a critical library (rope) that
Maude depends on is broken with clang. Currently I have an ugly work around that allows
Maude to compile under clang but that is incompatible with CVC4 because of its very complex
dependencies. Consequently the Darwin version of Maude has rewriting modulo SMT disabled.

Steven