debugMinor
Notation for a Kleene fixed point with a starting element
Viewed 0 times
startingpointwithnotationforelementfixedkleene
Problem
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.
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.
Solution
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$.
$$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$.
Context
StackExchange Computer Science Q#68413, answer score: 2
Revisions (0)
No revisions yet.