Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha94a/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

This is a pure alpha release.

Bug fixes
---------
(1) An bug where downTerm was not checking the kind of the downed term
and would return a object level term in the wrong kind. Illustrated by
this example from Andrei Stefanescu <andreistef@gmail.com>:

mod TEST is inc META-LEVEL .
  sort S1 S2 .
  op o1 : -> S1 .
  op o2 : -> S2 .
endm

red downTerm(upTerm(o1), o2) .

(2) A bug where the Qid code in the metalevel was stripping leading `
characters from the special character tokens
  `( `) `[ `]  `{ `} `,
leading to problems when these were used in meta operator
declarations. Illustrated by this example from Traian:

mod T is sort S . ops a , : -> S . eq `, = a . endm
reduce in META-LEVEL : wellFormed(upModule('T, false)) .

(3) In a related fix,
  [ ]  { } ,
can now be used unbackquoted in mixfix syntax:

mod T is sort S . ops a , : -> S . eq , = a . endm
red , .

and the printed mixfix syntax of , is , rather than `, :
parse `, .

Note that there is still an issue with metaParse() in that the Qid '`,
is needed to represent the token , and therefore cannot represent the
token `,

Perhaps allowing special characters as operator names was a bad idea
from the outset.


Improvements to unification
----------------------------
(1) I've replaced the brute force restricted ACU unification algorithm
with a novel one based on a BDD encoding of sets of Diophantine basis
elements that satisfy certain constraints; this seems to avoid a lot
of wasted time persuing fruitless branches of the search; compare with
alpha94 on the following example: 

fmod TEST is
  sort Foo .
  ops 1f a b c : -> Foo .
  op g : Foo Foo -> Foo .
  op h : Foo -> Foo .
  op f  : Foo Foo -> Foo [assoc comm id: 1f] .
  vars A B C X Y Z : Foo .
endfm

unify g(
f(X, X, Y, Y, h(Z)),
f(X, Y, Y, Z, Z)
) =? g(
f(A, A, A, B, C),
f(A, B, B, h(C))
) .

(2) The AC/ACU unification code now does eager variable
replacement. This optimization can reduce the number of redundant
unifiers; compare with alpha94 on the following example:

fmod FOO is
  sort Foo .
  op f : Foo Foo -> Foo [assoc comm] .

  vars W X Y Z : Foo .
endfm

unify X =? W /\ f(X, Y) =? f(W, Z) .

(3) I've replaced the Dershowitz-Journard90 MM-algorithm style
unification algorithms for the free, S and C theories and variable
handling with algorithms that are closer in spirit to the Boudet93
scheme.

In particular, the variable code now only handles binding of variables
to variables. Binding of variables to nonvariable terms is now done
by the nonvariable terms theory which also does purification and a
local occurs check. Previously the occurs check was completely
postponed and termination was achieved using the MM-algorithms
nonvariable size measure during a merge step mediated by the variable
handling code.

I made this change partly because I was uneasy combining algorithms
that used differenct termination assumptions (it not clear to me the
the combination always terminates, though I couldn't find a
counterexample), and partly because the purification of terms in an
almost (apart from coumpound cycles) solved form turn out to be
critical for compound cycle breaking.

(4) I've implemented compound cycle breaking via restricted
unification but not via the Boudet93 variable elimination
technique. It seems that variable elimination is only needed for
completeness when non-regular theories such a cancellation law are
present.

The problem of computing a complete set of E-eliminators is quite
subtle and will need to be addressed if we ever want to support
non-regular theories either as built-in or via metalevel unification
algorithm interface.

One suble point is the Boudet93 requires that the function symbols
from the theories to be combined are disjoint. This is not true for
identities that are not a simple constant. Nevertheless compound cycle
breaking via restricted unification can resolve some quite subtle
situations as long as all the nonvariable terms on a compound cycle
are pure (which is guarenteed by the new unification algorithms):

fmod NAT' is
  protecting BOOL .
  sorts Zero NzNat Nat .
  subsort Zero NzNat < Nat .
  op 0 : -> Zero .
  op s_ : Nat -> NzNat [iter] .
  op _*_ : NzNat NzNat -> NzNat [assoc comm id: s(0) prec 31] .
  op _*_ : Nat Nat -> Nat [ditto] .

  vars W X Y Z A B C D : Nat .
endfm

unify X =? s (X * Y) .
unify X =? s X * Y .

fmod COMM is
  sort Foo .
  ops a b c d : -> Foo .
  op f : Foo Foo -> Foo [assoc comm id: c(a, b)] .
  op c : Foo Foo -> Foo [comm] .
  vars W X Y Z A B C D : Foo .
endfm

unify X =? c(f(X, Y), Z) .

There are some instances where neither restricted unification nor
Boudet's variable elimination technique will break a breakable cycle
formed by the interdepency between two non-disjoint identity elements
or between a non-disjoint identity element and itself via some alien
symbol:

fmod FOO is
  sort Foo .
  ops a b c d : -> Foo .
  op f : Foo Foo -> Foo [assoc comm id: g(c, d)] .
  op g : Foo Foo -> Foo [assoc comm id: f(a, b)] .

  vars X Y : Foo .
endfm

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

Here f has an identity that depends on g which has an identity that
depends on f. In the unification problem, neither of the righthand
sides can collapse so restricted unification will not break the
cycle. Furthermore Boudet's variable elimination technique looks for
an assignment that will eliminate Y from f(Y, a, b) where Y is bound
to some other variable, which is not possible in this case.

fmod FOO is
  sort Foo .
  ops a b : -> Foo .
  op h : Foo -> Foo .
  op f : Foo Foo -> Foo [assoc comm id: h(f(a, b))] .

  vars X Y : Foo .
endfm

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

Here f has an identity that depends on itself and as before the
breakable cycle cannot be broken by the Boudet93 techniques.

In this release I've handled this situation by the ad hoc technique of
trying to unify variables on the cycle with the identity of the
function symbol they occur under. Since this can generate a host of
redundant unifiers, this is only tried if the identity looks
"sufficiently funky".

With these changes, unsorted ACU unification should be sound, complete
and terminating. Order-sorted ACU unification is still incomplete
because we allow signatures where ACU operators "collapse down" and
thus there can be order-sorted unifiers that aren't a sorted instance
of an unsorted unifier (see the alpha94 release notes for an
example). The immediate fix for this is to avoid such signatures. The
medium term fix is to build in Joe Hendrix's theory transformation;
but this has performance consequences if done in a naive way.

Talking of performance, there are many inefficiencies in the current
design that could potentially be fixed at the cost of effort and code
complexity. I would really like to have some large examples to
benchmark on before I start this, since it not obvious where the
bottlenecks really are.

I've added some harder unification examples to the test suite in
"unification2".

Steven