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

From: Bernd Brassel <bbr_at_informatik.uni-kiel.de>

Date: Fri, 02 Nov 2007 11:18:20 +0100

Thanks, Sergio, for the interesting discussion. I really do not think

that it is of such marginal importance.

And I think the "independence of the order of evaluation" is the key

problem to what you brought up. I also like Paco's example which seems

to me to be very direct to the point.

*> Paco's example:
*

*>
*

*> f 0 = 0
*

*> g 1 = 1
*

*> f x ? g x where x free
*

*>
*

*> The results are 0 and 1 independently of the order of evaluation
*

*> whether or not x is shared, since there is no residuation (easy
*

*> to verify all the possibilities).
*

Why does the problem have to do with residuation? Why is 1 still a

result if you decide to reduce (f x) first? In order to be able to

really reduce this in most settings, you need x to be 0.

So, let us consider a setting, where there really is an arbitrary

choice of evaluation order for this example. To make things simpler, I

would like to look at a slightly different expression

e:=let x=0?1 in f x ? g x

Now there would be some possibilities (=> is a parallel step):

1) e -> (let x=0?1 in f x) ? (let x=0?1 in g x) => (f 0 ? f 1) ? (g 0 ?

g 1) => 0 ? _|_ ? _|_ ? 1 = 0 ? 1

2) e -> (f 0 ? g 0) ? (f 1 ? g 1) => 0 ? _|_ ? _|_ ? 1 = 0 ? 1

Is this maybe towards the "independence from evaluation order" you have

in mind for this example, Sergio?

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

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

Received on Fri Nov 02 2007 - 12:05:05 CET

Date: Fri, 02 Nov 2007 11:18:20 +0100

Thanks, Sergio, for the interesting discussion. I really do not think

that it is of such marginal importance.

And I think the "independence of the order of evaluation" is the key

problem to what you brought up. I also like Paco's example which seems

to me to be very direct to the point.

Why does the problem have to do with residuation? Why is 1 still a

result if you decide to reduce (f x) first? In order to be able to

really reduce this in most settings, you need x to be 0.

So, let us consider a setting, where there really is an arbitrary

choice of evaluation order for this example. To make things simpler, I

would like to look at a slightly different expression

e:=let x=0?1 in f x ? g x

Now there would be some possibilities (=> is a parallel step):

1) e -> (let x=0?1 in f x) ? (let x=0?1 in g x) => (f 0 ? f 1) ? (g 0 ?

g 1) => 0 ? _|_ ? _|_ ? 1 = 0 ? 1

2) e -> (f 0 ? g 0) ? (f 1 ? g 1) => 0 ? _|_ ? _|_ ? 1 = 0 ? 1

Is this maybe towards the "independence from evaluation order" you have

in mind for this example, Sergio?

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

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

Received on Fri Nov 02 2007 - 12:05:05 CET

*
This archive was generated by hypermail 2.3.0
: Mon Nov 11 2019 - 07:15:07 CET
*