Re: call-time choice vs partial application?

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 Sun May 06 2007 - 17:56:00 CEST

This archive was generated by hypermail 2.3.0 : Mon Sep 23 2019 - 07:15:06 CEST