## 03 July 2013

### Least Fixed-Points of Monotone Functions are Monotone

This post presents a simple lemma related to the Knaster-Tarski fixed-point theorem. I used to think it's obvious, but today I set out to write down the full proof and I was somewhat surprised that I got stuck for awhile. As often is the case, I got unstuck with some help from Rasmus, and his slides in this case.

Definitions. Feel free to skip and refer back only if necessary.

A partial order $\le$ is a binary relation that is reflexive, transitive, and antisymmetric. \begin{align} &(1) &&x \le x\\ &(2) &&x \le y \land y \le z \to x \le z\\ &(3) &&x \le y \land y \le x \to x = y \end{align} A greatest lower bound $\inf Y$ of a set $Y$ is a lower bound (smaller than all elements of $Y$) and as big as possible: \begin{align} &(4) &&y:Y\to \inf Y \le y\\ &(5) &&(\forall y\; y:Y\to x\le y) \to x\le\inf Y \end{align} Lowest upper bounds are defined symmetrically. A set equipped with a preorder is a complete lattice when all its subsets $Y$ have a greatest lower bound $\inf Y$ and a lowest upper bound $\sup Y$. A function $f$ is monotone when it preserves the order: \begin{align} &(6) && x \le y \to f(x) \le f(y) \end{align} A pre-fixed-point of $f$ is an element $x$ that may only decrease by going thru $f$: \begin{align} &(7) && f(x) \le x \end{align} Post-fixed-points are defined symmetrically. A fixed-point is an element that is both pre- and post-fixed-point. A least fixed point ${\rm lfp}\,f$ of $f$ is the minimum of fixed points: \begin{align} &(8) &&f({\rm lfp}\,f)={\rm lfp}\,f\\ &(9) &&f(x)=x \to {\rm lfp}\,f \le x \end{align} Note that there is no a-priori reason to believe that least fixed-points (or even fixed-points) exist. Let ${\rm pre}\,f=\{x:f(x)\le x\}$ denote the set of $f$'s pre-fixed points.

Lemmas. Suppose from now on that $f$ is a fixed but arbitrary monotone function, on some complete lattice. Here's the first lemma: \begin{align} &(10) &&f(y)\le y \to f(\inf{\rm pre}\,f) \le y \end{align} Proof. \begin{align} & &&f(y) \le y\\ &\Rightarrow &&\{\text{(4) with Y:={\rm pre}\,f}\}\\ & &&\inf{\rm pre}\,f \le y\\ &\Rightarrow &&\{(6)\}\\ & &&f(\inf{\rm pre}\,f)\le f(y)\\ &\Rightarrow &&\text{assumption f(y)\le y}\\ & &&f(\inf{\rm pre}\,f)\le y \end{align}

Here's the second lemma: \begin{align} &(11) &&f(\inf{\rm pre}\,f) \le \inf{\rm pre}\,f \end{align} Proof. Instantiate (5) with $x:=f(\inf{\rm pre}\,f)$, and use (10) to discharge the assumption.

Here's the third lemma: \begin{align} &(12) &&\inf{\rm pre}\,f \le f(\inf{\rm pre}\,f) \end{align} Proof. Be careful here. It's a tricky argument that avoids talking about descending chains and such. \begin{align} & &&\{(11)\} \\ & &&f(\inf{\rm pre}\,f) \le \inf{\rm pre}\,f \\ &\Rightarrow &&\{(6)\}\\ & &&f(f(\inf{\rm pre}\,f)) \le f(\inf{\rm pre}\,f) \\ &\Rightarrow &&\{\text{(4) with y:=f(\inf{\rm pre}\,f) and Y:={\rm pre}\,f}\} \\ & &&\inf{\rm pre}\,f \le f(\inf{\rm pre}\,f) \end{align}

Here's the fourth lemma: \begin{align} &(13) &&{\rm lfp}\,f \le \inf{\rm pre}\,f \end{align} Proof. \begin{align} & &&\{\text{(3) with x:=\inf{\rm pre}\,f and y:=f(\inf{\rm pre}\,f)}\}\\ & &&(\inf{\rm pre}\,f \le f(\inf{\rm pre}\,f))\land(f(\inf{\rm pre}\,f) \le \inf{\rm pre}\,f) \to \inf{\rm pre}\,f=f(\inf{\rm pre}\,f)\\ &\Rightarrow &&\{\text{(11) and (12)}\}\\ & &&\inf{\rm pre}\,f=f(\inf{\rm pre}\,f) \\ &\Rightarrow &&\{\text{(9) with x:=\inf{\rm pre}\,f}\} \\ & &&{\rm lfp}\,f \le \inf{\rm pre}\,f \end{align}

You guessed: Here's the fifth lemma: \begin{align} &(14) &&f(y)\le y \to {\rm lfp}\,f \le y \end{align} Proof. \begin{align} & &&f(y) \le y \\ &\Rightarrow &&\{(10)\} \\ & &&f(\inf{\rm pre}\,f) \le y \\ &\Rightarrow &&\{\text{(13) and (2)}\} \\ & &&{\rm lfp}\,f \le y \end{align}

Proposition. Least-fixed points of monotone functions are monotone. Given that both $f$ and $g$ are monotone functions on some complete lattice, we have that \begin{align} \bigl(\forall x\; f(x) \le g(x)\bigr) \to {\rm lfp}\,f \le {\rm lfp}\, g \end{align} Proof. \begin{align} & &&f(x) \le g(x) \\ &\Rightarrow &&\{\text{instantiate with x:={\rm lfp}\,g}\} \\ & &&f({\rm lfp}\,g) \le g({\rm lfp}\,g) \\ &= &&\{\text{(8) with f:=g}\} \\ & &&f({\rm lfp}\,g) \le {\rm lfp}\,g \\ &\Rightarrow &&\{\text{(14) with y:={\rm lfp}\,g}\} \\ & &&{\rm lfp}\,f \le {\rm lfp}\, g \end{align}