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.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
