I was learning fixed points in the context of programming languages and the text wants on page 89 wants to show that $fix(\mathcal F)$ is a fix point by applying $\mathcal F$ to the fix point itself. Why is that?

Right now we define the fix point as the least upper bound (LUB) of a the chain $ \bot \leq \mathcal F( \bot) \leq \mathcal F^2( \bot) \leq ...$ bottomed complete partial order (BCPO). How does apply the (continuous) function to the fix point show its a LUB of the chain in question?

I would have thought the fixed point was obvious a fixed point by definition but it seems we actually have to manipulate it to show this...

Note that in wikipedia and other sources fixed points are defined as points that continuous application of a rule leads to the same element. I assume that should be a consequence of the LUB definition we gave above but thats NOT how we show fixed points YET.

I understand the steps of the proof just not the rationale of the first step, why are we applying $\mathcal F$?

enter image description here

  • $\begingroup$ $fix(\mathcal F)$ is defined as a LUB of a chain of expressions. This certainly doesn't say that $fix(\mathcal F)$ is a fixed point by definition. Instead, for $z$ to be a fixed point of $\mathcal F$, $z$ should satisfy $\mathcal F(z)=z$. This is exactly what the proof shows for $z=fix(\mathcal F)$. $\endgroup$ – Derek Elkins Oct 3 '18 at 7:55
  • $\begingroup$ I don't get it, they never say that the definition of a fixed point is $\mathcal F(z) = z$. I thought just merely the definition of LUB would induce that property instead of just invoking it randomly. $\endgroup$ – Pinocchio Oct 3 '18 at 14:46
  • $\begingroup$ The notes you linked to appear to be an excerpt from a book. Note that Chapter 2 starts at section 2.6. Presumably, in the original book the definition of fixed point is given in one of the five sections preceding section 2.6. That said, the definition of fixed point is relatively consistent across mathematics. $\endgroup$ – Derek Elkins Oct 3 '18 at 19:14
  • $\begingroup$ @DerekElkins so it cannot be derived from the property I quoted? I know what it usually is, but Im trying to make sure Im not making assumptions $\endgroup$ – Pinocchio Oct 3 '18 at 22:01

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.