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