HiveBrain v1.2.0
Get Started
← Back to all entries
debugMinor

Notation for a Kleene fixed point with a starting element

Submitted by: @import:stackexchange-cs··
0
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.

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$.

Context

StackExchange Computer Science Q#68413, answer score: 2

Revisions (0)

No revisions yet.