- Contemporary messages sorted: [ by date ] [ by thread ] [ by subject ] [ by author ] [ by messages with attachments ]

From: Santiago Escobar <sescobar_at_dsic.upv.es>

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-

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 ﬁnal 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-uniﬁcation 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

speciﬁed.

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-uniﬁcation 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

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-

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 ﬁnal 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-uniﬁcation 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

speciﬁed.

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-uniﬁcation 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

*
This archive was generated by hypermail 2.3.0
: Mi Okt 21 2020 - 07:15:04 CEST
*