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 agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.