Changes between Version 6 and Version 7 of Commentary/Compiler/StrictnessAnalysis/KirstenNotes


Ignore:
Timestamp:
Oct 26, 2006 10:20:03 AM (7 years ago)
Author:
kirsten
Comment:

more notes on linearity

Legend:

Unmodified
Added
Removed
Modified
  • Commentary/Compiler/StrictnessAnalysis/KirstenNotes

    v6 v7  
    1 = Linearity = 
     1= ~~Linearity~~ Patent nonsense = 
    22 
    33Instead of: 
     
    4040}}} 
    4141because it's called more than once. We really want the demand to reflect that (f 1) is called only once and (f 3) is called only once, but it doesn't. So it doesn't seem like we can figure out what we need to know just by looking at the demand on f. 
     42 
     43= Linearity == 
     44The real solution is to distinguish call demands from product demands. Consider again: 
     45{{{ 
     46let f = \ x. \ y. ... in 
     47  ...(f 1 2)...(f 3 4)... 
     48}}} 
     49The demands placed on {{{f}}} by the first and second call get bothed together to yield {{{SM(SM(T))}}}. But this is incorrect. Consider: 
     50{{{ 
     51let f = \ x. \ y. ...  
     52    frob = f 1 in 
     53  ...(f 1 2)...(frob 2)...(frob 3)... 
     54}}} 
     55Here, the demands placed on {{{f}}} by the body of {{{frob}}} and by the call to {{{f}}} in the {{{let}}}-body get bothed together: {{{S1(T) & S1(S1(T)) = SM(SM(T))}}}. Note that this is the same as the demand placed on {{{f}}} above, yet we want to distinguish between the two situations, because in the first example, the inner lambda in {{{f}}}'s rhs is only called once.  
     56 
     57The solution is to treat call demands and product demands differently, and to define the {{{both}}} function for call demands to have the same behavior as {{{lub}}}. Then in the first example, {{{f}}} has demand {{{SM(S1(T))}}} placed on it, and in the second, {{{SM(T)}}}. This is what we want; now, if {{{f}}} has demand {{{D(D(T)}}} placed on it, that implies {{{f}}} is always called with two arguments.