on termination

[Cagdas Ozgenc]

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

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.

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