Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha111a/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

This is a bug fix release that tidies up some corner cases
in variant narrowing and unification.

Bug fixes
==========

(1) A bug in the handling of irreducibility constraints in the new narrowing
descent function that produces a crash:

mod XOR is
  sorts Elt Expr .
  subsort Elt < Expr .
  ops a b c d e : -> Elt .
  op _+_ : Expr Expr -> Expr [assoc comm] .
  op 0 : -> Elt .

vars W X Y Z : Expr .
  eq Y + 0 = Y [variant] .
  eq X + X = 0 [variant] .
  eq X + X + Y = Y [variant] .
endm

mod XOR-TEST is inc XOR .
  ops g h : Expr -> Expr .
  op f : Expr Expr -> Expr .

vars W X Y Z : Expr .
  rl g(Y + a) => h(Y) [label nar] .
endm

red in META-LEVEL :
  metaNarrowingApply(
    ['XOR-TEST],
    'f['g['_+_['#2:Expr, 'b.Elt]], '#1:Expr],
    'nar,
    '_+_['#1:Expr, 'b.Elt],
    '#,
    0) .

What happens is that because '#1:Expr does not occur in the narrowing redex,
'g['_+_['#2:Expr, 'b.Elt]], it isn't part of the variants generated during
variant unification, and thus doesn't get a binding in the variant unifier.
Normally this wouldn't be a problem because the variant unfication code
just ignores '#1:Expr, but here because '#1:Expr occurs in an irreducibility
constraints, the variant unification code is aware of it.


(2) Another bug in the handling of irreducibility constraints in the new
narrowing descent function that ignores the irreducibility constraints if
a renaming takes place. This example uses the same modules:

*** the irreducibility constraint rules out solutions where
*** W contains 0 or b
variant unify W + b =? Y + a such that W + b irreducible .

but

red in META-LEVEL :
  metaNarrowingApply(
    ['XOR-TEST],
    'g['_+_['W:Expr, 'b.Elt]],
    'nar,
    '_+_['W:Expr, 'b.Elt],
    '#,
    3) .

returns

result NarrowingResult: {'h['%1:Expr],'Expr,
        'W:Expr <- '_+_['a.Elt,'b.Elt,'%1:Expr],
        'Y:Expr <- '%1:Expr,
[],'%}

where the binding for 'W:Expr contains 'b.Elt and thus '_+_['W:Expr, 'b.Elt]
is reducible by
  eq X + X = 0 [variant] .

This happens becaust the variables in the irreducibility constraints are not
being renamed with along with those in the term being reduced (renaming
is required because 'W:Expr is not a '# variable).


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

(1) Extra information is kept when a renaming takes place, so the original
context can be reconstructed. Thus the context passed back in metaNarrowingApply()
is now expressed in the original variables, with no instantiation:

red in META-LEVEL :
  metaNarrowingApply(
    ['XOR-TEST],
    'f['g['_+_['W:Expr, 'b.Elt]], 'Z:Expr],
    'nar,
    '_+_['W:Expr, 'b.Elt],
    '#,
    0) .

using the modules above now gives:

result NarrowingResult: {'f['h['_+_['b.Elt,'@1:Expr]],'@2:Expr],'Expr,
        'W:Expr <- '_+_['a.Elt,'@1:Expr] ; 
        'Z:Expr <- '@2:Expr,
        'Y:Expr <- '_+_['b.Elt,'@1:Expr],
'f[[],'Z:Expr],'@}

Here the context is 'f[[],'Z:Expr], and 'Z:Expr appears neither renamed nor
instantiated, even though if you trace you will see that the narrowing actually
happens on a term with # variables.

set trace on .
set trace whole on .

red in META-LEVEL :
  metaNarrowingApply(
    ['XOR-TEST],
    'f['g['_+_['W:Expr, 'b.Elt]], 'Z:Expr],
    'nar,
    '_+_['W:Expr, 'b.Elt],
    '#,
    0) .

*********** narrowing step
rl g(a + Y:Expr) => h(Y:Expr) [label nar] .
Rule variable bindings:
Y:Expr --> b + @1:Expr
Subject variable bindings:
#1:Expr --> a + @1:Expr
#2:Expr --> @2:Expr
Old: f(g(b + #1:Expr), #2:Expr)
g(b + #1:Expr)
--->
h(b + @1:Expr)
New: f(h(b + @1:Expr), @2:Expr)

Here 'W:Expr was renamed to #1:Expr and 'Z:Expr was renamed to #2:Expr
prior to narrowing step to avoid any potential variable name clashes with
rules in the module, but the context was translated back to the original
variables before being lifted to the metalevel.

(2) Variables that only occur in irreducibility constraints have to meet
the same safety requirements as variables in the term or unification
problem being variant narrowed, for old descent functions; for example:

red in META-LEVEL : metaVariantDisjointUnify(['XOR],
    '_+_['W:Expr, 'b.Elt] =? '_+_['Y:Expr, 'a.Elt],
    '_+_['#1:Expr, 'b.Elt],
    0, 0) .

Warning: unsafe variable name #1:Expr in irreducibility constraint.
rewrites: 2 in 4ms cpu (0ms real) (500 rewrites/second)
result UnificationTriple?: (noUnifier).UnificationTriple?
Maude> 

Here the second to last argument says we won't use fresh variables (from
any family) with indices greater than 0, but '#1:Expr occurring only in
an irreducibility constraint violates this.

Finally, note that  variables in irreducibility constraint for
metaVariantDisjointUnify() can only refer to variables in the lhs of the
unification problem since variables in the rhs are invisibly renamed to
obtain the disjointness. This has been true since metaVariantDisjointUnify()
was introduced in alpha96a but not documented.

Steven