Changes between Version 18 and Version 19 of NestedCPR


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

--

Legend:

Unmodified
Added
Removed
Modified
  • NestedCPR

    v18 v19  
    4949 2. The convergence information a function is what holds always. This would ineffect prevent `<S>tm()` from happening. 
    5050 
    51 The first is stronger, but more involved. So currently, we go with the second one. 
     51Implementation implications: 
     52 1. For the first one, We need to be careful when `lub`’ing: If one branch is lazy, but not absent in an argument or free variable), and the other branch is strict, then even if both branches claim to terminate, we need to remove the termination flag (as one had the termination under a stronger hypothesis as the hole result). Feels inelegant. 
     53 2. For the second one, we’d need a different `both` for functions and case-expressions: For function applications, convergence in the first argument is not affected by (possible) divergence in the second argument. For case expressions, it has to be! Also, data constructors with strict fields, including `I# _` must not be terminating...sounds like a show-stopper. 
    5254 
    53 This means that {{{t `bothRes` m}}} is still `t`! 
     55What is the semantics for bottom? 
    5456 
    5557=== join points ===