Catamorphisms and anamorphisms = general or primitive recursion?

By combining catamorphisms and anamorphisms, can one write only primitive recursive functions or any general recursive function? Do you know a good reference discussing that?

I was surprised by reading that "combining anamorphisms and catamorphisms [...] leads to general recursion" in an ICFP paper [1]. I would have expected to see "primitive recursion" there, and no reference is given for the statement.
Neel Krishnaswami states, on L-t-U forums [2], only that:
"Better still, a fold and an unfold composed together can describe any primitive recursive function."

I also skimmed again "Functional programming with bananas, lenses, envelopes and barbed wire", which builds only examples of primitive recursion - it does not go as far as Neel Krishnaswami.

[1] "Boxes Go Bananas: Encoding Higher-Order Abstract Syntax with Parametric Polymorphism", Geoffrey Washburn and Stephanie Weirich, ICFP 2003.
[2] http://lambda-the-ultimate.org/classic/message9257.html

Fold + Unfold

...gives you general recursion. The basic reason is that for inductive types, unfolds can diverge, and for coinductive types, folds can diverge. For a simple example, consider the natural numbers:

type nat = Z | S of nat

let rec fold f = function
  | Z -> f None
  | S n -> f (Some (foldnat f n))

let rec unfold f seed =
  match f seed with
  | None -> Z
  | Some seed' -> S(unfold f seed')

(* Creating an infinite loop *)

let loop () =
  unfold (fun () -> Some ()) ()

Given a total f, the fold will always terminate. However, the same is not true of unfold, as the loop example demonstrates. To ensure termination of the unfold, you need to show that there is some well-order along which f always shrinks its argument.

By neelk at Tue, 2011-06-14 14:36 | login or register to post comments

Provable shrinkings

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.

By Charles Stewart at Wed, 2011-06-15 11:31 | login or register to post comments

Broken link

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.

By Blaisorblade at Wed, 2011-06-15 23:13 | login or register to post comments

"Constructive" argument

neelk and Charles, your answers are along a power/termination axe: fold+unfold is more expressive than primitive recursion because they can express bigger functions or slower to terminate computations.

This is interesting, and an elegant way to answer the original question, but still it doesn't explain, given a recursive function, how to express it with fold+unfold.

I feel a bit lazy asking this question; It seems that with a little effort, it could be figured. Yet I enjoy seeing this topic discussed here and am confident you'll provide additional, interesting insights.

By gasche at Thu, 2011-06-16 07:42 | login or register to post comments

Hand waving

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.

By Matt M at Thu, 2011-06-16 13:33 | login or register to post comments

The easy way...

...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.

By neelk at Thu, 2011-06-16 16:07 | login or register to post comments

Bananas in space

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).

By jeremygibbons at Mon, 2011-06-20 22:37 | login or register to post comments

Yet a third way

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.

By Neil Toronto at Fri, 2011-06-17 16:26 | login or register to post comments

Lambda the Ultimate

User login

Navigation