3
$\begingroup$

Assume a CPO $Q,\leq$ and a Scott-continuous function $f : Q \rightarrow Q$. As it is known, the chain $\bot \leq f(\bot) \leq \ldots \leq f^n(\bot)$ (where $f^n$ denotes the function $n-1$-times composed with itself) leads to a fixed point of $f$.

It is also clear, if $f$ is inflationary, that for any $q \in Q$, the chain $q \leq f(q) \leq \ldots \leq f^m(q)$ leads to a fixed point. (This follows immediately by just considering the subset $\{\,p\,|\, p \in Q \wedge q \leq p\}$, which is also a CPO.)

This second form is often more useful in practice. But how to denote it? While the fixed point of $f$ is easily written $\text{fix} f$, is there a standard convention for the second form? Writing $\text{fix} f(q)$ seems intuitive but is - strictly speaking - wrong, since $f(q)$ is not a function (it might also be confusing in the case of higher-order functions).

edit: Added note, that $f$ must be inflationary.

$\endgroup$
2
$\begingroup$

Suppose $Q$ is a join semilattice. Define $g:Q \to Q$ by

$$g(x) = f(x) \sqcup q.$$

Then $\text{fix} \; g$ is equal to the least fixpoint of $q,f(q),f^2(q),\dots$. So, at least for cpo's that form a join semilattice, you can indicate it pretty naturally using existing notation -- there's not a strong need to invent a new notation (though you could of course introduce one if you wanted).

If $Q$ is not a join semilattice, I think you can still define

$$g(x) = \sup \{ f(x), q \}$$

and then do the same thing. The least fixpoint of $q,f(q),f^2(q),\dots$ will be $\text{fix} \; g$.

$\endgroup$
1
$\begingroup$

Note that, in general, there might not be such a fixed point.

E.g. $$ \begin{array}{l} f : \mathbb{N}_\bot \to \mathbb{N}_\bot\\ f(\bot) = \bot\\ f(\lfloor n\rfloor) = \lfloor n + 1\rfloor \end{array} $$ is the standard denotation of the lazy lambda calculus function $\lambda n.\ n+1$. It is Scott-continuous.

Its least fixed point is $\bot$ -- actually, there are no other fixed points. So, if we consider the "chain" starting from $q = \lfloor 42 \rfloor$, which is $\lfloor 42 \rfloor, f(\lfloor 42 \rfloor), f^2(\lfloor 42 \rfloor), \ldots$ we discover that it's not even a chain, and as a set has no supremum in $\mathbb{N}_\bot$.

Hence, one should be careful here:

It is also clear, that for any $q \in Q$, the chain $q \leq f(q) \leq \ldots \leq f^m(q)$ leads to a fixed point. (This follows immediately by just considering the subset $\{\,p\,|\, p \in Q \wedge q \leq p\}$, which is also a CPO.)

If that is a chain, then it leads to a fixed point -- but it might not be a chain. Also, the subset you mention is a CPO: in the previous example it is the singleton CPO $\{q\}=\{\lfloor 42 \rfloor\}$. However, in general, $f$ is not an internal operation on that CPO. Indeed, in the example we immediately escape that.

$\endgroup$
  • 1
    $\begingroup$ You are right, I forgot to mention that the function also needs to be inflationary. Do I understand your answer correctly in that only $\bot < \lfloor n \rfloor$? $\endgroup$ – choeger Feb 8 '17 at 18:57
  • $\begingroup$ @choeger Yes, $\mathbb{N}_\bot$ only has $\bot < \lfloor n \rfloor$ as a strict inequality. (and $\lfloor - \rfloor : \mathbb{N}\to\mathbb{N}_\bot$ denotes the lifting injection -- I am probably being overly pedantic in using that explicitly here) $\endgroup$ – chi Feb 8 '17 at 19:32

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.