Is the class of primitive recursion functionals equivalent to the class of functions which Foetus proves to terminate?

Question

Foetus, if you have not heard of it, can be read up on here. It uses a system of 'call matrices' and 'call graphs' to find all 'recursion behaviors' of recursive calls in a function. To show that a function terminates it shows that all the recursion behaviors of recursive calls made to a function obey a certain 'lexicographic ordering'. It's termination checker allows all primitive recursive functions and functions such the Ackermann function. Basically it allows multi-argument primitive recursion. This is also basically the the termination checker of Agda; I believe that Coq has some similar facilities as well though perhaps more general.

From reading the paper "Total Functional Programming" by D.A. Turner. He explains that his proposed language would be able to express all "primitive recursive functionals" as seen in System T studied by Godel. He goes on to say that this system is "known to include every recursive function whose totality can be proved in first order logic".

Dose Foetus allow all primitive recursive functionals? If so does it allow functions which are not primitive recursive functionals? Can a citation be provided for the answer to this? (this is not actually necessary as I'm just interested; it's just that some reading marital on the matter would be nice)

Bonus question: Primitive recursive functionals have a very concise definition in terms of combinators: typed S and K (that can't express the fixed point combinators), zero, the successor function, and the iteration function; that's it. Are there other more general such languages which have such a concise definition and in which all expressions terminate?

Answer 1

Yes, the Foetus checker can typecheck everything in Goedel's T. You can show this by using the checker to show that the iteration operator in T is terminating. For example, the following definition will work:

$$ \begin{array}{lcl} \mathit{iter} & : & A \to (A \to A) \to \mathbb{N} \to A \\ \mathit{iter} \;i \;f \;0 & = & i \\ \mathit{iter} \;i \;f \;(n+1) & = & f\;(\mathit{iter} \;i \;f \;n) \end{array} $$

This is very easy for the Foetus checker (or most any other termination checker) to check, because it is an obviously structurally recursive definition.

Agda and Coq both permit proving termination of functions that go far beyond what is provably total in first-order arithmetic. The feature which enables this is that they permit defining types by recursion on data, which is called "large elimination". (In ZF set theory, the axiom scheme of replacement serves roughly the same purpose.)

An easy example of something that goes beyond T is the consistency of Goedel's T itself! We can give the syntax as a datatype:

data T : Set where 
   N : T 
   _⇒_ : T → T → T

data Term : T → Set where 
   zero : Term N
   succ : Term (N ⇒ N)
   k    : {A B : T} → Term (A ⇒ B ⇒ A)
   s    : {A B C : T} → Term ((A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C)
   r    : {A : T} → Term (A ⇒ (A ⇒ A) ⇒ N ⇒ A)
   _·_  : {A B : T} → Term (A ⇒ B) → Term A → Term B

Note that the type dependency permits us to define a datatype of terms containing only the well-typed terms of T. We can then give an interpretation function for the types:

interp-T : T → Set 
interp-T N       = Nat 
interp-T (A ⇒ B) = (interp-T A) → (interp-T B)

This says that N should be the Agda natural numbers, and T's arrow should be interpreted as the Agda function space. This is a "large" elimination, because we define a set by recursion on the structure of the datatype T.

We can then define an interpretation function, showing that every term of Goedel's T can be interpreted by an Agda term:

interp-term : {A : T} → Term A → interp-T A
interp-term zero    = 0 
interp-term succ    = \n → n + 1
interp-term k       = \x y → x
interp-term s       = \x y z → x z (y z)
interp-term r       = Data.Nat.fold 
interp-term (f · t) = (interp-term f) (interp-term t)

(I don't have Agda on this machine, so there are doubtless some missing imports, fixity declarations, and typos. Fixing that is an exercise for the reader, who can also be an editor, if they like.)

I don't know what the consistency strength of Agda is, but Benjamin Werner has shown that the Calculus of Inductive Constructions (Coq's kernel calculus) is equiconsistent with ZFC plus countably many inaccessible cardinals.

Answer 2

As means of clarification, I should note that Foetus is developed by Andreas Abel, who also developed the original termination checker for Agda, and worked on more advanced termination techniques since.

The answer to your question might be a bit disappointing: the class of functions from $\mathbb{N}$ to $\mathbb{N}$ is exactly the functions that can be defined in system $\mathrm{F}$. The reason for this: the aforementioned class is equal to the provably terminating functions in Second Order Arithmetic ($\mathrm{PA}^2$) which in turn is equal to the functions definable in system $\mathrm F$ (see e.g. Proofs and Types, chapter 11). Furthermore, if you remove the polymorphism, then you fall down to functions definable in $\mathrm{PA}$, which happens to coincide with those definable in system $\mathrm{T}$.

Again, the reson for this is that the decrease captured by the "call matrices" is provably well-founded, and that proof can be carried out entirely in $\mathrm{PA}$.

However, this doesn't mean that Foetus is not more useful than system $\mathrm{T}$! In practice, more complex termination analyses are required to be able to accept certain presentations of computable functions. You don't want to have to do a complicated proof in Peano Arithmetic every time you write a unification function, for example. So in this respect, Foetus is very powerful, and allows you to define functions in a way which wouldn't be accepted by either Coq, Agda or any other common proof system.

Answer 3

If by primitive recursive functionals you mean primitive recursive functions and you know that Foetus contains the Ackermann function then Foetus does not coincide with the class of p.r. functions as the Ackermann function is not primitive recursive. This was shown by Ackermann and later a simplified proof was given by Rosza Peter in "Konstruktion nichtrekursiver Funktionen" 1935 (unfortunately only in German as far as I know).

If you look for larger classes of recursive functions that are guaranteed to terminate which might coincide with the class of functions captured by Foetus then some other work of Rosza Peter might interest you.

The Ackermann function is contained in the class of multiple recursive functions as defined by Rosza Peter in "Uber die mehrfache Rekursion" 1937. Informally, the idea behind multiple recursion is that you can have multiple recursive variables which can change after a recursive step. For example $f(a,b)$ might call $f(a,b-1)$ or $f(a-1,b)$.

Yet a stronger class is given by the concept of transfinite recursion described in "Zusammenhang der mehrfachen und transfiniten Rekursion" by Rosza Peter. For transfinite recursion you have one recursive variable which can call predecessors w.r.t. to a special ordering $<$

For example, you can interpret an integer as a pair of integers and use the ordering $$ (a,b) < (c,d) \iff ( a < c \wedge b \leq d ) \vee ( a \leq c \wedge b < d )$$ This can be generalized for triples of integers and so on. Peter calls these orderings $\omega^2, \omega^3$ and so on. You can go one step further and interpret an integer as an arbitrary number of integers. Let $p_i$ be the $i$-th prime number. Then we can consider $z = p_1^{n} \cdot p_2^{x_1} \cdot p_3^{x_2} \cdot \dots$ where $n$ denotes the number of integers encoded in $z$ and the $x_i$'s contain the resp. value. She denotes an ordering for such a list of integers as $\omega^\omega$ and shows by diagonalization that this kind of recursion is stronger than multiple recursion. However, I'm not sure if there is a syntactical characterization of this class.

[edit] Primitive recursive functions are not the same as primtive recursive functionals as noted in the comment below. Yet I think one could transfer the concept of transfinite recursion to functionals. However, it isn't clear whether it still is more powerful w.r.t. a functional setting.