Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha113/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

This version revises and extends the variant unification based
narrowing capabilities.

Changes
========

(1) There is now a new statement attribute, narrowing, that may be
given to rules:

  rl g(i(X, k(Y, Z))) => f(k(Z, X)) [narrowing] .

It indicates that the rule should be used for narrowing. Variant unification
based narrowing now only uses rules with this attribute.

(2) The vu-narrow command is unchanged but the results now include the
accumulated substitution. Furthermore the accumulated substitution is
applied to the goal term before the final variant unification step
so it is reasonable to have variables from the start term appear in
the goal term:

mod FOO is
  sort Foo .
  ops f g h : Foo -> Foo .
  op i : Foo Foo -> Foo .

vars X Y Z W A B C D : Foo .
  rl i(f(X), h(Y)) => g(f(X)) [narrowing] .
endm

vu-narrow i(A, B) =>+ g(A) .

Solution 1
rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second)
state: g(f(@1:Foo))
accumulated substitution:
A --> f(@1:Foo)
B --> h(@2:Foo)
variant unifier:
@1:Foo --> #1:Foo

Note that because A wast instantiated by the accumulated
substitution, it does not get a binding in the final
variable unifier.

Note that fresh variables like #1, %1 or @1 are reserved for the
various internal narrowing and unification processes and should
not appear in the intial term or the goal.

(3) There is now a new command, fvu-narrow, that works just like
vu-narrow, but with folding. A state S is considered to be
more general that a state T if S <=_E T. Note that this
matching takes place modulo the axioms E only - any variant
equation are ignored for this step. Furthermore, the accumulated
substitution is not considered (unlike variant folding).

 A state is only considered for variant unification with the goal
if no more general state has been seen when it is generated
(or for =>! when it fails to expand). Likewise it is only considered
for expansion if no more general state has been seen, when its turn
for expansion comes around.

It is possible that a state T might be variant unified with the
goal but but later on, not be expanded because some intervening
expansion has generated a more general state S.

(4) At the metalevel, the new statement attribute is reflected by:
  op narrowing : -> Attr [ctor] .

(5) The descent function making single steps of vu-narrowing is now:
  op metaNarrowingApply : Module Term TermList Qid Nat -> NarrowingApplyResult? .

where the arguments are:
  Module to work in
  Term to narrow (after reducing)
  TermList of blocker terms for variant unification
  Qid giving fresh variable family that might appear in Term (and which will be avoided for result)
  Nat giving which of many solutions is wanted

It no longer takes a Qid specifying the label of the rules to use, as this
information is now conveyed by the narrowing attribute.
The success result is:
  op {_,_,_,_,_,_,_} : Term Type Context Qid Substitution Substitution Qid -> NarrowingApplyResult [ctor] .

where the arguments are:
  Term after narrowing and reducing
  Type of Term
  Context in the original term where narrowing took place
  Qid giving label of rule used
  Substitution into the original term
  Substitution into the rule used for narrowing
  Qid giving fresh variable family used to express result Term and Substitutions

and the failure results are:
  op failure : -> NarrowingApplyResult? [ctor] .
  op failureIncomplete : -> NarrowingApplyResult? [ctor] .

(6) The descent function for searching for sequences for vu-narrowing
steps is now:
  op metaNarrowingSearch : Module Term Term Qid Bound Qid Nat -> NarrowingSearchResult? .

where the arguments are:
  Module to work in
  Term to narrow (after reducing)
  Term that is goal to be reached
  Qid giving search type
  Bound on depth of search
  Qid giving folding strategy
  Nat giving which of many solutions is wanted

Currently the only legal values for the folding strategy are 'none which is
equivalent to vu-narrow and 'match which is equivalent to fvu-narrow.
The success result is:
  op {_,_,_,_,_,_} : Term Type Substitution Qid Substitution Qid -> NarrowingSearchResult [ctor] .

where the arguments are:
  Final term after narrowing and reducing
  Type of Term
  Accumulated Substitution
  id giving fresh variable family used to express result Term and accumulated Substitution
  Unifier between narrowed term and instantiated pattern
  Qid giving fresh variable family used to express unifier

and the failure results are:
  op failure : -> NarrowingSearchResult? [ctor] .
  op failureIncomplete : -> NarrowingSearchResult? [ctor] .

(7) There is a new descent function:
  op metaNarrowingSearchPath : Module Term Term Qid Bound Qid Nat -> NarrowingSearchPathResult? .

This takes the same arguments and carries out the same computation as
metaNarrowingSearch(). The different is that it saves (part of) the search
graph and returns the path to each successful state:

  op {_,_,_,_,_,_} : Term Type Substitution NarrowingTrace Substitution Qid -> NarrowingSearchPathResult [ctor] .

where the arguments are:
  Initial term after renaming and reducing
  Type of term
  Substitution corresponding to initial renaming
  Trace of narrowing steps
  Unifier between narrowed term and instantiated pattern
  Qid giving fresh variable family used to express unifier

Note that all the vu-narrowing sequence commands and descent functions
rename the variables in the initial term to #variables to avoid potential
conflicts with variables in narrowing rules. This is mostly invisible to
the user, except for tracing and this descent function. Here this initial
renaming is included at the 3rd argument.

Failure results are:
  op failure : -> NarrowingSearchPathResult? [ctor] .
  op failureIncomplete : -> NarrowingSearchPathResult? [ctor] .

The trace is an associative list built from the following construtors.
  op nil : -> NarrowingTrace [ctor] .
  op __ : NarrowingTrace NarrowingTrace -> NarrowingTrace [ctor assoc id: nil] .
  op {_,_,_,_,_,_,_} : Context Qid Substitution Qid Term Type Substitution -> NarrowingStep [ctor] .

where the arguments to the NarrowingStep constructor are:
  Context where narrowing happens
  Label of rule used for narrowing
  Variant unifier used for narrowing
  Qid giving fresh variable family used to express unifier
  New term (after reducing)
  Type of term
  Accumulated Substitution

Steven