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
`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 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

`g3`

is equivalent to
`f3`

, that is not the case:
`g3(NaN)`

diverges whereas
`f3(NaN)`

returns 0.
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
-- 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.

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,
comparison,
`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
```
if exp1
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
`exp2`

or
`exp3`

. It seems the decision procedure is total and correct.

To test if a function
`f`

terminates for some particular
input
`x1`

, we define a function
`g(y) = f(x1)`

and check if it terminates for all inputs, using the test described
above.

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://pobox.com/~oleg/ftp/**

oleg-at-pobox.com or oleg-at-okmij.org or oleg-at-computer.org

Your comments, problem reports, questions are very welcome!

Your comments, problem reports, questions are very welcome!

Converted from SXML by SXML->HTML