- 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: Wed, 20 Jun 2007 09:18:57 +0200

thanks for your replies!

*>> This is similar and related to the
*

*>> following: u = x?y implies f u = f (x?y) holds for term rewriting,
*

*>> but not for Curry programs. Here is an example:
*

*>>
*

*>> test = (not u, not u)
*

*>> where u = x?y
*

*>> x = True
*

*>> y = False
*

This example demonstrates that in Curry it is not valid to replace

variables with their bindings in the presence of non-determinism.

*> The other question is of course the precise meaning of ``=''...
*

In the mentioned distributive property the equal sign denotes

"preservation of the set of results".

*> But even if you set
*

*>
*

*> test v = (not v, not v)
*

*> u = x ? y
*

*>
*

*> , you still have
*

*>
*

*> test u = test (x?y)
*

and even more:

test (x?y) = test x ? test y

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

pair x = (x,x)

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!

Cheers,

Sebastian

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

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

Received on Mi Jun 20 2007 - 09:36:25 CEST

Date: Wed, 20 Jun 2007 09:18:57 +0200

thanks for your replies!

This example demonstrates that in Curry it is not valid to replace

variables with their bindings in the presence of non-determinism.

In the mentioned distributive property the equal sign denotes

"preservation of the set of results".

and even more:

test (x?y) = test x ? test y

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

pair x = (x,x)

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!

Cheers,

Sebastian

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

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

Received on Mi Jun 20 2007 - 09:36:25 CEST

*
This archive was generated by hypermail 2.3.0
: Di Feb 07 2023 - 07:15:09 CET
*