Which abstract machine or language is exactly expressive enough to produce the computable functions?

Question

I'm interested in software verification and therefore only interested in algorithms which always terminate in predictable amount of time and can determine whether the final result is expected or not, hence I think the computable functions are a good place to start as as I understand it these are functions which can be defined using a decidable procedure, i.e. an algorithm which always terminates.

I'm a little familiar with the Chomsky hierarchy, I imagine I would be looking for a language or an abstract machine that is as far up the hierarchy as possible, but does not suffer from the halting problem. However I don't think Linear-bounded Turing machine's are what's needed as these seem to just cut of resources i.e. they are just computers which stop simply because they run out of resources. I think I need something which limits the number of computation steps using logical expressions which can be reasoned with effectively, so by the time the computation finishes we are able to describe something about the final state. I need to be able to reason about cycles too. Could this be pushdown automaton? Are there any other suitable models I've missed?

Answer 1

Your question is a bit unclear, but it seems to me that you are asking for a machine model that gets you exactly the computable total functions. There is no such thing.

The reason is simple: There cannot be an effective enumeration of all computable total functions (because we could diagonalize against it). Any reasonable machine model would give us an effective enumeration, QED. You either need to sacrifice being able to tell whether or not something is a machine in your model, or you need to sacrifice being able to run your machines. Neither are satisfactory.

You might be happy working with the class of primitive recursive functions. There's quite a bit in there, they are all total computable, and you can effectively enumerate them. If you have some specific total computable functions you need in addition (eg the Ackerman function), you can take a finite set of special total computable functions and close it under primitive recursion, and work with that.