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

From: Sebastian Fischer <sebf_at_informatik.uni-kiel.de>

Date: Thu, 21 Jun 2007 12:15:24 +0200

Dear Sergio,

thanks for your reply. It reminds me to use articulate statements in

order to not being misunderstood.

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

I referred to variables in rewrite rules. But with 'replacing

variables' I didn't mean to change the rewrite system. When a rule of

a term rewrite system is applied, the variables in the right-hand

side of this rule are replaced by other terms. I think the source of

confusion is that my examples uses variables that are arguments of

functions while yours uses variables that are defined in a local

declaration. Before I comment on your formalization and graph

rewriting, let me point out differences between local and top-level

declarations in Curry:

Wolfgang wrote:

*> Would you accept the following reformulation?
*

*>
*

*> | If "u = x?y" is a (desugared) program rule
*

*> | (as opposed to a (derived) semantic equation),
*

*> | then t[v \ u] = t[v \ (x?y)] holds as a semantic equation,
*

*> | otherwise the substitution rule holds only for values,
*

*> | or for expressions having the same SINGLE values.
*

*>
*

*> It tries to make explicit how program rules,
*

*> which are used as rewriting rules,
*

*> connect the two worlds....
*

Here, "program rules" should mean "rules on top-level" because as you

can see from the examples introduced by Sergio, local declarations

behave differently. For example the following two Curry programs have

different semantics:

program 1:

pair = (x,x)

x = True ? False

program 2:

pair = (x,x)

where

x = True ? False

I consider this counter intuitive.

Now back to the formalization of distributivity:

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

At first, I considered this a good formalization, but now I noticed

that it holds neither in term rewriting nor in graph rewriting (but

in some sense in Curry).

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

Here is a counter example:

pair x = (x,x)

Now, we have

pair (True?False) -> (True?False,True?False) -> (True,True?False) ->

(True,False)

in other words: pair (True?False) -*-> (True,False), i.e., the left

part of the equivalence holds for

f = pair, x = True, y = False, v = (True,False) and an empty context C

The corresponding right part of the equivalence is

pair True ? pair False -*-> (True,False)

which is wrong. As a conclusion, distributivity as you defined it

does not hold for term rewriting.

For completeness, lets observe that your example is indeed a counter

example for the distributive law in graph rewriting. Here, we choose

f as the first 'not', x as True and y as False and the context C as

the surrounding expression:

(not z, not z) where z = True ? False

The only values of this expression are (True,True) and (False,False).

The right part of the equivalence is now:

(not True, not z) ? (not False, not z) where z = True ? False

which has more results. If we link both non-deterministic choices and

restrict them to choose the same alternative in every computation,

then the law holds. This observation is familiar to those who are

aware of a new natural semantics for Curry which is unfortunately not

yet published.

In the context of Curry, your equivalence is not applicable to

(not z, not z) where z = True ? False

as there is no function application of the form f (x?y) in this

expression. This textual understanding of the rule ensures that the

argument of f cannot be shared somewhere else in the context C.

However, there is no Curry semantics (besides graph rewriting) that

allows such expressions -- usually only normalized expressions are

allowed.

If we agree that

f z where z = (x?y)

is not a Curry expression of the form 'f (x?y)', then the

distributive property as you defined it holds for Curry programs.

I tried to reformulate the property such that it holds for graph

rewriting too but did not get to an elegant definition yet.

I'd like to see a definition that is satisfied or Curry and graph

rewriting but not for term rewriting because I think the distributive

law characterizes call-time choice semantics. Curry and graph

rewriting have call-time choice semantics while term rewriting has not.

I need to think about this some more..

Cheers,

Sebastian

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

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

Received on Do Jun 21 2007 - 12:27:31 CEST

Date: Thu, 21 Jun 2007 12:15:24 +0200

Dear Sergio,

thanks for your reply. It reminds me to use articulate statements in

order to not being misunderstood.

I referred to variables in rewrite rules. But with 'replacing

variables' I didn't mean to change the rewrite system. When a rule of

a term rewrite system is applied, the variables in the right-hand

side of this rule are replaced by other terms. I think the source of

confusion is that my examples uses variables that are arguments of

functions while yours uses variables that are defined in a local

declaration. Before I comment on your formalization and graph

rewriting, let me point out differences between local and top-level

declarations in Curry:

Wolfgang wrote:

Here, "program rules" should mean "rules on top-level" because as you

can see from the examples introduced by Sergio, local declarations

behave differently. For example the following two Curry programs have

different semantics:

program 1:

pair = (x,x)

x = True ? False

program 2:

pair = (x,x)

where

x = True ? False

I consider this counter intuitive.

Now back to the formalization of distributivity:

At first, I considered this a good formalization, but now I noticed

that it holds neither in term rewriting nor in graph rewriting (but

in some sense in Curry).

Here is a counter example:

pair x = (x,x)

Now, we have

pair (True?False) -> (True?False,True?False) -> (True,True?False) ->

(True,False)

in other words: pair (True?False) -*-> (True,False), i.e., the left

part of the equivalence holds for

f = pair, x = True, y = False, v = (True,False) and an empty context C

The corresponding right part of the equivalence is

pair True ? pair False -*-> (True,False)

which is wrong. As a conclusion, distributivity as you defined it

does not hold for term rewriting.

For completeness, lets observe that your example is indeed a counter

example for the distributive law in graph rewriting. Here, we choose

f as the first 'not', x as True and y as False and the context C as

the surrounding expression:

(not z, not z) where z = True ? False

The only values of this expression are (True,True) and (False,False).

The right part of the equivalence is now:

(not True, not z) ? (not False, not z) where z = True ? False

which has more results. If we link both non-deterministic choices and

restrict them to choose the same alternative in every computation,

then the law holds. This observation is familiar to those who are

aware of a new natural semantics for Curry which is unfortunately not

yet published.

In the context of Curry, your equivalence is not applicable to

(not z, not z) where z = True ? False

as there is no function application of the form f (x?y) in this

expression. This textual understanding of the rule ensures that the

argument of f cannot be shared somewhere else in the context C.

However, there is no Curry semantics (besides graph rewriting) that

allows such expressions -- usually only normalized expressions are

allowed.

If we agree that

f z where z = (x?y)

is not a Curry expression of the form 'f (x?y)', then the

distributive property as you defined it holds for Curry programs.

I tried to reformulate the property such that it holds for graph

rewriting too but did not get to an elegant definition yet.

I'd like to see a definition that is satisfied or Curry and graph

rewriting but not for term rewriting because I think the distributive

law characterizes call-time choice semantics. Curry and graph

rewriting have call-time choice semantics while term rewriting has not.

I need to think about this some more..

Cheers,

Sebastian

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

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

Received on Do Jun 21 2007 - 12:27:31 CEST

*
This archive was generated by hypermail 2.3.0
: Do Aug 06 2020 - 07:15:05 CEST
*