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

From: Sergio Antoy <antoy_at_redstar.cs.pdx.edu>

Date: Wed, 20 Jun 2007 08:56:25 -0700 (PDT)

Sebastian,

Thanks for this attempt. Let me try to formalize it a little more.

*> I'll try to sum up the situation:
*

*>
*

*> The semantics of Curry differs from standard term rewriting in the
*

*> presence of non-determinism. In term rewriting, we can safely replace
*

*> variables by their bindings, even if the variables are shared and the
*

*> bindings induce a non-deterministic branching.
*

In term rewriting, there are no variables in a term being

rewritten. A variable would be treated as an irreducible constant

or a nullary constructor. In term rewriting there are variables

in rewrite rules. Replacing these variables would change the

rewrite system. So, what are we trying to capture here? I think

that we use variables for capturing sharing. In other words, we

are talking of graph rewriting. In graph rewriting a variable is

the label of a node. We use variables in two different ways. In

rewrite rules, variables are "place holders" for any term. In the

graphs to be rewritten, variables are a "notational device" to

express sharing. If we are allowed to represent a graph in other

ways than textually, we might not use variables at all as

notational devices. E.g.;

(not x, not x) where x = True ? false

vs

(,)

/ \

not not

\ /

?

/ \

True False

If we agree that a variable is (the label of) a node, the "binding

of a variable" is the subgraph rooted at that node. There is no

natural or implied replacement. There is the subgraph at the

node. And one could replace the (sub)graph at a node with another

graph, but this is a separate issue.

*> In Curry we are not
*

*> allowed to do so because of the call-time choice semantics. On the
*

*> other hand, the distributive properties
*

*>
*

*> f (x?y) = f x ? f y
*

*> (f?g) x = f x ? g x
*

*>
*

*> hold for Curry programs (without encapsulation) but not for term
*

*> rewriting! Consider
*

Let me try to formalize a bit more this distributive property.

As usual, -*-> denotes zero or more rewriting steps.

Let R be a term (or graph) rewriting system or a Curry program.

We say that the distributive property holds for R iff

for every unary symbol f, terms x and y, value v, and context C[],

C[f (x?y)] -*-> v iff C[f x ? f y] -*-> v.

*> In Curry it is true that the expression
*

*>
*

*> pair (True?False)
*

*>
*

*> has the same results as
*

*>
*

*> pair True ? pair False
*

*>
*

*> namely (True,True) and (False,False). However, in term rewriting, the
*

*> first expression could evaluate to (True,False) and (False,True)
*

*> also. Distributivity does not hold here!
*

With my proposed definition, the distributive property does not

hold for Curry programs and graph rewriting. I would conjecture

that it holds for every term rewriting system.

Cheers,

Sergio

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry

Received on Mi Jun 20 2007 - 18:28:15 CEST

Date: Wed, 20 Jun 2007 08:56:25 -0700 (PDT)

Sebastian,

Thanks for this attempt. Let me try to formalize it a little more.

In term rewriting, there are no variables in a term being

rewritten. A variable would be treated as an irreducible constant

or a nullary constructor. In term rewriting there are variables

in rewrite rules. Replacing these variables would change the

rewrite system. So, what are we trying to capture here? I think

that we use variables for capturing sharing. In other words, we

are talking of graph rewriting. In graph rewriting a variable is

the label of a node. We use variables in two different ways. In

rewrite rules, variables are "place holders" for any term. In the

graphs to be rewritten, variables are a "notational device" to

express sharing. If we are allowed to represent a graph in other

ways than textually, we might not use variables at all as

notational devices. E.g.;

(not x, not x) where x = True ? false

vs

(,)

/ \

not not

\ /

?

/ \

True False

If we agree that a variable is (the label of) a node, the "binding

of a variable" is the subgraph rooted at that node. There is no

natural or implied replacement. There is the subgraph at the

node. And one could replace the (sub)graph at a node with another

graph, but this is a separate issue.

Let me try to formalize a bit more this distributive property.

As usual, -*-> denotes zero or more rewriting steps.

Let R be a term (or graph) rewriting system or a Curry program.

We say that the distributive property holds for R iff

for every unary symbol f, terms x and y, value v, and context C[],

C[f (x?y)] -*-> v iff C[f x ? f y] -*-> v.

With my proposed definition, the distributive property does not

hold for Curry programs and graph rewriting. I would conjecture

that it holds for every term rewriting system.

Cheers,

Sergio

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry

Received on Mi Jun 20 2007 - 18:28:15 CEST

*
This archive was generated by hypermail 2.3.0
: Do Jun 20 2024 - 07:15:09 CEST
*