Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha129/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

Bug fixes
==========
(1) Removed a stray space after the last unification equation when
echoing top level variant unify command.

(2) A memory leak in the metalevel where terms were not being
completely deleted when the arguments of a unification
descent function were erroneous.

New features
=============
(1) There is a command to generate irredundant unifiers:

fmod BAG is
  sorts Elt Bag .
  subsort Elt < Bag .
  op empty : -> Bag .
  op __ : Bag Bag -> Bag [assoc comm id: empty] .
vars L M N O P Q : Bag .
vars E F G : Elt .
endfm

irredundant unify L M =? P Q .

Here because of the sort decreasing axioms the ACU unification
algorithm is obliged to generate a large number of redundant
unsorted unifiers in case subsumption between unsorted
unifiers doesn't hold after sorts are computed or a subsuming
unifier doesn't survive order sorting. The new command
generates all the unifiers and filters them against each other.
This is somewhat expensive but is useful if you want to know the
cardinality of the minimal complete set of unifiers (which is
uniquely defined for a given unification problem). It also
means that no unifier will be output until all have been generated.

For problems on which Maude's unification algorithms are incomplete,
the irredundant set of unifiers found will be the most general members
of the incomplete set that regular unification finds, though there
is no guarantee that either set contains any unifiers that are most
general for the original problem.

You could get the same result in earlier versions Maude of by using
variant unification without any variant equations but this is more
expensive because there are two levels of filtering: at the unifier
level and at the variant folding level.

In the functional metalevel this functionality is reflected by two new
descent functions:

  op metaIrredundantUnify :
     Module UnificationProblem Qid Nat ~> UnificationPair? [...] .
  op metaIrredundantDisjointUnify :
     Module UnificationProblem Qid Nat ~> UnificationTriple? [...] .

These work precisely like metaUnify() and metaDisjointUnify()
respectively except they filter out redundant unifiers.

In the meta-interpreter this functionality is reflected by two new
message pairs:

  op getIrredundantUnifier :
     Oid Oid Qid UnificationProblem Qid Nat -> Msg [ctor msg format (b o)] .
  op gotIrredundantUnifier :
     Oid Oid Substitution Qid -> Msg [ctor msg format (m o)] .

and

  op getIrredundantDisjointUnifier :
     Oid Oid Qid UnificationProblem Qid Nat -> Msg [ctor msg format (b o)] .
  op gotIrredundantDisjointUnifier :
     Oid Oid Substitution Substitution Qid -> Msg [ctor msg format (m o)] .

These work precisely like the message pairs getUnifier()/gotUnifier()
and getDisjointUnifier()/gotDisjointUnifier() respectively except they
filter out redundant unifiers.

(2) There is a new command to filter variant unifiers using
variant subsumption:

fmod ID-UNSORTED is
  sort List .
  op nil : -> List .
  op __ : List List -> List [assoc] .
  ops a b c : -> List .
vars L P : [List] .
vars W X Y Z M N Q R : List .
  eq P nil L = P L [variant] .
  eq nil L = L [variant] .
  eq L nil = L [variant] .
endfm

filtered variant unify X Y =? W a .

This does for variant unification what irredundant unification does
for unification - it removes redundant unifiers by subsumption with
respect to the axioms and the variant equations. Note that regular
variant unification doesn't even guarantee removal of redundant
unifiers with respect to the axioms because unifiers are output
as soon as they are generated can could potentially be subsumed by
a later unifier. Here no unifier is output until all unifiers have
been generated so every unifier is checked (possibly transitively)
against every other. This functionality is called filtered variant
unification rather than irredundant variant unification because
complete removal of redundant unifiers cannot be guarenteed if
incomplete unification algorithms are involved, because variant
subsumption is computed using a skeleton form of variant
narrowing which only considers variant terms. Because we don't
care about which variant matcher actually witnesses subsumption
we don't bother with the variant substitution and states can
be considered equal if their variant term parts are equal.
An advisory is printed informing the user if the filtering
process is complete and a warning is printed if the filtering
process is incomplete.

