on termination

[oleg@pobox.com]

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.