On Sat, 17 Mar 2007, Nicolas Frisby wrote:

Bekic's lemma [1], allows us to transform nested fixed points into a single fixed point, such as:

fix (\x -> fix (\y -> f (x, y))) = fix f where f :: (a, a) -> a

The 'fix' on the right hand side is not the standard one (e.g. Control.Monad.Fix), is it?

Nicolas Frisby wrote:

My question is: Given products and a fixed point combinator, can any pure expression be transformed into a corresponding expression that has just a single use of fix?

If yes, has there been any usage of such a transformation, or is it just crazy?

Yes. One use is theoretical and conscious. Facts proven about single recursion automatically carry over to mutual recursions, since the latter can be packaged up as the former. For example, one fact says that regarding the equation x = f x, you can construct the sequence _|_, f _|_, f (f _|_), ..., f^n _|_, ... the terms get closer to a solution for x as you go down the sequence, and under a continuity assumption, you just need omega iterations to get to the fixed point. The same fact automatically applies to the system of equations {y = g z, z = h y}, i.e., the sequence (_|_, _|_), (g_|_, h_|_), (g (h_|_), h (g_|_)), ... gets closer and closer to a solution for (y,z), and under a continuity assumption you just need omega iterations to get to the solution. This is of course the most basic example of facts. There are more advanced facts, such as fusion, leapfrogging, etc. with practical use in code optimization, and they are enjoyed by both single recursion and mutual recursion. (Perhaps it is now clear what is meant by "true product" and why it is required. The above example fact says in general: start your sequence from the bottom. This "bottom" seems a bit ambiguous in the mutual case, since there are two different common ways of tupling up two partial orders. One is the cartesian product, which you probably know how to do, and its bottom is (_|_, _|_). The other is, on top of that --- or shall I say below bottom of that --- insert an extra _|_ below (_|_, _|_), and this is what Haskell 98 does with its (,) type. Clearly, for our theory to work, you want the former, and its probably called the "true product" in contrast to the latter, which is the "lifted product" or "pointed product".) But perhaps the most widespread practical use is a subconscious one. How do you write an interpreter, for a language that supports mutual recursion, in a language that just provides iteration? You introduce a program counter and a stack, then you write just one loop: it dereferences the program counter, does a case analysis, updates stack as necessary, updates program counter as necessary, repeat. You have turned a mutual recursion into a single tail recursion. In an indirect sense it is an application of the basic example theoretical fact above. It is so widespread and yet so subconscious, you cannot avoid it if you use any real computer at all, and yet you hardly think about it, as this is exactly what every existing CPU does.