The problem has been stated by Peter Gammie in his May 2003 message to the Haskell-Cafe mailing list:
What I want: a class of functions that don't all terminate, don't all not terminate, and furthermore I can tell how a given element of the class will behave without running it. It must have at least some expressiveness; this is up for grabs, but it'll have to encompass at least primitive recursion to be interesting.
Let us consider a first-order language of functions defined with
the help of addition, multiplication, ``if-nonnegative exp then exp1
else exp2'', and
NPFIX. Functional applications and compositions
are allowed provided they use the names of previously defined functions.
(NPFIX n) is the n-th Church numeral (aka fold):
NPFIX n f seed --> f (f ... (f seed)) n times (n>=0) seed otherwise
The second argument of
NPFIX is the name of a
previously defined function. The
domain of our functions consists of integers and of a special value
undefined (to be called
NaN for short). The
usual reduction rules are extended with
NaN + x -> NaN + x for any
x, etc. That is, any operation with
NaN leads to non-termination.
The language obviously includes every primitive recursive function.
Some functions in the language terminate for every input: e.g.,
f(x) = 1+2 . Some functions, such as
f(x) = x + NaN, never terminate. There are many functions
that terminate only on some inputs.
Our class of functions admits a decidable termination decision
procedure: a decidable
halt. The decision procedure takes
the description of a function in our language and tells if that
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). In the following we describe the termination
decision procedure. Obviously the procedure cannot be implemented in
our language itself.
Because the domain includes 'undefined' (aka
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
f1(x) = x f2(x,y) = y f3(x) = 0 f4(x) = if-nonnegative power(5,125) then x else NaNThe 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 1Although it might seem that
g3is equivalent to
f3, that is not the case:
These examples clarify the decision procedure, which can be stated
as follows: if a partial evaluation of the body of the function
f(x...z) -- that is, unfolding plus constant propagation
f3 types, the function
f() terminates on all
inputs. Otherwise, there is one value (most likely
that, when passed to
f(), will cause it to diverge.
To be more precise, 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,
NPFIX) on a dynamic value can lead to
non-termination (if that value is
NaN). Thus the only
operations that can still guarantee termination are
then exp2 else exp3 and
NPFIX exp1 exp2 exp3 where
exp1 is a constant expression. We can ``symbolically''
evaluate it to obtain either an integer result or
NaN. Because the expression involves only primitive recursive functions,
we can provably evaluate it in finite time. Therefore, we can decide
which branch to take and continue to analyze
exp3. It seems the decision procedure is total and correct.
To test if a function
f terminates for some particular
x1, we define a function
g(y) = f(x1)
and check if it terminates for all inputs, using the test described
This page is a compilation of two messages Re: on termination posted on the Haskell-Cafe mailing list on Thu, 8 May 2003 20:01:54 -0700 and Fri, 9 May 2003 11:33:34 -0700 (PDT).
This site's top page is http://okmij.org/ftp/
Converted from SXML by SXML->HTML