Ex 9.9 in Paul Hudak's book

Paul Hudak paul.hudak@yale.edu
Mon, 01 Apr 2002 10:41:12 -0500

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 ...)