In the functional metalevel we extend the metaVariantUnify() and
metaVariantDisjointUnify() with a new VariantOptionSet argument.

  op metaVariantUnify : Module UnificationProblem TermList Qid
                        VariantOptionSet Nat ~> UnificationPair? [...] .
  op metaVariantDisjointUnify : Module UnificationProblem TermList Qid
                                VariantOptionSet Nat ~> UnificationTriple? [...] .

The VariantOptionSet terms are formed from the signature:
  
  sorts VariantOption VariantOptionSet .
  subsort VariantOption < VariantOptionSet .
  ops delay filter : -> VariantOption [ctor] .
  op none : -> VariantOptionSet [ctor] .
  op __ : VariantOptionSet VariantOptionSet -> VariantOptionSet [ctor assoc comm id: none] .

Here the delay option delays returning unifiers until all have
been generated (essentially equivalent to irredundant variant
generation) while filter uses variant subsumption to compare unifiers.
Combining both options obtains the semantics of filtered variant
unify. However I have yet to find an example where the delay option
reduces the number of unifiers returned regardless of whether filter
is used. My suspicion is that later unifiers, because they result
from deeper variant narrowing, are unlikely to subsume earlier
unifiers in most FVP theories.

In the interests of backward compatibility the old versions of
metaVariantUnify() and metaVariantDisjointUnify() equationally
reduced to the new versions with VariantOptionSet passed as none.

In the meta-interpreter, the messages getVariantUnifier() and
getDisjointVariantUnifier() now take a VariantOptionSet argument:

  op getVariantUnifier : Oid Oid Qid UnificationProblem TermList Qid
                         VariantOptionSet Nat -> Msg [ctor msg format (b o)] .
  op getDisjointVariantUnifier : Oid Oid Qid UnificationProblem TermList Qid
                                 VariantOptionSet Nat -> Msg [ctor msg format (b o)] .

The new argument takes the same values and has the same
semantics as in the functional metalevel versions. Again the
old versions of these messages equationally reduces to the new
versions with VariantOptionSet passed as none, for backward
compatibility.

(3) There is a new command to generate variant matchers:

fmod VARIANT-MATCH-TEST is
  sort Foo .
  ops f g h : Foo -> Foo .
  ops a b c : -> Foo .

vars X Y Z : Foo .
  eq f(X) = g(X) [variant] .
endfm

variant match f(X) <=? g(Y) /\ g(Y) <=? f(b) .

Variant matching works like variant unification except that
right hand side of each match pair is considered to be a ground
term with any variable treated as a constant. Thus the
two appearances of Y above are completely different. The first
one is treated like a constant and the second one is a normal
variable. Operationally Maude uses a slightly different algorithm
to that for variant unification: only the left hand sides are
expanded using variant narrowing, while the right hand sides
are merely reduced (since they don't contain anything that
is treated like a variable, narrowing would be pointless).
The reduced right hand sides are then matched rather unified
with the variants generated for the left hand sides.
Because variant equations may be non-regular, it may be
necessary to introduce new variables to express a complete
set of matchers. If this happens they are always selected
from the # variable family. Just like variant unification
at the object level, the pattern may not contain variables
from the #, % and @ families. The subject is not restricted
since such variables are regarded as constants. If # variables
appear in the subject and new # variables are needed, the
new variables are numbered so as to avoid a clash.

At the metalevel, simultaneous matching problems are built
using the new metasyntax:

  sorts PatternSubjectPair MatchingProblem .
  subsort PatternSubjectPair < MatchingProblem .
  op _<=?_ : Term Term -> PatternSubjectPair [ctor prec 71] .
  op _/\_ : MatchingProblem MatchingProblem -> MatchingProblem
    [ctor assoc comm prec 73] .

Since variant matching may be incomplete there is a new result
constructor:

  op noMatchIncomplete : -> Substitution? [ctor] .

