Non-trivial class of functions with a decidable halt

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 NaN

     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

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).

Last updated May 1, 2004

This site's top page is http://okmij.org/ftp/

Converted from SXML by SXML->HTML