on termination

[Peter Gammie]

On Thu, 8 May 2003, Cagdas Ozgenc wrote:

> > The class of recursive (total) functions is not recursively enumerable,
> > i.e. not acceptable by a Turing machine. This result can be found in any
> > textbook on recursive function theory (ask me off list and I'll dig up a
> > reference).
>
> You lost me there. I thought recursive class is a subset of recursively
> enumerable class. Perhaps you are referring to a special case.

No, I am saying that you cannot write a program that runs on a Turing
machine that accepts all and only (some representation of) the class of
total functions. You can, of course, write programs that accept subsets of
this class (e.g. the primitive recursive functions) or all of this class
and some more (e.g. Turing-computable functions, incidentally including
some partial functions along the way).

Tony Hoare wrote a paper about this that you might find interesting:

http://portal.acm.org/citation.cfm?id=356606&coll=portal&dl=ACM&CFID=10349987&CFTOKEN=44706211#FullText

> > More interestingly, it is possible to (uniformly) define classes of total
> > functions that are strictly larger than the primitive recursive class - in
> > particular, this is what type theorists spend a lot of time doing. (See,
> > for example, Simon Thompson's book on Type Theory and Functional
> > Programming.)
>
> I have skimmed through the following work.
>
> http://www.math.chalmers.se/~bove/Papers/phd_thesis_abs.html
>
> She claims that it is not possible syntactically detect termination, if the
> recursion is not based on smaller components at each turn. But I think she
> doesn't supply a proof for that.

I believe this statement as it stands is not true; there are functions
that can be proved terminating but do not uniformly reduce the size of an
argument. (Does Ackermann's function serve as a counter example?) Suffice
it to say that Ana's condition is sufficient but not necessary, and is
used in practice as it can be automated. See the work done on termination
analysis in Mercury for variations on this theme:

http://citeseer.nj.nec.com/speirs97termination.html

> > Now, a question of my own: is it possible to uniformly define a class of
> > functions that have a non-trivial decidable halting predicate? The notion
> > of "uniform" is up for argument, but i want to rule out examples like
> > Andrew's that involve combining classes in trivial ways.
>
> You lost me once again. What do you mean, could you please eloborate?

OK:

1. The primitive recursive functions have a trivial termination predicate,
   viz "true". This is also the case for the type theorists' systems I
   have seen.

2. The Turing partially-computable functions have an undecidable
   termination predicate.

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.

Utility? Absolutely none. ;-)

cheers
peter