Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha128/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

This is mostly a bug fix release but it does include an experimental
extension of the modified PIG-PUG algorithm that is used for elementary
associative unification, in order to be complete in more cases.

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

(1) A bug where bad modules that were left in an inconsistent state were
still allowed to be pulled up to the metalevel, causing an internal error.
Reported by Rubén, and illustrated by the following example:

fmod BAD is
  pr NON-EXISTENT .
endm

red in META-LEVEL : upModule('BAD, false) .

This also affected other ascent functions; for example:

red in META-LEVEL : upSorts('BAD, false) .


(2) A bug where illegal variable names such as '#1:Nat in narrowing
rules and variant equations weren't being detected in the functional
metalevel (unlike the object level and meta-interpreters) and quietly
produced incorrect results. Reported by Stephen Skeirik
<skeirik2@illinois.edu>.


(3) A bug where Maude hangs when a server socket is closed with a
closeSocket() message. This happens because the PseudoThread class
that makes the poll() system call isn't being told that the socket
has been closed. Reported by Rubén.

Changes
========

(1) The command to clear the memo tables of the current module
now optionally takes a module name.

do clear memo FOO .

is equivalent to

select FOO .
do clear memo .

The main reason of the change is so allow this command to use the
the same current module validating code as the other commands such

show module FOO .


(2) There is a new version of the PIG-PUG algorithm that is used to solve
elementary associative unification. This version uses the sort bound
idea that I introduced many years ago for A(C)(U) matching and later
AC(U) unification to constrain what assignments are allowed in the
unsorted unification phase based on sort considerations. The old version
of PIG-PUG only took element variables into account, while this version
supports variables with arbitrary finite bounds. Such variables can be
ignored for the purpose of determining strict left-linearity. Thus certain
problems where Maude 3.0 would report incompleteness, even though there
were only finite order-sorted unifiers can now be solved completely.
Consider:

fmod TEST is
  sorts Elt Pair Triple List .
  subsort  Elt < Pair < Triple < List .
  op __ : Elt Elt -> Pair [assoc] .
  op __ : Elt Pair -> Triple [assoc] .
  op __ : Pair Elt -> Triple [assoc] .
  op __ : List List -> List [assoc] .

  var E F G : Elt .
  var P Q R : Pair .
  var T U V : Triple .
  var L M N : List .
endfm

Here although Pair and Triple can take terms with the associative
symbol on top, they have upper-bounds of 2 and 3 respectively on
the number of arguments that can appear under the associative symbol.
This allows the new algorithm to terminate with a finite complete
set of unifiers in cases like:

unify P T =? T P .

Here the unsorted problem has an infinite set of most general unifiers:

P --> #1 ^ n
T --> #1 ^ m
for gcd(n,m) = 1

and the old PIG-PUG implementation is incomplete - if you use

set verbose on .

you will see it uses cycle detection and finds a cycle corresponding
to an infinite family of unifiers. However only 5 of these unsorted
unifiers correspond to order-sorted unifiers:

Solution 1
P --> #1:Elt #1:Elt
T --> #1:Elt

Solution 2
P --> #1:Elt #1:Elt
T --> #1:Elt #1:Elt #1:Elt

Solution 3
P --> #1:Elt
T --> #1:Elt #1:Elt #1:Elt

Solution 4
P --> #1:Elt
T --> #1:Elt #1:Elt

Solution 5
P --> #1:Pair
T --> #1:Pair

and the new algorithm computes these directly by tracking bounds
through the PIG-PUG moves and terminates without the need for
cycle detection.

For termination purposes, only unbounded variables count for
determining if a problem is strict left-linear - the main case
that can be handled finitely - so quite complex ordered sorted
elementary A unification problems with hundreds of unifiers can be
solved completely:

unify V L T L U =? T T U M U V V .
unify T T U M U V V T T =? V L T L U T V N T V .

Here the only unbounded variable that occurs on the left-hand side
in both problems is M and since it only occurs once, the problems
are strict left-linear and can be shown to have a finite number
of order-sorted unifiers.


(3) The handling of ^C handing during the unify command has been
cleaned up so that a junk unifier isn't printed before halting.


(4) The handling of ^C handing during the match command has been 
changed so that if a ^C arrives after a solution has been obtained 
rather than during rewriting (to evaluate a side condition) the command
immediately halts. Thus whether ^C produces an abort or drops you
into the debugger depends on a race condition. While this is somewhat
unsatisfactory, the old behavior where Maude would ignore ^C and
spew junk matchers if there was no rewriting happening was worse.


(5) The missing projection functions for UnificationPair,
UnificationTriple, Variant and TraceStep are added:

  op getSubstitution : UnificationPair -> Substitution .
  op getVariableFamily : UnificationPair -> Qid .

  op getLhsSubstitution : UnificationTriple -> Substitution .
  op getRhsSubstitution : UnificationTriple -> Substitution .
  op getVariableFamily : UnificationTriple -> Qid .

  op getTerm : Variant -> Term .
  op getSubstitution : Variant -> Substitution .
  op getVariableFamily : Variant -> Qid .
  op getParent : Variant -> Parent .
  op getMoreVariantsInLayerFlag : Variant -> Bool .

  op getTerm : TraceStep -> Term .
  op getType : TraceStep -> Type .
  op getRule : TraceStep -> Rule .

Note that only the new forms of UnificationPair, UnificationTriple
and Variant are supported in order to discourage the use of the
deprecated forms.


(6) There is a utility function in META-LEVEL,
  op applySubstitution : Module Term Substitution -> Term .
which applies a substitution to a term and puts the result in
theory-normal form. Currently this is written in Maude using
equations that hit the optimal case for the matching algorithms
but it might be reimplemented as a descent function at some point
if it becomes a performance bottleneck.


The supplied binaries are linked with the latest libraries.
Note that because of issues building the latest CVC4 library,
I've only produced Yices2 binaries for the moment, though there
should be no difficulty building CVC4 versions _if_ you can
get CVC4 to build. I've dropped the "64" from the binary
names since no one uses 32-bit machines anymore.

Steven