9
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ On Agda vs Coq: I always read Agda's termination checker to be more advanced and accepts more functions, yours is the first claim to the contrary (this is a good rule of thumb when comparing Agda to Coq, except for Agda's lack of tactics: Agda is more researchy and open to extensions whose stability is less established). Andreas Abel has been working on even more advanced termination checkers based on sized types, see his work on MiniAgda and also this paper. $\endgroup$ – Blaisorblade Jan 14 '14 at 13:50
  • $\begingroup$ There is "accept more function definitions" and "have a larger class of computable functions". The two are incomparable. Agda wins on the first count, but Coq clearly wins on the second. $\endgroup$ – cody Jan 14 '14 at 19:30
  • $\begingroup$ I should clarify that I have not used Coq at all and Agda only a little. It seemed that from what little I read Coq was capable of defining a wider class of computable functions but I did not know so I said "I believe that Coq has some similar facilities as well though perhaps more general"; "belive" and "perhaps" were used to convey that I did not know. $\endgroup$ – Jake Jan 15 '14 at 0:04
7
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Note that you haven't used large elimination in your example. Large elimination doesn't actually add computational power. Impredicativity does: system F doesn't have the former, but can express functions not expressible in system T. $\endgroup$ – cody Jan 14 '14 at 16:46
  • $\begingroup$ @cody: The interp-T function computes a set from a term, which looks like a large elimination to me! It is definitely the case that large eliminations add power: Martin-Loef type theory can't even derive inconsistency from 0=1 without a large elimination. (To see this, note that without universes/large eliminations you can erase all dependencies and get a simply typed term: this is what Harper and Pfenning did in their adequacy proof for LF.) $\endgroup$ – Neel Krishnaswami Jan 14 '14 at 20:37
  • $\begingroup$ I'm sorry: yes the interp-T function does indeed use large elimination. I also agree that proving 0 != 1 does indeed require it. However, defining computable functions is not the same thing as proving mathematical statements. My answer clarifies this a bit. The pure Calculus of Constructions, for example, cannot prove 0 != 1. It can, however, define the Ackermann function with relative ease. $\endgroup$ – cody Jan 14 '14 at 22:01
  • $\begingroup$ This shows that Agda is more general sense it can write an interpreter for system T but does it does not show weather or not Foetus, a language which is not dependently typed, is more general. Can Foetus do this? Would Agda still be able to do this if not for "large elimination"? $\endgroup$ – Jake Jan 14 '14 at 23:51
  • 1
    $\begingroup$ Agda's documentation says its termination checker uses the Foetus algorithm. If you took T, and extended it with pattern matching and recursive definitions checked by Foetus, you would not be able to write an interpreter for T in it. In fact, you would not change the functions computable by T at all -- all of the termination orders Foetus computes are provably well-founded in Peano arithmetic. (See cody's answer.) The Foetus algorithm lets you write more definitions, without changing the set of functions you can compute. Agda's large eliminations actually increase the set of functions. $\endgroup$ – Neel Krishnaswami Jan 15 '14 at 9:55
3
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ how can a class of functions which are provably terminating (PA^2) be equivalent to the class of functions in system F which are not provable to terminate as far as I know? Also I don't understand how you are answering me question. Are you saying system T has a larger class of computable functions or are you saying that foetus is? I think there was a leap in your logic that expected I had more background than I actually do. Also the link you provided seems to lead to a bad page that does not render correctly. $\endgroup$ – Jake Jan 15 '14 at 0:02
  • $\begingroup$ Functions in system F all terminate. Foetus captures a larger class of computable functions than system T, but "by accident", if you remove polymorphism, then Foetus only captures exactly system T. Can you tell me which link doesn't work for you? (and which browser you are using :) $\endgroup$ – cody Jan 15 '14 at 18:12
1
$\begingroup$

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.

$\endgroup$
  • 2
    $\begingroup$ the class of primitive recursive functionals of finite type is more general than the class of primitive recursive functions. It can express the Ackermann function for instance and can be seen in Godel's system T. $\endgroup$ – Jake Jan 14 '14 at 23:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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