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

[Lennart Augustsson]

Using a single fix sounds possible.
First transform your program (by lambda lifting) to a program with  
only global definitions, and then tuple them up and and use fix.

The c with a hacek, č, is Unicode character 010D.

	-- Lennart


On Mar 18, 2007, at 03:01 , 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
>
>
>
> This depends on having "true products," though I'm not exactly sure
> what that means. Mutual recursion can also be described with recursion
> and products
>
> 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,
> Nick
>
>
> [1] - 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?]
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe