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

From: Claus Reinke <claus.reinke_at_talk21.com>

Date: Sat, 05 May 2007 02:40:19 +0100

*> > choices only propagate outwards out of strict contexts
*

*> That last sentence is not strctly true... ;-)
*

i still think it is!-)

*> two x = [x,x]
*

*>
*

*> The contexts the ``x'' inhabits in the right-hand side of ``two''
*

*> are non-strict:
*

the strictness of sub-contexts changes during reduction, as

demands are propagated and subexpressions move around (*)

*> coin = 0
*

*> coin = 1
*

*>
*

*> and you get:
*

*>
*

*> -- two coin
*

*> -- Result: [0,0] ? ;
*

*> -- Result: [1,1] ? ;
*

*>
*

*> ``as if the choice had been made at call-time''
*

i suspect that the 'as if' is the issue here - it is not bi-directional:

- shared choices, *if they are made*, behave 'as if the choices

*for those parameters* had been made at call-time'

- call-time choice *for all parameters* of a function call ignores

the strictness of the function, and *can make more choices*

than strictly necessary

in other words, sharing choices forced by strictness is more precise/

makes fewer choices than call-time choice irrespective of strictness.

as for the strict contexts: when putting 'two coin' into an interactive

Curry system, the combination behaves somewhat like 'print (two coin)',

where the 'print' traverses the result of 'two coin', thereby providing the

strict context that forces the choices for the parameter embedded into

the list. since the choices were shared, we get the 'as if'. (*)

my two coins;-)

claus

(*) i tend to find the language-level operational semantics of call-by-need

lambda calculus [1] by Ariola et al a most useful starting point for

discussing sharing without resorting to external heaps:

http://citeseer.ist.psu.edu/132534.html

if one starts with their standard call-by-need reduction, and adds a

rule that propagates choices out of strict positions in evaluation

contexts:

E[ a?b ] -> E[ a ] ? E[ b ]

one gets derivations roughly like this one:

let coin = 0?1 in

let two x = [x,x] in

two coin

-beta-need-> -- let-V in [1]

let coin = 0?1 in

let two x = [x,x] in

(\x->[x,x]) coin

-beta-bind-> -- let-I in [1]

let coin = 0?1 in

let two x = [x,x] in

let x = coin in

[x,x]

-lift-choice-> -- print traversal demands x, which demands coin,

-- which triggers propagation of shared choice

let coin = 0 in

let two x = [x,x] in

let x = coin in

[x,x]

?

let coin = 1 in

let two x = [x,x] in

let x = coin in

[x,x]

-beta-need->* -- let-V in [1]

let coin = 0 in

let two x = [x,x] in

let x = coin in

[0,0]

?

let coin = 1 in

let two x = [x,x] in

let x = coin in

[1,1]

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

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

Received on So Mai 06 2007 - 17:56:00 CEST

Date: Sat, 05 May 2007 02:40:19 +0100

i still think it is!-)

the strictness of sub-contexts changes during reduction, as

demands are propagated and subexpressions move around (*)

i suspect that the 'as if' is the issue here - it is not bi-directional:

- shared choices, *if they are made*, behave 'as if the choices

*for those parameters* had been made at call-time'

- call-time choice *for all parameters* of a function call ignores

the strictness of the function, and *can make more choices*

than strictly necessary

in other words, sharing choices forced by strictness is more precise/

makes fewer choices than call-time choice irrespective of strictness.

as for the strict contexts: when putting 'two coin' into an interactive

Curry system, the combination behaves somewhat like 'print (two coin)',

where the 'print' traverses the result of 'two coin', thereby providing the

strict context that forces the choices for the parameter embedded into

the list. since the choices were shared, we get the 'as if'. (*)

my two coins;-)

claus

(*) i tend to find the language-level operational semantics of call-by-need

lambda calculus [1] by Ariola et al a most useful starting point for

discussing sharing without resorting to external heaps:

http://citeseer.ist.psu.edu/132534.html

if one starts with their standard call-by-need reduction, and adds a

rule that propagates choices out of strict positions in evaluation

contexts:

E[ a?b ] -> E[ a ] ? E[ b ]

one gets derivations roughly like this one:

let coin = 0?1 in

let two x = [x,x] in

two coin

-beta-need-> -- let-V in [1]

let coin = 0?1 in

let two x = [x,x] in

(\x->[x,x]) coin

-beta-bind-> -- let-I in [1]

let coin = 0?1 in

let two x = [x,x] in

let x = coin in

[x,x]

-lift-choice-> -- print traversal demands x, which demands coin,

-- which triggers propagation of shared choice

let coin = 0 in

let two x = [x,x] in

let x = coin in

[x,x]

?

let coin = 1 in

let two x = [x,x] in

let x = coin in

[x,x]

-beta-need->* -- let-V in [1]

let coin = 0 in

let two x = [x,x] in

let x = coin in

[0,0]

?

let coin = 1 in

let two x = [x,x] in

let x = coin in

[1,1]

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

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

Received on So Mai 06 2007 - 17:56:00 CEST

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