Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha110a/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

This is a bug fix release to fix a critical bug in ACU unification, illustrated by this example from Stephen Skeirik:

set include BOOL off .

fmod NAT-ACU is
    sorts Nat NzNat .
    subsorts NzNat < Nat .
    op 0 : -> Nat [ctor] .
    op 1 : -> NzNat [ctor] .
    op _+_ : NzNat NzNat -> NzNat [ctor assoc comm id: 0] .
    op _+_ : Nat Nat -> Nat [ctor assoc comm id: 0] .
    var n : Nat . var p : NzNat .
endfm

fmod NAT-ACU-PAIR is protecting NAT-ACU .
    sorts Pair .
    op p : Nat Nat -> Pair [ctor] .
endfm

*** missing unifier
unify p(1 + y:Nat, y:Nat) =? p(1, 0) .

I introduced the bug in alpha108 when I optimized the conversion of Maude variables to Diophantine variables. Here y:Nat gets bound to a ground term and so it is abstracted by Diophantine variable that must have a nonzero assignment, on the assumption that y:Nat can't be bound to the identity element since otherwise it would have already been canceled (there was even a comment to this effect). But in fact the code that did the canceling did not handle variables bound to the identity element specially. Variables that are bound to other in-theory terms don't need special treatment since they are always unsolved and added to the Diophantine problem to avoid termination issues.

Steven