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