Changes between Version 17 and Version 18 of NestedCPR


Ignore:
Timestamp:
Jan 9, 2014 9:28:43 AM (14 months ago)
Author:
nomeata
Comment:

more on converges

Legend:

Unmodified
Added
Removed
Modified
  • NestedCPR

    v17 v18  
    4141 * A recursive function can have a CPR-beneficial recursive call that makes CPR worthwhile, even if it does not help at the initial call. But it is also not unlikely that the recursive call is a tail-call, and CPR-ing has zero effect on that. Then it all depends on the external call. 
    4242 
     43=== Converges detection === 
     44 
     45Nested CPR is only sound if we know that the nested values are known to converge for sure. The semantics is clear: If `f` has CPR `<...>m(tm(),)`, then in the body of `case f x of (a,b)`, when entering `a`, we are guaranteed termination. 
     46 
     47What is the semantics of an outer `t`? Given `f` with CPR `<L>tm()` and `g` with CPR `<S>tm()`? Does the latter even make sense? If so, should `f undefined` have CPR `m()` or `tm()`? Two possibilities: 
     48 1. The convergence information a function is what holds if its strictness annotations are fulfilled: So if `g x`  has `tm()` if `x` has `t` (possibly because it has previously been evaluated by the caller), otherwise `m()`. `f x` always has `m ()` (presumably because `x` is _never_ entered when evaluating `f`. 
     49 2. The convergence information a function is what holds always. This would ineffect prevent `<S>tm()` from happening. 
     50 
     51The first is stronger, but more involved. So currently, we go with the second one. 
     52 
     53This means that {{{t `bothRes` m}}} is still `t`! 
     54 
    4355=== join points === 
    4456