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 . 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 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 this way. We will have something of the form:
Actually, Capretta will write
This is because the coinductive type for computations that either diverge or converge with a result of type is , with (co-inductive) constructors:
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 s):
This 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 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 , or something indicating divergence. This type might be written as a sum-type . 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 of type is in 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 , which is not possible in general. The coinductive type is the perfect standin for , 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.