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?]