Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha96a/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

Bug fixes
--------

(1) A bug where meta variants with a singleton substitution were not
being generated correctly; illustrated by the following example:

fmod XOR is
  sort XOR .

  sort Elem .
  ops cst1 cst2 cst3 cst4 : -> Elem .

  subsort Elem < XOR .
  op _+_ : XOR XOR -> XOR [ctor assoc comm] .
  op 0 : -> XOR .

  vars X Y : XOR .

  eq Y + 0 = Y [variant] .
  eq X + X = 0 [variant] .
  eq X + X + Y = Y [variant] .

endfm

fmod TEST is
  inc XOR .
  inc META-LEVEL .
endfm

red metaGenerateVariant(['XOR], upTerm(X:XOR + cst2), 0, 0) .

This bug was independently reported by Kyungmin Bae.

(2) A bug in narrowing caused by clashes between variables occuring in
rules and variables occuring in the term being narrowed.

mod FOO is
  sort Foo .
  ops a b c d e : -> Foo .
  ops f k : Foo Foo -> Foo  .
  op g : Foo -> Foo  .

vars W X Y Z A B C : Foo .
  rl f(X, g(Y)) => k(X, Y) .
endm

narrow f(X, X) =>+ Z .

Here the first arguments compare equal, and no constraint is imposed
on the the variable X in the rule. 

This is a symptom of a more general problem in the management of
variable names. In alpha96 I fixed bug (4) by using bigger numbers for
indices of variables occuring in unifiers, but this is not entirely
satisfactory.

In this version, I used the same approach for both narrowing and
variant narrowing.

The variables in the starting term are immediately renamed using #
variables before any reduction or narrowing happens. Then in narrowing
steps, the names of the variables generated alternate between % and #,
so in one step # variables get assigned values expressed over %
variables and in a successor step from that state, the % variables get
assigned values over # variables. This allows variables names to be
reused without escalating index numbers, but at the same time
the same variable name will never be used for two purposes in a
narrowing step. This also makes tracing look more sensible. The
downside is that % variables must now suffer the same restrictions as
# variables, and a given narrowing result might be expressed in #
variables or % variables, depending on whether the number of narrowing
steps was even or odd. Also with narrowing search, cycle detection is
less effective because there are # and % versions of each state, but
variable renaming was always the Achilles heel of narrowing search
cycle detection, and probably the way narrowing search actually works
should be redesigned in the future.

Other changes
------------

(1) Variant narrowing now supports irreducibility constraints with the
syntax:

get variants t such that t1, t2,..., tn irreducible .

Any variant whose substitution would cause one or more of t1,...,tn to
be reducible by a variable equation is discarded.

I've done quite a bit of optimization on variant generation - some
large examples are about twice as fast.

The reflection of variant narrowing has changed. The descent function
is now:

  op metaGetVariant : Module Term TermList Nat Nat ~> Variant? [...] .

where the TermList argument may be passed the constant "empty" if
there are no irreducibility constraints. The constructor for
meta-variants now has the term before the substitution:

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


(2) Variant unification is now supported. The syntax is:

variant unify u1 =? v1 /\ u2 =? v2 /\ ... /\ un =? vn
  such that t1, t2,..., tn irreducible .

The such that clause is optional and applies the same irreducibility
constaints during the variant search.

This is reflected by:

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

where the TermList argument may be passed the constant "empty" if
there are no irreducibility constraints. There is also a disjoint
unification version:

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

which treats the variables in the left hand sides as distinct from
those in the right hand sides, and returns pairs of substitutions.

Both object level commands take an optional "in <module> :" clause,
and both can be prefixed by "debug" to immediately enter the
debugger. This might be useful for single stepping since variant
narrowing and variant unification often blow up in unexpected ways.

The Darwin binary is now 64-bit; there is an ugly work around because
the rope implementation is broken on the current Darwin version of gcc
- see INSTALL if you want to compile your own binary on a Mac.

Steven