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?
Is the class of primitive recursion functionals equivalent to the class of functions which Foetus proves to terminate?
lo.logic;computability;functional programming
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  Tdata 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 BNote 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 Ainterp-term zero    = 0 interp-term succ    = \n  n + 1interp-term k       = \x y  xinterp-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. 