Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha88d/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

This is a pure alpha release to let maude abusers try out unification.

The unify command has the syntax:
  unify [<limit>] in <module> : <term> =? <term> .

As usual the
  [<limit>]
and
  in <module> :
parts are optional with unbounded and current module being assumed
respectively if they are omitted. Currently only the free theory is
supported. The use of operators from other theories such as iter,
assoc, comm etc and constants from non-algebraic data types such as
String, Float etc will cause the unification to fail ungracefully.

Because even in the free theory, order-sorted unification may required
the introduction of fresh variables, all unifiers are presented as
substitutions from the variables occurring in the problem to fresh
variables with base names #1, #2, #3 etc. Variables with these base
names should not occur in the original problem (this is not checked
for).

The calculation of sorts for the fresh variables is done by an
original BDD based algorithm with avoids the introduction of redundant
unifiers:

fmod TEST is
  sorts NzNat Nat .
  subsort NzNat < Nat .
  op _+_ : Nat Nat -> Nat .
  op _+_ : NzNat Nat -> NzNat .
  op _+_ : Nat NzNat -> NzNat .
  op 0 : -> Nat .
  op 1 : -> NzNat .
  op s : Nat -> NzNat .
  op f : Nat Nat -> Nat .
endfm

unify f(X:Nat + Y:Nat, B:NzNat) =? f(A:NzNat, Y:Nat + Z:Nat) .

yields:

Decision time: 1ms cpu (0ms real)

Solution 1
X:Nat --> #1:NzNat
Y:Nat --> #2:Nat
B:NzNat --> #2:Nat + #3:NzNat
A:NzNat --> #1:NzNat + #2:Nat
Z:Nat --> #3:NzNat

Solution 2
X:Nat --> #1:Nat
Y:Nat --> #2:NzNat
B:NzNat --> #2:NzNat + #3:Nat
A:NzNat --> #1:Nat + #2:NzNat
Z:Nat --> #3:Nat

The
  cont <limit> .
command (<limit> part optional) can be used to look for further
unifiers if the orginal command terminated early due to a limit.
The unify command is reflected by the descent function:

  op metaUnify : Module Term Term Nat ~> Substitution?
        [special (...)] .

As with metaMatch(), the last argument controls which solution is
returned and
  op noMatch : -> Substitution? [ctor] .
is returned if there are no further unifiers.

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

(1) The strategy language now has some optimizations. Stacks of
pending strategies are stored as a shared structure - essentially one
big persistent stack. Each task keeps track of the terms and pending
stacks that have been seen during the search for that task researching
from the the same state reached along different paths is thus
avoided. As a by-product this also avoids finding the same solution
multiple times.

(2) There is a new trace option to control the tracing of builtin
operators:

  set trace builtin on/off .

Steven