Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha96/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

Bug fixes
--------

(1) A bug in narrowing where binding from a unifier were used in eager places without
copying within the context of the subterm being narrowed, and thus vunerable to
subsequent in-place rewriting. This shows up in a number of situations. One is
where unification generates a unifier where a subterms is shared between an
eager and lazy place, and then gets evaluated without being copied:

mod BUG1 is
  sort Foo .
  ops a b c : -> Foo .
  ops f g : Foo Foo Foo -> Foo .
  op l : Foo -> Foo  [strat (0)]

vars A X Y Z : Foo .

   rl f(A, A, A) => c .
   eq a = b .
endm

narrow g(f(l(a), l(X),  Y), X, Y) =>+ Z .

Here the a in l(a) should not be evaluated. The unification at f binds X to a and Y to l(a) but
the a is shared. This bindings are then used to instantiate X and Y in the context of f, both
of which are in eager positions. When the binding of X is evaluated to b the binding of Y
from l(a) to l(b) due to sharing.

A nastier case arises when a variable in the subterm being narrowed is bound to a
reducible ground term from the rule being used for narrowing and this variable then
appears in an eager position in the context of the subterm being narrowed.

mod BUG2 is
  sort Foo .
  ops a b c : -> Foo .
  ops f g : Foo Foo -> Foo .

vars X Y Z : Foo .

   rl f(a, b) => c .
   eq a = b .
endm

narrow f(b, Y) =>+ Z .
*** fails as expected

narrow g(f(X, Y), X) =>+ Z .
*** X binds to a from the rule and reduces it to b

narrow f(b, Y) =>+ Z .
*** succeeds because we have corrupted the dag representation of the rule


(2) A bug in narrowing where abstraction variables introduced for matching purposes confuse
unification:

mod FOO is
  sort Foo .
  ops a b c d e : -> Foo .
  op 1f : -> Foo .
  op f : Foo Foo -> Foo [assoc comm id: 1f] .
  op g : Foo Foo -> Foo [assoc comm] .

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

rew g(a, b, c) .

nar g(A, B, C) =>+ X .


(3) A bug in the pretty printing of equations where the (unlikely) combination of nonexec and
owise attributes didn't print correctly:

fmod FOO is
  sort Foo .
  ops a b : -> Foo .
  eq a = b [nonexec owise] .
endfm

show eqs .


(4) A bug in narrowing where fresh variables introduced by unification for one step of narrowing
could clash with fresh variables introduced unification for subsequent steps. This can be observed
here:

mod FOO is
  sort Foo .
  ops a b c d e : -> [Foo] .
  ops f g : Foo Foo ~> Foo [assoc comm] .
  op r : Foo Foo ~> Foo  .
  op k : Foo ~> Foo .

  
vars X Y Z A B C : [Foo] .
  rl k(f(X, Y)) => k(g(X, Y)) .
  rl k(g(X, Y)) => k(r(X, Y)) .

endm

narrow k(f(A, B)) =>* C .

Only 17 solutions are found at the kind level (because fresh variables are always kind variables) whereas
at the sort level, 19 solutions are found:

mod FOO is
  sort Foo .
  ops a b c d e : -> Foo .
  ops f g : Foo Foo -> Foo [assoc comm] .
  op r : Foo Foo -> Foo  .
  op k : Foo -> Foo .

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

endm

narrow k(f(A, B)) =>* C .

This now handled by the expediant of using larger numbers in fresh variables introduced by unification
and then renumbering all free variables after the unification is complete, to avoid growth in
variable numbers as narrowing proceeds. Unfortunately this changes the order in which fresh variable names
are created globally, which can lead to a counter-intuitive ordering on variables in unification problems.


New feature
----------
The main reason for this new release it to allow users to experiment with a very tentative implementation of
variant narrowing.

Equations that are to be used for variant narrowing take a variant attribute. It causes the equation to be
compiled in an inefficent way (for normalization), in order that it can be used for narrowing.
Variants are  generated by the get variants command. Here is an example supplied by Santiago:

fmod XOR is
  sort XOR .

  sort Elem .
  ops 1 2 3 4 : -> Elem .

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

  var X : XOR . var Y : XOR .

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

endfm

get variants Z:XOR * Z:XOR .

get variants in XOR : X:XOR * Y:XOR .

For various technical reasons variant generation is non-incremental; this may change in the future. During
normalization, all equations (and built-in equational semantics) are used, but for narrowing and reducibility
tests, only equations with the variant attribute are considered.

Variant generation is reflected at the metalevel by a new descent function.

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

while variants are formed using the ctor:

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

Here the first Nat in the descent function and the final Nat in the Variant are used to control the numbering
of fresh variables, using the same scheme as for unification. The second Nat in the descent function is
used to determine which variant is returned, although as explained above, variant generation itself is
non-incremental.

Steven