[Haskell-cafe] There can be only one fix? Pondering Bekic's lemma

[Albert Y. C. Lai]

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.