Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha94/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

This is an alpha release to allow Maude abusers to try out a partial
implementation of ACU unification.

Bug fixes
---------
(1) Hash consing wasn't being used for model checking.

(2) An empty sort declaration can cause show module command to crash:

mod T is sort  . endm
show mod .

Bug reported by Traian.

(3) A bug where one or more op->op mappings preceeding an op->term
mapping could get ignored in the translation of an operator with
resulting mayhem. Since operators from parameters cannot be renamed
and operators from parameters are replaced rather than translated by a
view, this can only happen by generating the op->op mapping from a
theory-view:

fth T1 is
  sorts Foo .
  op f : Foo -> Foo .
endfth

fmod P{X :: T1} is
  sort Bar{X} .
  op k : X$Foo -> Bar{X} .
  op j : X$Foo -> Bar{X} .

  eq k(X:X$Foo) = j(f(X:X$Foo)) .
endfm

fth T2 is
  sorts Foo .
  op g : Foo -> Foo .
endfth

view TV from T1 to T2 is
  op f to g .
endv

fmod DO is
  sort Do .
  op d : Do -> Do .
endfm

view V from T2 to DO is
  sort Foo to Do .
  op g(X:Foo) to term d(d(X:Do)) .
endv

fmod TEST is
  inc P{TV}{V} .
endfm

show all .

Here the instance of f in P, comes from T1 and must first be mapped by
TV and then by V to make  P{TV}{V}. TV does an op->op mapping which is
lost by the op->term mapping in V.

(4) A bug in upView() where the global from and to modules rather than
the locally created from and to modules used to parse op->term
mappings were being used in the term->metaterm conversion with
resulting chaos:

fth TEST8 is
 sorts Foo Faa .
 op update : Foo -> Faa .
endfth

view V2 from TEST8 to BOOL is
 sort Foo to Bool .
 sort Faa to Bool .
 
 op update(X:Foo) to term _or_(true, X:Bool) .
endv

red in META-LEVEL : upView('V2) .

Bug reported by : Adrian Riesco <ariesco@fdi.ucm.es>

(5) A potential bug in the unification scheme where dag nodes created
during unification could be garbage collected due rewriting taking
place between the generation of two unifiers. This can only happen at
the metalevel.

New feature
------------
There is a partial implementation of ACU unification. There is a
restricted elementary ACU unification algorithm and all implemented
unification algorithms are collapse-aware. The combination algorithm
is based on Boudet93.

The missing pieces are:

(1) No attempt is made to break compound cycles; they are treated as
occur check failures and unifiers can be missed. For example:

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

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

fails to find any unifiers.

(2) No attempt is made to find order-sorted unifiers that are not
instances of unsorted unifiers. For example:

fmod FOO is
  sorts Small Big .
  subsort Small < Big .
  op 1 : -> Big .
  op f : Small Small -> Small [assoc comm id: 1] .
  op f : Big Big -> Big [assoc comm id: 1] .

  var A : Small .
  vars X Y : Big .
endfm

unify A =? f(X, Y) .

only finds one order-sorted unifier.

The current restricted elementary ACU algorithm is very naive. While
it often finds unifiers quickly, it can spend a doubly-exponential
amount of time and a large amount of space to check that no more are
possible. I have some ideas for a smarter algorithm but I would like
some resource intensive examples to benchmark.

Steven