I'd like to clarify the termination decision procedure. I believe it can take the body of a function in our language and tell if the function terminates for all inputs. This implies that we can decide on termination without evaluating the function on all inputs (whose set is countably infinite). A small clarification: the 'branch-on-zero' statement should have the form "if-nonnegative exp then exp1 else exp2". Because the domain includes 'undefined' (aka NaN), the only functions that terminate for all inputs are those that leave their arguments alone and either propagate them or return constants. For example, the following functions terminate on all inputs f1(x) = x f2(x,y) = y f3(x) = 0 f4(x) = if-nonnegative power(5,125) then x else NaN The following functions will fail to terminate on at least one input: g1(x) = x + x g2(x) = if-non-negative x then x else NaN g3(x) = if-non-negative x*x then 0 else 1 Although it seems that g3 is equivalent to f3, that is not true: g3(NaN) diverges whereas f3(NaN) returns 0. These examples clarify a decision procedure, which can be stated as follows: if a partial evaluation of f(x...z) -- that is, unfolding plus constant propagation -- reduces f() to f1, f2, or f3 types, the function f() terminates on all inputs. Otherwise, there is one value (most likely NaN), that, when passed to f(), will cause it to diverge. Our partial evaluation procedure first unfolds all function calls. That is possible because the call graph does not have direct cycles (NPFIX must be treated as a special node in the call graph). Any operation (multiplication, addition, comparison, NPFIX) on a dynamic value can lead to a non-termination (if that value is NaN). Thus the only operations that can still guarantee termination are "if exp1 then exp2 else exp3" and "NPFIX exp1 exp2 exp3" where exp1 is a constant expression. We can evaluate it. Because it contains only primitive recursive functions, we provably can do that in some finite time. Therefore, we can decide which branch to take and continue to analyze exp2 or exp3. It seems the decision procedure is total and correct.