on termination

Cagdas Ozgenc co19@cornell.edu
Thu, 8 May 2003 11:43:36 +0300

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

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


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.

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