8
$\begingroup$

I'm working on a proof-checker that can verify termination proofs. The fundamental method it provides for constructing such proofs is to translate the program into primitive recursion. Basically, I provide a combinator $\rho$ typed as:

$\rho: \forall A,B:(A\rightarrow Nat \rightarrow A)\rightarrow (A \rightarrow B)\rightarrow A\rightarrow Nat \rightarrow B$

which, in the notation defined here, constructs $h$ given $f$ and $g$.

Although the term language contains a fixed-point combinator and is therefore Turing-complete, terms that use it have a "tentative" flag in their type that indicate this. The $\rho$ combinator and the fixed-point combinator are the only two language primitives that allow for recursion or looping of any sort (i.e., without either of these two combinators, all you've got is a finite-state machine). Therefore, all terms that are well-typed and non-tentatively typed are primitive recursive.

What I'm wondering is if there are any interesting complexity classes that you can build by starting with primitive-recursive constructions, and adding a finite number of other functions $Nat \rightarrow Nat$, each of which is in R but not in PR, and allowing composition with these functions. It's easy to come up with non-interesting examples of such classes, e.g. "primitive recursion plus the Ackermann function", but I'm looking for any that have sufficiently interesting properties that it would be worth adding the functions which characterize them as admitted axioms in the proof system.

$\endgroup$
5
  • $\begingroup$ Maybe I misunderstood something, but you seem to claim that membership in PR is decidable. It is not (see Rice’s theorem). I’m not sure, but it might be possible if your programs are written in some non-Turing-equivalent programming language. Could you clarify? $\endgroup$ Aug 13, 2010 at 10:59
  • $\begingroup$ ...right, which is what I get for trying to ask coherent math questions at 5:30 AM. The system I'm working in is one based on Luo's Extended Calculus of Constructions. It contains a fixed-point combinator in addition to the above $\rho$ combinator and therefore is Turing-complete, but expressions that invoke it have their types flagged to indicate that they do. But, every well-typed term that is not so-flagged is in PR, because $\rho$ is the only other combinator that provides recursion. $\endgroup$
    – dfranke
    Aug 13, 2010 at 12:50
  • $\begingroup$ So, to rephrase my question without having to go into the gory details of the type calculus: can you get any interesting complexity classes by starting with a system that permits only primitive-recursive constructions, and augmenting it with certain $Nat \rightarrow Nat$ total functions that are not in PR. $\endgroup$
    – dfranke
    Aug 13, 2010 at 12:53
  • $\begingroup$ Could you please edit the original question according to your last comment? $\endgroup$ Aug 13, 2010 at 13:35
  • $\begingroup$ This question appears to be very closely related: mathoverflow.net/questions/46350/… $\endgroup$ Nov 29, 2012 at 21:29

1 Answer 1

7
$\begingroup$

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.

$\endgroup$
4
  • $\begingroup$ Sorry, I answered before your edit to the original question; now I see you already excluded the “PR + Ackermann” case. :-) $\endgroup$ Aug 13, 2010 at 14:08
  • $\begingroup$ Nifty. So the answer is that I don't even need $\rho$ as an axiom: the underlying system is already expressive enough to construct it and much more beyond it, and I need to finish wrapping my brain around the properties of that system. $\endgroup$
    – dfranke
    Aug 13, 2010 at 14:35
  • $\begingroup$ Alright, I get it now. What I was missing before was the essentialness of encoding natural numbers as iterator functions. That's where you get the "potential energy", so to speak, in order to compute complex functions without the need for a recursion operator. Thanks again. $\endgroup$
    – dfranke
    Aug 15, 2010 at 15:33
  • $\begingroup$ The link to the slides no longer works - but they can be still found in the Wayback Machine. $\endgroup$ Mar 10, 2023 at 13:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.