In the functional metalevel variant matching is reflected by the
new descent function:

  op metaVariantMatch : Module MatchingProblem TermList Qid
                        VariantOptionSet Nat ~> Substitution? [...] .

Here the arguments are:
Module : module to work in
MatchingProblem : simultaneous matching problem
TermList : irreducibility constraints
Qid : variable family whose variables may appear in patterns
VariantOptionSet : for future extensions; must be none currently
Nat : index of matcher wanted

The matcher is returned as a substitution; or noMatch if there
are no more matchers and the variant narrowing was complete; or
noMatchIncomplete if there are no more matchers and the variant
narrowing was incomplete.

In the meta-interpreter is a new message pair:

  op getVariantMatcher : Oid Oid Qid MatchingProblem TermList Qid
                         VariantOptionSet Nat -> Msg [ctor msg format (b o)] .

where:
Oid, Oid : target and sending objects
Qid : name of module to work in
MatchingProblem : simultaneous matching problem
TermList : irreducibility constraints
Qid : variable family whose variables may appear in patterns
VariantOptionSet : for future extensions; must be none currently
Nat : index of matcher wanted

  op gotVariantMatcher : Oid Oid RewriteCount Substitution -> Msg [ctor msg format (m o)] .

where:
Oid, Oid : target and sending objects
RewriteCount : total of rewrite and narrowing steps
Substitution : matcher

If there are no more matchers, the generic 

  op noSuchResult : Oid Oid Bool -> Msg [ctor msg format (m o)] .

message is return, with the Bool argument indicating completeness
of the variant narrowing.

Other changes
==============
(1) File handling and process execution are now disabled by
default. It is difficult to for a user to tell just by looking
at it, if an arbitrary Maude program contains malware and in
particular, a Maude program can assemble meta-malware using
innocent looking code and then execute it in a meta-interpreter.
These features need to be enabled with the command line flags
  -allow-files
and
  -allow-processes
If you're running code that you completely trust the command
line flag
  -trust
enables all dangerous features. The -no-execute flag is removed.

(2) The situation of sort decreasing axioms which is critical
for chosing which unification algorithm to use in collapse
theories is now explicitly noted if verbose mode,
  set verbose on .
is used. Axioms which neither sort preserving nor sort decreasing
are consider errors and have always generated a warning.

(3) Previously when a program attempted to receive() on a
socket, the other end of which was closed for writing (either
just the writing half with shutdown() or the whole socket with
shutdown() or close()), Maude would close the socket and
return a closedSocket() message. This however prevents the
common idiom where a program will close its write half of
a socket to indicate that it is done sending data while still
wanting to read results. In the Alpha 128a the semantics of
send() changed so that Maude programs could employ this idiom
when communicating with programs that expect it. In this version
the semantics of receive() are changed so that Maude programs
can handle the other end of the idiom.

The new behavior is that when an end-of-file condition is seen
during a receive(), Maude will return a received() message with
the empty string the first time it happens. This allows new
code to recognize the situation and handle it appropriately.

To minimize backwards incompatibility with legacy code that
is expecting to see a closedSocket() message, the second time
it happens on a socket, Maude reverts to the old semantics and
closes the socket. Legacy code should be prepared to deal with
its input coming in as multiple receive()s anyway so only weird
code that treats the empty string specially but doesn't grok
the empty string as end-of-file should be impacted. New code
should handle receiving an empty string and not send the socket
any more receive() messages so the legacy semantics are not
triggered.

(4) The conventions for naming lists of results returned by top
level commands has been made uniform:

match/xmatch : Solution n -> Matcher n
unify : Solution n -> Unifier n
get variants/get irredundant variants : Variant #n -> Variant n
variant unify : Unifier #n -> Unifier n

In particular the removal of the redundant # was suggested by
Santiago since they visually clash with the # family of fresh
variables.

(5) irred is an abreviation for irredundant on the command line.

Steven