beginner's questions - fix f

[Marcin 'Qrczak' Kowalczyk]

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