Maude 2.4 release updated

[Francisco Durán]

Dear colleagues,

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 based on the unification facilities by Santiago Escobar. 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,

The Maude Team

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

_______________________________________________
Maude-users mailing list
Maude-users@...
http://maude.cs.uiuc.edu/cgi-bin/mailman/listinfo/maude-users