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