[Haskell-cafe] There can be only one fix? Pondering Bekic's lemma
nicolas.frisby at gmail.com
Sat Mar 17 23:01:07 EDT 2007
Bekic's lemma , 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
This depends on having "true products," though I'm not exactly sure
what that means. Mutual recursion can also be described with recursion
f = \a -> ... g a ...
g = \b -> ... f b ...
can be defined as
(f, g) = fix (\knot -> \a -> ... (snd knot) a ..., \b -> ... (fst knot) b ...)
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?
If no, could you provide a counter-example?
Thanks for playing along,
 - Bekic has an entire book, but the most available reference for
this I found is Levent Erkök's thesis regarding MonadFix/mfix (pgs 16
and 141). [Also, I cannot figure out how to get the proper symbol
above that c in Bekic... sorry about that. I'd appreciate if someone
told me how; does Unicode even have it?]
More information about the Haskell-Cafe