Simultaneous Least/Greatest Fixed Points

Question

I have two functions $f : V \times S \to V$ and $g : V \times S \to S$ where $V$ and $S$ are complete lattices and $v \subseteq v' \wedge s \subseteq s'$ implies $f(v, s) \subseteq f(v', s') \wedge g(v, s) \subseteq g(v', s')$.

Do we have enough information to show that there exists some $v$ and $s$ such that $v$ is the least fixed point of $f'(x) = f(x, s)$ and $s$ is the greatest fixed point of $g'(x) = g(v, x)$? If so, are $v$ and $s$ unique?

I'd also love a reference for this sort of thing if possible, I've been having a hard time finding one!

Answer 1

Notations:

• $f_s:x\mapsto f(x,s)$
• $g_v:y\mapsto f(v,y)$

You question is: If $f:V\times S\to V$ and $g:V\times S \to S$ are monotonic, are there $v_*$ and $s_*$ so that $v=\mu f_{s_*}$ and $s=\nu g_{v_*}$?

---

First, note that since $f$ is monotonic, so is $f_s$ for every $s$ so that $\mu f_s$ always exists (by the Knaster–Tarski theorem). Similarly $\nu g_v$ always exists.

But this isn't enough because if you take some random $s_0$, then you can take $v_1:=\mu f_{s_0}$ and then $s_2:=\nu g_{v_1}$ but there no reason to have $s_2=s_0$. We could try to go one step further by taking $v_3:=\mu f_{s_2}$ but then again, there would be no reason to have $v_3=v_1$. Can you see where I'm going with this?

What we want is a fixpoint of $(v,s)\mapsto (\mu f_s,\nu g_v)$. Can we have that?

-

Yes! We can just prove that $H:(v,s)\mapsto (\mu f_s,\nu g_v)$ is monotonic. Then we're done by the Knaster–Tarski theorem.

-

Define $F:s\mapsto f_s$ and $M:f\mapsto \mu f$. Why are they monotonous?

-

$F$ is monotonic because $s\le s'$ implies $\forall v, f_s(v)=f(v,s)\le f(v,s')=f_{s'}(v)$.

-

$M$ is monotonic because if $f\le g$, then whenever $g(x)\le x$ we have the inequality $f(x)\le g(x)\le x$. We therefore have the inclusion $\{x:f(x)\le x\}\supseteq \{x:g(x)\le x\}$. From which we can conclude that $\mu f = \bigwedge\{x:f(x)\le x\}\le \bigwedge \{x:g(x)\le x\}=\mu g$

-

Similar arguments work for $G:v\mapsto g_v$ and $N:g\mapsto \nu g$. If $f\le g$, $x\le f(x)$ implies $x \le f(x) \le g(x)$, so $\{x:x \le f(x)\}\subseteq \{x:x \le g(x)\}$. And we conclude $\nu f=\bigvee \{x:x \le f(x)\}\le \bigvee \{x:x \le g(x)\} = \nu g$

---

To show that it is not unique, you can take $V=S$, $f(v,s)=v\lor s$ and $g(v,s)=v\land s$. What's $\mu f_s$?

Hint: $v=v\lor s$ is equivalent to $s\le v$

-

$\mu f_s$ is the smallest $v$ so that $v=v\lor s$. But $v=v\lor s$ is equivalent to $s\le v$ so that $\mu f_s$ is the smallest $v$ so that $s \le v$, that is $\mu f_s=s$. Similarly $\nu g_v=v$. So taking $s=v$ is sufficient to satisfy your conditions. Since there are complete lattices with more than one element, we can therefore conclude that the couple $(v,s)$ is not unique in general.

---

As for references, I don't really know. I scrolled through this and it looks nice. You could try to use induction or coinduction as keywords in your search.