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. If the function is strict, the least fixpoint is not very interesting because it's bottom, a value representing nontermination or error. If the function is not strict, bottom is not its fixpoint, so the fixpoint obtained by "x = f x" or "fix f" is more interesting. 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.
fix f = f (fix f)
This looks like a recursive definition again, but if you want a system without explicit recursion you have to disallow this as a function. In such a system, fix is a builtin operator,
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.
Note that operationally, this Haskell version of the fixpoint operator is only sort-of equivalent to a Haskell recursive definition (which is defined in terms of a 'real' fixpoint). That's even clearer with data structures; compare
zeroes = 0 :: zeroes
and
zer_step l = 0 :: l zeroes2 = fix zer_step
zeroes is a circular list with one element, while zeroes2 is an infinite list with all zero elements.
This is the difference between two definitions of fix above. -- __("< Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK