Denotational semantics, proving that fixed point iteration results in the least fixed point

Question

I'm working through the Haskell wikibook section on denotational semantics and I'm kind of stuck on this exercise:

Prove that the fixed point obtained by fixed point iteration starting with is also the least one, that it is smaller than any other fixed point. (Hint: is the least element of our cpo and g is monotone).

Where the following statements define the core of the concepts leading up to the exercise (I think):

where f is the factorial function and is shown to be the fixed-point of g, given that g is continuous.

I think I basically understand the part where it is shown that g(f) = f but I don't really know what to make of the exercise. From what I understand, the factorial function f is the least-fixed point (with least based on the operator) but it's not at all clear to me what it means (intuitively) to compare functions with , let alone how I would find fixed points other than the least-fixed point shown in the example.

I understand that is less than everything else, and I understand that since g(x) is monotonic, if I apply it to two things, where one is less than the other, the results will still obey this ordering.

I think I would start the proof with taking some function f' and assuming . If that is the case, through the monotonic property of g I can show that . If I can then show that necessarily g(f') = g(f) or f' = f I think the proof is complete but I have no idea how to show that.

Answer 1

Let x be the sup/least upper bound of the sequence bot, g(bot), g(g(bot)), .... Let y be any fixed point of g (monotonic). We want to prove that x <= y.

By induction on the number of iterations, it's easy to see that every element in the sequence is <= y. Indeed, it trivially holds for bot, and if z is <= y by monotonicity we get g(z) <= g(y) = y.

So, y is an upper bound of the sequence. But x is the least, so x <= y. QED.