on termination

[Peter Gammie]

> That's a good example. So how much can we expand this class? Is it possible
> to cover all recursive languages, or is there a theorem that says this is
> not possible?

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

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

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.

cheers
peter