Re: Please explain: Monad.ST, Monad.Fix and recursive do.
- From: Joachim Durchholz <jo@xxxxxxxxxxxxx>
- Date: Sat, 09 Jul 2005 12:10:49 +0200
Paul Johnson wrote:
What is Monad.Fix about, and how is it related to this recursive do stuff? I thought I had some kind of handle on what a Least Fix Point is (its the smallest set X for some function f such that f X == X), but I don't see what that has to do with programming.
Your notion of a Least Fixed Point is correct.
Let me try a rather vague introduction to the topic (being precise would require all kinds of formal definitions where I'd probably get the details wrong).
The relationship with programming is that it's a way to define the value of a recursive function without resorting to step-by-step evaluation tactics. (Language designers often want to avoid step-by-step evaluation tactics because such a definition of the language semantics tends to nail down more implementation details than necessary.)
Least Fixed Points are also helpful when thinking about really hard problems. For example, when defining equality over possibly circular structures. At the most abstract level, equality can be defined like this:
A = B if and only if:
1) A and B are of equal type
2) If that type is a primitive type,
A and B are in the equality relationship defined for that type
3) If that type is a record type,
the fields of A and B are equal
4) If that type is a reference type,
the referred-to items are equal.The problem here is case (4): the references may "bend back" to the original A and B, and you end up with a nonsensical definition.
Now you interpret the above definition as a function f: Set [value] -> Set [value]
If you take an initial value (i.e. a set with a single value) and repeatedly apply the function, you get
f (f (f (f (.... (initial_set) ....)))
The repeated application should stop when applying the function discovers no new values, i.e. if
f (f (x)) = f (x)
or
f(x) = x
which is exactly the definition of a fixed point.
Now the above definition of equality would also be satisfied if we simply said "everything is equal to everything". That's why we take the *least* fixed point of the function, that is, the smallest set that satisfies the definition.
Fixed-point theory also tells us *when* the "repeat until no changes occur" approach will work:
* if any set of values (in the above example: sets of equal values) always have a common "more basic" value (that's needed so that whatever initial value you start with, you finally arrive at the same set of values that satisfy the definition).
* there are no infinities involved when going to the common "more basic" value (otherwise you'd get into an endless loop, always nearing the fixed point but never quite reaching it - say, recursing towards a given string by enumerating all intermediate string will give you this kind of effect).
HTH Jo .
- References:
- Please explain: Monad.ST, Monad.Fix and recursive do.
- From: Paul Johnson
- Please explain: Monad.ST, Monad.Fix and recursive do.
- Prev by Date: Please explain: Monad.ST, Monad.Fix and recursive do.
- Next by Date: Re: Please explain: Monad.ST, Monad.Fix and recursive do.
- Previous by thread: Please explain: Monad.ST, Monad.Fix and recursive do.
- Next by thread: Re: Please explain: Monad.ST, Monad.Fix and recursive do.
- Index(es):
Relevant Pages
|
