Dear colleagues on functional-logic programming,
Full Maude 2.4 and the Maude Manual (and its set of examples) have been
updated. Since _Core_Maude_has_not_changed_, they are distributed as
part of
version 2.4 but their date is now Feb 2009.
The main change is that now Full Maude includes an implementation of
narrowing developed by me (Santiago Escobar) and based on the AC-
unification
facilities recently included in Maude. The main new features are listed
below. Please, see the new manual for additional details.
The updated Maude 2.4 is now available from the Maude web-site at
http://maude.cs.uiuc.edu
Best regards,
-Santiago
==================================
New features and changes
==================================
For narrowing, given an order-sorted system module mod (Sigma, Ax U E,
R)
endm, such that (Sigma, Ax) satisfies the restrictions for unification
(see
Chapter 12 of the manual), the rules R must satisfy the following
conditions:
- Conditional rules are not taken into account, i.e., there may be
conditional rules in the theory but they will not be used for narrowing.
- A rule’s lefthand side cannot be a variable.
- The rules must be explicitly Ax-coherent (see Chapter 16 and Section
5.3 of
the new manual).
(1) A narrowing search command is available in Full Maude.
Given a system module <ModId>, the user can give to Full Maude a search
command of the form:
(search [ n, m ] in <ModId> : <Term-1> <SearchArrow> <Term-2> .)
where:
- n is an optional argument providing a bound on the number of desired
solutions;
- m is another optional argument stating the maximum depth of the
search;
- the system module <ModId> where the search takes place can be
omitted if it
is the current one;
- <Term-1> is the starting non-variable term, which may contain
variables;
- <Term-2> is the term specifying the pattern that has to be reached,
with
variables possibly shared with <Term-1>;
- <SearchArrow> is an arrow indicating the form of the narrowing proof
from <Term-1> until <Term-2>:
- ~>1 means a narrowing proof consisting of exactly one step,
- ~>+ means a narrowing proof consisting of one or more steps,
- ~>* means a narrowing proof consisting of none, one, or more
steps, and
- ~>! indicates that only strongly irreducible final states are
allowed,
i.e., states that cannot be further narrowed; note that this is
stronger than
requiring states that cannot be rewritten.
(2) A variants-based unification procedure is provided in Full Maude
through
the command id-unify.
Given a functional module, system module, or theory <ModId> having a
set Ax
of equational axioms for the signature Sigma such that Sigma does not
include
symbols with assoc without comm attributes in Ax, the user can give to
Full
Maude a unification command for Ax-unification of the form:
(id-unify in <ModId> : <Term-1> =? <Term-2> .)
where only one unification problem is admitted, in contrast to the unify
command, and such that no limit to the number of unifiers can be
specified.
The theories supported must satisfy the following requirements:
- the signature Sigma is preregular modulo Ax;
- the equational axioms Ax associated to function symbols are as
follows:
- there can be arbitrary function symbols and constants with no
equational
attributes;
- the iter equational attribute can be declared for some unary
symbols;
- the id:, left id:, right id:, comm, comm id:, assoc comm, and
assoc comm
id: attributes can be declared for some binary function symbols, but any
assoc attribute must also be accompanied by comm.
(3) Narrowing-based reachability analysis is also available at the
metalevel
by using the function metaNarrowSearch.
The functional module providing the necessary infrastructure is called
META-NARROWING-SEARCH and the metaNarrowSearch function has the
following
declaration:
op metaNarrowSearch : Module Term Term Substitution Qid Bound Bound ->
ResultTripleSet .
If a non-identity substitution is provided in the fourth argument,
then any
computed substitution must be an instance of the provided one, i.e.,
we can
restrict the computed narrowing sequences to some concrete shape. The
Qid
metarepresents the appropriate search arrow, similar to the metaSearch
command. For the bounds, the first bound is the maximum length of the
narrowing sequences, i.e., the depth of the narrowing tree, and the
second bound is the number of computed solutions.
(4) The procedure for equational Ax-unification where Ax can contain
any
equational attribute except assoc without comm is available at the
metalevel
by using the metaACUUnify function.
The functional module providing the necessary infrastructure is called
META-E-UNIFICATION and the metaACUUnify function available has the
following
declaration:
op metaACUUnify : Module Term Term -> SubstitutionSet .
-ago
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Mo Feb 09 2009 - 09:10:43 CET