beginner's questions - fix f
Marcin 'Qrczak' Kowalczyk
24 Jul 2001 13:05:25 GMT
24 Jul 2001 12:04:33 -0000, Lars Henrik Mathiesen <firstname.lastname@example.org> 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
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)
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
> 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 * email@example.com http://qrczak.ids.net.pl/
^^ SYGNATURA ZASTĘPCZA