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

### Last updated May 1, 2004

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

oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!

Converted from SXML by SXML->HTML