Lambda the Ultimate

you need to show that there is some well-order along which f always shrinks its argument.

And for primitive recursiveness, even this is not enough: you need that the well-foundedness of the measure can be proven using a limited notion of induction. Sufficiently tangled unfolds over tree structures, such as those you get from recursive path orderings, are not primitive recursive.

Cf. Dershowitz, 1987, Termination of rewriting (long scanned journal article).

Postscript Link fixed, thanks Blaisorblade.

That link is broken. Did you refer to this paper [1]?
[1] http://www.cs.tau.ac.il/~nachumd/papers/termination.pdf

Anyway, thanks for both answers.

Given a function that recurses on itself, do a partial CPS transform so that it only ever recurses on itself with tail calls. Then, convert the recursive calls to codata returns, so that the function either returns TheAnswer or StillWorking with enough parameters to describe the recursive call / continuation state. This codata can be built with an unfold and can be collapsed back down to the final answer with a fold.

...is to use the constructive lift monad, the coinductive type T(A) ≡ να. A + α. The intuition is that this type either tells you a value of type A, or tells you to compute some more and try again. Nontermination is modelled by the element which never returns a value, and always keeps telling you to compute some more.

Our goal is to construct a general fixed-point combinator μ(f : TA → TA) : 1 → TA, which takes an f and then produces a computation corresponding to the fixed point of f. To fix notation, we'll take the constructors to be:

roll : A + TA → TA
unroll : TA → A + TA 

Since this is a coinductive type, we also have an unfold satisfying the following equation:

unfold(f : X → A + X) : X → TA ≡ roll ○ (id + (unfold f)) ○ f 

First, we will explicitly construct the bottom element, corresponding to the computation that runs forever, with the following definition:

⊥ : 1 → TA ≡ unfold inr

This definition just keeps telling us to wait, over and over again. Now, we can define the fixed point operator:

μ(f : TA → TA) : 1 → TA  
μ(f) ≡ (unfold (unroll ○ f)) ○ ⊥

What this does is to pass bottom to f. If f returns a value, then we're done. Otherwise, f returns us another thunk, which we can pass back to f again, and repeat.

Of course, this is exactly the intuition behind fixed points in domain theory. Lifting in domains is usually defined directly, and I don't know who invented the idea of defining it as a coinductive type. I do recall a 1999 paper by Martin Escardo which uses it, and he refers to it as a well-known construction in metric spaces, so probably the papers from the Dutch school of semantics are a good place to start the search.

This construction has seen a renewed burst of interest in the last few years, since it offers a relatively convenient way to represent nonterminating functions in dependent type theory.

I think this boils down to the same thing, but the way I heard the story (in Meijer and Hutton's Bananas in Space paper) is like this:

fix f = foldr ($) undefined (repeat f)

That is, to construct fix f, first build an infinite stream of fs (an unfold), and then replace each cons with application (a fold).

Any paper that defines an operational semantics using inference rules demonstrates a third way that unfolds can express general recursion, even though it usually isn't apparent.

A reduction relation R(x,y) is a mapping, or a set of pairs, from input terms x to output terms y. To keep it simple, we'll assume a big-step operational semantics, so the output terms are always final, unreducible values.

Using the inference rules as a guide, define F(R_n) = R_n + { all the new conclusions reachable given the conclusions in R_n }. (A "conclusion" is a pair (x,y), which means "x reduces to y".) The fixed point R of F is the union of a completed unfold over F, starting at R_0 = {}.

Usually every R_n is computable. (This is certainly the case when R defines a computable operational semantics.) And even though the limit R isn't computable, you could write a very slow interpreter that, for any given term x, computes R_n's until R_n(x,y) is true (equiv. (x,y) is in R_n) for some y. It will halt for precisely the same x's that a recursive interpreter would, and give the same answers.