Given a complete partial order $(D,\, {\leq})$ and a Scott-continuous function $F\colon D \rightarrow D$ and some fixed point $X = F(X)$.

Are there any criteria that ensure that $X = \mathsf{lfp} F$ where $\mathsf{lfp} F$ is the least fixed point of $F$?

Furthermore, are there any criteria that ensure that $Y \leq \mathsf{lfp} F$ for an arbitrary point $Y$?

  • 1
    $\begingroup$ You mean without computing the LFP? To check if y is less than LFP you can check if for some n $y < F^n(\bot)$ which seems only semidecodable in general. $\endgroup$ – Kaveh Nov 12 '15 at 17:01
  • $\begingroup$ Yes, I mean without computing or knowing the LFP. I'm looking for something more elegant than finding such an $n$. The method need not be complete, just sound. $\endgroup$ – zander Nov 12 '15 at 18:00

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Browse other questions tagged or ask your own question.