- 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: Thu, 08 Nov 2007 10:52:05 -0800 (PST)

Hi Wolfgang,

I dropped this issue, but it keeps coming back, so I'll try one

more time.

*> I'm sorry Sergio, but I do not understand you problem here.
*

My fault. I should have explained it better. Sorry if this

message is long. First I change a bit your program to work only

with algebraic types, the usual integers are not defined by a

finite data declaration (but Brassel et al. showed that they could

be "declared").

t = let x free in (f x ? g x)

f True = success

g False = success

I also assume that both f and g are flexible or narrow their

argument.

Let (a/x) denote the substitution that maps x to a. t(True/x)

evaluates to success and so t(False/x). A complete strategy

evaluates t to success with computer answer (True/x) and likewise

(False/x).

t has 3 narrexes (4 steps). I think you disagreed with this

statement in the past, but I insist.

1. t -> let x free in f x

2. t -> let x free in g x

3. t -> success ? g (True ? False)

4. t -> f (True ? False) ? success

In the narrowing step, I bound the free variable x to (True ?

False) rather than only True or only False, because variables may

be shared (indeed x is shared in this case).

Each of these steps can be extended to a derivation that computes

an intended result. All this is good. In particular, the order

of evaluation does not affect the results of t. The last

statement is subtle, because depending on the first step some

computed expressions are not longer reachable, but the concept can

be satisfatorily formalized.

Now, here comes the twist.

Suppose that g is rigid or residuates on its argument. What are

the intended results of t? If t is equal to

(let x free in f x) ? (let x free in g x)

the the only result is success with (True/x). Then the

independence of the order of evaluation argued above is lost. The

derivations starting with steps 1 and 2 give the intended meaning,

step 4 is never computed, which is OK, but step 3 gives a wrong

result. Incompleteness problems with the order of evaluation are

not new, e.g., consider backtracking or see

http://www.informatik.uni-kiel.de/~pakcs/pitfalls.html. This is

the first case I know of unsoundness. Furthermore, the problem

originates from parallelism rather than lack of parallelism.

Are there simple, good solutions? Fixing the order of evaluation

is very bad. Banning residuation may be difficult because of

builtin types. Giving a declarative semantics for which the

variable x in (let x free in (f x ? g x)) is not shared seems

difficult as well. The only solution that I see at this time is

that the variable x in (let x free in (f x ? g x)) is indeed

shared. If this is not what the programmer intends, he can

simply code ((let x free in f x) ? (let x free in g x)).

Cheers,

Sergio

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

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

Received on Thu Nov 08 2007 - 23:27:25 CET

Date: Thu, 08 Nov 2007 10:52:05 -0800 (PST)

Hi Wolfgang,

I dropped this issue, but it keeps coming back, so I'll try one

more time.

My fault. I should have explained it better. Sorry if this

message is long. First I change a bit your program to work only

with algebraic types, the usual integers are not defined by a

finite data declaration (but Brassel et al. showed that they could

be "declared").

t = let x free in (f x ? g x)

f True = success

g False = success

I also assume that both f and g are flexible or narrow their

argument.

Let (a/x) denote the substitution that maps x to a. t(True/x)

evaluates to success and so t(False/x). A complete strategy

evaluates t to success with computer answer (True/x) and likewise

(False/x).

t has 3 narrexes (4 steps). I think you disagreed with this

statement in the past, but I insist.

1. t -> let x free in f x

2. t -> let x free in g x

3. t -> success ? g (True ? False)

4. t -> f (True ? False) ? success

In the narrowing step, I bound the free variable x to (True ?

False) rather than only True or only False, because variables may

be shared (indeed x is shared in this case).

Each of these steps can be extended to a derivation that computes

an intended result. All this is good. In particular, the order

of evaluation does not affect the results of t. The last

statement is subtle, because depending on the first step some

computed expressions are not longer reachable, but the concept can

be satisfatorily formalized.

Now, here comes the twist.

Suppose that g is rigid or residuates on its argument. What are

the intended results of t? If t is equal to

(let x free in f x) ? (let x free in g x)

the the only result is success with (True/x). Then the

independence of the order of evaluation argued above is lost. The

derivations starting with steps 1 and 2 give the intended meaning,

step 4 is never computed, which is OK, but step 3 gives a wrong

result. Incompleteness problems with the order of evaluation are

not new, e.g., consider backtracking or see

http://www.informatik.uni-kiel.de/~pakcs/pitfalls.html. This is

the first case I know of unsoundness. Furthermore, the problem

originates from parallelism rather than lack of parallelism.

Are there simple, good solutions? Fixing the order of evaluation

is very bad. Banning residuation may be difficult because of

builtin types. Giving a declarative semantics for which the

variable x in (let x free in (f x ? g x)) is not shared seems

difficult as well. The only solution that I see at this time is

that the variable x in (let x free in (f x ? g x)) is indeed

shared. If this is not what the programmer intends, he can

simply code ((let x free in f x) ? (let x free in g x)).

Cheers,

Sergio

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

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

Received on Thu Nov 08 2007 - 23:27:25 CET

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