From: "Marcin 'Qrczak' Kowalczyk" <qrczak@knm.org.pl> Date: 24 Jul 2001 13:05:25 GMT
24 Jul 2001 12:04:33 -0000, Lars Henrik Mathiesen <thorinn@diku.dk> pisze:
Now, anything that's defined as "x = f x" is called a fixpoint of f. It's possible to prove that there's only one (when f is a Haskell function, at least) so we can talk of 'the' fixpoint.
Not necessarily only one, e.g. any value is a fixpoint of identity function.
But there is one *least* fixpoint wrt. definedness, and it can be effectively found.
My error. I meant to write "only one relevant fixpoint". This was a beginner's question, after all, so I wasn't going to go into too many details.
BTW, a better definition than fix f = f (fix f) is fix f = let x = f x in x because it increases sharing, avoiding recomputation.
And it very obviously constructs a solution to "x = f x" and delivers it. But trying to explain its operational behaviour gets right back to Haskell's builtin recursion, which wasn't what the original poster was trying to understand.
You can define fix without recursion in a typeless lambda calculus:
fix f = (\x -> f (x x)) (\x -> f (x x))
and this can even be stretched to fit Haskell's type system by smart use of algebraic types.
I know. I even posted about it to another thread about two weeks ago. But that loses sharing again, of course. Lars Mathiesen (U of Copenhagen CS Dep) <thorinn@diku.dk> (Humour NOT marked)