Maude 2.4 release with unification and narrowing

From: Santiago Escobar <>
Date: Sun, 08 Feb 2009 21:05:21 +0100

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-
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

Best regards,

New features and changes

For narrowing, given an order-sorted system module mod (Sigma, Ax U E,
endm, such that (Sigma, Ax) satisfies the restrictions for unification
Chapter 12 of the manual), the rules R must satisfy the following
- 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> .)

- n is an optional argument providing a bound on the number of desired
- m is another optional argument stating the maximum depth of the
- 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
- <Term-2> is the term specifying the pattern that has to be reached,
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
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
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
symbols with assoc without comm attributes in Ax, the user can give to
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
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
   - there can be arbitrary function symbols and constants with no
   - the iter equational attribute can be declared for some unary
   - 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
by using the function metaNarrowSearch.

The functional module providing the necessary infrastructure is called
META-NARROWING-SEARCH and the metaNarrowSearch function has the

  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
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
equational attribute except assoc without comm is available at the
by using the metaACUUnify function.

The functional module providing the necessary infrastructure is called
META-E-UNIFICATION and the metaACUUnify function available has the

  op metaACUUnify : Module Term Term -> SubstitutionSet .


curry mailing list
Received on Mo Feb 09 2009 - 09:10:43 CET

This archive was generated by hypermail 2.3.0 : Sa Feb 24 2024 - 07:15:10 CET