beginner's questions - fix f

Lars Henrik Mathiesen thorinn@diku.dk
24 Jul 2001 13:54:16 -0000


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