
It's really not as obscure as it first seems. A fixpoint of a function foo is a value x such that foo x = x. The fix operator tells us one way (not the only way) to generate such a fixpoint: fix foo = foo (fix foo) Note from this equation that (fix foo) is, by definition (!), a fixpoint of foo, since foo (fix foo) is just (fix foo). Consider now any recursive definition: f = ... f ... This can be rewritten as: f = (\f -> ... f ...) f Note that the inner f is bound locally, so we can change names (which I only do for clarity): f = (\g -> ... g ...) f Now note that f is a fixpoint of \g -> ... g ... So all we need is a way to find this function's fixpoint. But from the above we know how to do that, and we are done: f = fix (\g -> ... g ...) -Paul