Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha89c/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

These is very much an experimental release to allow the protocol
analysis folks to try out new unification features that they
requested.

Bug fix
========
Matching with extension in the iter theory allowed matches against
alien subterms with all the iter operators going into the
extension. Provoked by

xmatch in NAT : X:Nat <=? 1 .

Changes
========
(1) There is now a very crude implementation of unification with
extension. The idea is similar to matching with extension in that as
well as unifying the whole of the righthand side r = f(t1,...,tn) with
the lefthand side, if there are subterms s of members of [r]_E that
are not (possibly improper) subterms of some member of some [tk]_E then
unifying these subterms against the lefthand side is also tried.

For example

fmod AC is
  sort Foo .
  ops a b c d e z : -> Foo .
  op f : Foo Foo -> Foo [assoc comm] .
  op g : Foo Foo -> Foo .
  vars W X Y Z A B C D E F : Foo .
endfm

unify f(X, Y) =? f(A, B, C) . *** no extension - 25 solutions
xunify f(X, Y) =? f(A, B, C) .  *** extension - 46 solutions

There are two major limitations with the current implementation:

(a) Only the AC theory is supported; even though the iter theory
is supported for regular unification, the extension case is not yet
done. So for example:

xunify in NAT : s X:Nat =? 7 .

fails with a not implemented warning though

xmatch in NAT :  s X:Nat <=? 7 .

works.

(b) No support for a bare variable as the lefthand side when unifying
with extension. So for example:

xunify in AC : X =? f(a, b, c, d) .

fails with a not implemented warning though

xmatch in AC : X <=? f(a, b, c, d) .

works.

There is no conceptual difficulty in implementing these missing cases
- it just requires significant code.

(2) The metalevel interface to unification is redesigned from scratch.
There is a descent function

  op metaUnify : Module UnificationProblem Nat Nat ~> UnificationPair? [...] .

That takes a module, a unification problem, a variable index and a
solution number and returns a unfication pair.

Unification problems are built from the following signature which
allows for simultaneous unification:

  sorts UnificandPair UnificationProblem .
  subsort UnificandPair < UnificationProblem .
  op _=?_ : Term Term -> UnificandPair [ctor prec 71] .
  op _/\_ : UnificationProblem UnificationProblem -> UnificationProblem [ctor assoc comm prec 73] .

Unification pairs are made from the following constructor:

  op {_,_} : Substitution Nat -> UnificationPair [ctor] .

where the second argument is a variable index. The idea of passing
variable indices is to allow fresh variables introduced by a
unification to be used in subsequent unification problems without
confusion and to give some control over the names chosen for fresh
variables. Fresh variable names have the form '#n:Sort where n is the
index. The rule is that the variable index i passed in the unification
problem must be >= than largest variable index encountered in the
problem. Fresh variables will then be given indices >= i+1. The
variable index in the result is the largest index belonging to a fresh
variable, or i if no fresh variables were introduced to form the
unifier. There is a

  op noUnifier : -> UnificationPair? [ctor] .

for the case of failure.

There is also a descent function

  op metaDisjointUnify : Module UnificationProblem Nat Nat ~> UnificationTriple? [...] .

which takes the same arguments but returns a unification triple made
from the constructor:

  op {_,_,_} : Substitution Substitution Nat -> UnificationTriple [ctor] .

Here variables occuring in the righthand side(s) of a (potentially
simultaneous) unification problem are renamed before unification takes
place and then have their names restored and have their assignments
placed in a second substitution when the results are returned. The
idea behind disjoint unification is then when checking for critical
pairs or performing narrowing, any occurrence of some variable on both
sides of a unification problem is accidental and Maude can keep track
of the necessary renamings to avoid such accidents at almost zero
cost. There is a

  op noUnifier : -> UnificationTriple? [ctor] .

for the case of failure.

Unification with extension is reflected by 

 op metaXunify : Module Term Term Nat Nat ~> UnificationContextTriple?

and

 op metaDisjointXunify : Module Term Term Nat Nat ~> UnificationContext4Tuple?

These just take a pair of terms rather than a potential conjunction of
unification problems. Their return types includes a context to indicate
what part of the righthand side term has actually been unified. But
otherwise they are completely analogous to the two nonextension unification
functions.

(3) Parsing of file names in the commands load, in, cd and pushd now
allows spaces using either of two syntactic conventions:

If the file name starts with " then all following characters will be
taken literally up to the terminating ", line feed or form 
feed.

If a file name starts with other than ", the following escape
  sequences are recognized
  \\	      becomes \
  \<space>    becomes <space>
  \"	      becomes "

Change requested by Paco.

Steven