First of all, it’s certainly possible to obtain some intermediate class by taking a language that only computes PR functions (say, an imperative programming language using only for loops) and adding any total computable but non PR function (e.g., Ackermann’s function). The resulting language L is non-universal, because it only computes total functions: you can still construct a computable but non-L-computable function by diagonalisation. However, L is clearly more powerful than the original language.
As for “interesting”, I guess it really depends on what you mean by that.
If “interesting” means “of practical use”, then one could answer that all computable functions of practical use are PR, since a non-PR function requires an amount of time to compute that is not, in turn, PR. Considering that time bounds such as 2n, 22n, 222n, …, are all PR, you see that there isn’t much hope to compute non-PR functions for large values of n.
If “interesting” means “logically interesting”, then I think the answer is “yes”. I’m somewhat familiar with Girard’s System F (also called “second order λ-calculus” or “polymorphic λ-calculus”), described for instance in Girard’s Proofs and Types (freely available here). The functions that can be computed in F are “exactly those which are provably total in [second order Peano arithmetic]” (page 123), and among these we have Ackermann’s function. There is an explicit λ-term for it on these slides (page 20).
If I recall correctly, the standard calculus of constructions includes System F and only computes total functions, so it also provides an example.
No comments:
Post a Comment