on termination

[oleg@pobox.com]

Peter Gammie wrote:
> 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, branching-on-zero, and NPFIX. 
Functional applications 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 (a known name, a functional constant). The domain of our
functions consists of integers and a special value 'undefined' (to be
called NaN for short). The reduction rules are as usual, with an
addition
	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.
There are terminating expressions (any expression that never directly
or indirectly mentions NaN always terminates). There are obviously
non-terminating functions, such as f(x) = x + NaN. 

It is also clear that the halting predicate for our language is
decidable. Given an expressing, we examine it and the body of all
involved functions. If we don't find any NaN, we yield TRUE. If we
find a NaN, we "abstractly" interpret our expression. That is, we
execute it step by step until we come across a step that tries to add,
compare, multiply NaN. At this point we yield FALSE. If our abstract
interpreter halts, we yield TRUE. Obviously our abstract interpreter
is just the concrete interpreter with one small change. Because any
sequence of NaN-free reductions in our language is a sequence of
reductions for some primitive recursive function, such sequence must
terminate.

We're a bit running afoul of the requirement:

> I can tell how a given element of the class will behave without
> running it

but then, a decision procedure must take some 'deciding', so to
speak -- if it is non-trivial. We must have a deciding machine. In our
example, the deciding machine is the original machine with a slight
modification.