There are numerous examples of models of computation in which all programs halt, for example primitive recursion. Are there (non-trivial) examples of models in which only some programs halt, but the halting problem is still decidable? Does the decision procedure need to lie outside of the original model itself? EDIT: Carl Mummert gives very good example of a model of computation that has this property. But the example of polynomially clocked Turing machines is weaker than primitive recursion. Are there examples which are stronger than primitive recursion?