Fdtxjr

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!

Notations:

• $f_s:xmapsto f(x,s)$


• $g_v:ymapsto f(v,y)$

You question is: If $f:Vtimes Sto V$ and $g:Vtimes 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:smapsto f_s$ and $M:fmapsto mu f$. Why are they monotonous?

-

$F$ is monotonic because $sle s'$ implies $forall v, f_s(v)=f(v,s)le f(v,s')=f_s'(v)$.

-

$M$ is monotonic because if $fle 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 xsupseteq x:g(x)le x$. From which we can conclude that $mu f = bigwedgex:f(x)le xle bigwedge x:g(x)le x=mu g$

-

Similar arguments work for $G:vmapsto g_v$ and $N:gmapsto nu g$. If $fle g$, $xle 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)=vlor s$ and $g(v,s)=vland s$. What's $mu f_s$?

Hint: $v=vlor s$ is equivalent to $sle v$

-

$mu f_s$ is the smallest $v$ so that $v=vlor s$. But $v=vlor s$ is equivalent to $sle 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.