Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha88f/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

This version reports itself as Maude 2.3 and is a 2.3 release
candidate to go with the forthcoming Maude book.

There are binaries for PowerPC/Darwin, x86/Darwin, x86/Linux,
x86-64/Linux and x86/FreeBSD.

Bug fixes
==========
(1) A bug in the instantiation code that can lead to incorrect
unifiers or BDD errors. Provoked by:

fmod BUG is
  sort Foo .
  ops a b : -> Foo .
  op f : Foo Foo -> Foo .
  op g : Foo Foo Foo -> Foo .
  vars W X Y Z : Foo .
endfm

*** X gets the wrong binding
unify g(X, Y, Z) =? g(f(Y, Z), a, b) .

*** BDD error
unify g(X, Y, Z) =? g(f(Y, Z), W, b) .

(2) A bug in the sort calculations for terms (but not dags) involving
the iter theory. Provoked by:

fmod TEST is
  sorts EvenNat OddNat Nat .
  subsorts OddNat EvenNat < Nat .

  op s : EvenNat -> OddNat [iter] .
  op s : OddNat -> EvenNat [iter] .
  op s : Nat -> Nat [iter] .
  op 0 : -> EvenNat .
endfm

*** should have sort EvenNat
parse s^2(0) .

(3) A bug causing an internal error when there are too many variables
in a unification problem. Reported by Santiago Escobar and provoked
by:

fmod ERROR is
  sort S .
  op _+_ : S S -> S .
endfm

unify (((((((X:S + X1:S) + X2:S) + X3:S) + X4:S) + X5:S) +  
X6:S) + X7:S) + (X7:S + (X6:S + (X5:S + (X4:S + (X3:S + (X2:S + (X1:S  
+ X:S))))))) =? (((((((Y:S + Y1:S) + Y2:S) + Y3:S) + Y4:S) + Y5:S) +  
Y6:S) + Y7:S) + (Y7:S + (Y6:S + (Y5:S + (Y4:S + (Y3:S + (Y2:S + (Y1:S  
+ Y:S))))))) .

Changes
========
(1) Unification modulo commutativity is now supported. Note that
redundant unifiers may be generated:

fmod COMM is
  sorts Zro NzNt Nt .
  subsorts Zro NzNt < Nt .

  op 0 : -> Zro .
  op 1 : -> NzNt .
  op s : Nt -> NzNt .
  op f : Nt Nt -> Nt [comm] .
endfm

unify f(f(X:Nt, s(Y:Nt)), f(Y:Nt, Z:Nt)) =? f(f(s(0), W:Nt),  f(s(s(0)), Z:Nt)) .

Here the 1st unifier generalizes the 2nd and the 3rd generalizes the
4th and 5th.

(2) Unification involving the iter theory is supported. Note the BDD
based sort calculation algorithm is extended to be able to push sort
calculations through large stacks of iter function symbols
efficiently:

fmod ITER is
  sorts NzEvenNat EvenNat OddNat NzNat Nat EvenInt OddInt NzInt Int .

  subsorts OddNat < OddInt NzNat < NzInt < Int .
  subsorts EvenNat < EvenInt Nat < Int .
  subsorts NzEvenNat < NzNat EvenNat < Nat .

  op 0 : -> EvenNat .

  op s : EvenNat -> OddNat [iter] .
  op s : OddNat -> NzEvenNat [iter] .
  op s : Nat -> NzNat [iter] .

  op s : EvenInt -> OddInt [iter] .
  op s : OddInt -> EvenInt [iter] .
  op s : Int -> Int [iter] .

  op _+_ : Int Int -> Int [comm gather (E e)] .
  op _+_ : OddInt OddInt -> EvenInt [ditto] .
  op _+_ : EvenInt EvenInt -> EvenInt [ditto] .
  op _+_ : OddInt EvenInt -> OddInt [ditto] .

  op _+_ : Nat Nat -> Nat [ditto] .
  op _+_ : Nat NzNat -> NzNat [ditto] .
  op _+_ : OddNat OddNat -> NzEvenNat [ditto] .
  op _+_ : NzEvenNat EvenNat -> NzEvenNat [ditto] .
  op _+_ : EvenNat EvenNat -> EvenNat [ditto] .
  op _+_ : OddNat EvenNat -> OddNat [ditto] .
endfm

unify s^1000000(X:OddNat) =? s^100000000001(Y:Int) .

unify s^1000000(X:OddNat) =? s^100000000001(Y:Int + Z:Int + W:Int) .

Steven