Re: beginner's questions - fix f
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
Marcin 'Qrczak' Kowalczyk wrote:
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.
The latter definition is more likely to give you sharing, but Haskell gives you no such guarantees. There are also implementations that give you sharing for the first definition.
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.
But those algebraic types are recursive! -- Lennart
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)
participants (3)
-
Lars Henrik Mathiesen -
Lennart Augustsson -
Marcin 'Qrczak' Kowalczyk