I recently read this very nice paper by Venanzio Capretta (Logical Methods in Computer Science, Volume 1, 2005, pages 1-28).  To summarize very crudely: if your termination analysis supports lazy computations (“corecursive functions”) on possibly infinite data structures (“coinductive data”), then you can implement general recursive functions as certain such computations on certain such data structures.  This is important, because the idea works even in a type theory where all functions are required to terminate (and all co-recursive functions are required to be productive; that is, in finite time one must always be able to unfold the infinite data structure the next finite amount).

The remarkable thing Capretta realized is that the only possibly infinite data structure you need is one which we can think of as a list which begins with possibly infinitely many copies of a single symbol $\triangleright$.  This symbol means “the computation is still running”.  If there are only finitely many such symbols, that means the computation is finite, and then the list ends in the result of the computation.  If there are infinitely many $\triangleright$ symbols, that means the computation runs forever (without producing a value).  For example, let’s say we are trying to represent the (terminating) computation of $2^4$ this way.  We will have something of the form:

$\triangleright \cdots \triangleright 16$

Actually, Capretta will write

$\triangleright \cdots \triangleright \ulcorner 16 \urcorner$

This is because the coinductive type for computations that either diverge or converge with a result of type $A$ is $A^\nu$, with (co-inductive) constructors:

$\begin{array}{lll} \triangleright & : & A^\nu \rightarrow A^\nu \\ \ulcorner \cdot \urcorner & : & A \rightarrow A^\nu\end{array}$

Of course, if your computation is (for example) searching for counter-examples to Fermat’s Last Theorem, your computation will look like the following (with an infinite number of $\triangleright$s):

$\triangleright \cdots$

This $A^\nu$ is a rather spartan data structure for computations: all the information about what the computation is doing has been abstracted away, so that we see either only “still thinking” or “done, and here is the answer”.  Why is this enough for encoding general recursive functions in a terminating type theory?  The answer (as I believe I understand it) is that the type $A^\nu$ is the appropriate constructive analog of the more obvious but constructively inappropriate inductive (as opposed to co-inductive) type where you either have a result of type $A$, or something indicating divergence.  This type might be written as a sum-type $A + \uparrow$.  It is inappropriate for modeling general computation in a terminating type theory, because with a sum-type, we can always case split on whether some element $a$ of type $A+\uparrow$ is in $A$ or is the entity representing divergence.  In a constructive logic such as a terminating type theory, this implies we can decide termination of this element $a$, which is not possible in general.  The coinductive type $A^\nu$ is the perfect standin for $A + \uparrow$, because while we cannot case-split on its values, we can co-recursively analyze them, so if a computation does terminate, we can make use of the result.  If it does not, we will co-recursively analyze it forever.

Capretta develops and applies these ideas in a number of interesting ways.  But you’ll have to read his paper to learn more about that, as this post (delayed as it was by the end of the semester) is getting too long already.

1. This technique might be theoretically complete (I don’t know the details), but it’s inconvenient to use in practice. With Coq’s well-formedness conditions on co-fixpoints, many common abstractions aren’t possible. For instance, you can’t write one function in this style whose body calls a bunch of other such functions and then combines their results. Maybe you can get around this by using CPS or some other trick, but it probably wouldn’t be much fun.

2. It should probably also be noted that it’s a rather weak sense in which this gives you general recursion. You might be able to, say, implement mergesort in the typical style using this, but then your mergesort will have a type something like:

sort : {A : Set} -> List A -> D (List A)

So you can give it a list, and it will give you back an answer, but it is not a useful answer unless you can prove that the general recursive algorithm terminates, because ‘unwrap my D (List A) until you find a real answer’ is not, on its own, a total function. You could also, I suppose implement an ‘unwrap at most N times to see if there’s an answer’ function, but that isn’t particularly satisfying.

• Dan,

Well, it seems we could prove a theorem like this, expressing that the function is terminating:

$\forall A:Set.\ \forall l:List A.\ \exists l':List A. (\textit{sort}\ A\ l) \downarrow l'$

(where $x \downarrow a$ means that $x$ converges to value $a$, Definition 3.2 of the paper).

So once we write the general recursive function, we can prove it terminates. I agree with you that it is still not entirely clear to me (probably due to lack of doing some examples in this co-recursive style) how effectively we could program using such functions, whether proved total or not.

• Dan Doel
• Posted March 4, 2010 at 8:10 am