Showing that $F$ is a monotone function

I am currently studying the textbook Principles of Program Analysis by Flemming Nielson, Hanne R. Nielson, and Chris Hankin. Chapter 1.3 Data Flow Analysis says the following:

The least solution. The above system of equations defines the twelve sets $$\text{RD}_\text{entry}(1), \dots, \text{RD}_{\text{exit}}(6)$$ in terms of each other. Writing $$\overrightarrow{RD}$$ for this twelve-tuple of sets we can regard the equation system as defining a function $$F$$ and demanding that: $$\overrightarrow{RD} = F(\overrightarrow{RD})$$ To be more specific we can write $$F(\overrightarrow{RD}) (F_\text{entry}(1)(\overrightarrow{RD}), F_\text{exit}(1)(\overrightarrow{RD}), \dots, F_\text{entry}(6)(\overrightarrow{RD}), F_\text{exit}(6)(\overrightarrow{RD}))$$ where e.g.: $$F_\text{entry}(3)(\dots, \overrightarrow{RD}_\text{exit}(2), \dots, \overrightarrow{RD}_\text{exit}(5), \dots) = \overrightarrow{RD}_\text{exit}(2) \cup \overrightarrow{RD}_\text{exit}(5)$$ It should be clear that $$F$$ operates over twelve-tuples of sets of pairs of variables and labels; this can be written as $$F : (\mathcal{P}(\mathbf{\text{Var}_\star \times \mathbf{\text{Lab}_\star}))}^{12} \to (\mathcal{P}(\mathbf{\text{Var}_\star \times \mathbf{\text{Lab}_\star}))}^{12}$$ where it might be natural to take $$\mathbf{\text{Var}_\star} = \mathbf{\text{Var}}$$ and $$\mathbf{\text{Lab}_\star} = \mathbf{\text{Lab}}$$. However, it will simplify the presentation in this chapter to let $$\mathbf{\text{Var}_\star}$$ be a finite subset of $$\mathbf{\text{Var}}$$ that contains the variables occurring in the program $$\mathbf{S_\star}$$ of interest and similarly for $$\mathbf{\text{Lab}_\star}$$. So for the example program we might have $$\mathbf{\text{Var}_\star} = \{ x, y, z \}$$ and $$\mathbf{\text{Lab}_\star} = \{ 1, \dots, 6, ? \}$$.

It is immediate that $$(\mathcal{P}(\mathbf{\text{Var}_\star \times \mathbf{\text{Lab}_\star}))}^{12}$$ can be partially ordered by setting $$\overrightarrow{\text{RD}} \sqsubseteq \overrightarrow{\text{RD}}^\prime \ \ \ \text{iff} \ \ \ \forall i : \text{RD}_i \subseteq \text{RD}_i^\prime$$ where $$\overrightarrow{\text{RD}} = (\text{RD}_1, \dots, \text{RD}_{12})$$ and similarly $$\overrightarrow{\text{RD}}^\prime = (\text{RD}_1^\prime, \dots, \text{RD}_{12}^\prime)$$. This turns $$(\mathcal{P}(\mathbf{\text{Var}_\star \times \mathbf{\text{Lab}_\star}))}^{12}$$ into a complete lattice (see Appendix A) with least element $$\overrightarrow{\emptyset} = (\emptyset, \dots, \emptyset)$$ and binary least upper bounds given by: $$\overrightarrow{\text{RD}} \sqcup \overrightarrow{\text{RD}}^\prime = (\text{RD}_1 \cup \text{RD}_1^\prime, \dots, \text{RD}_{12} \cup \text{RD}_{12}^\prime)$$

It is easy to show that $$F$$ is in fact a monotone function (see Appendix A) meaning that: $$\overrightarrow{\text{RD}} \sqsubseteq \overrightarrow{\text{RD}}^\prime \ \ \ \text{implies} \ \ \ F(\overrightarrow{\text{RD}}) \sqsubseteq F(\overrightarrow{\text{RD}})^\prime$$ This involves calculations like $$\text{RD}_\text{exit}(2) \subseteq \text{RD}_\text{exit}^\prime(2) \ \ \text{and} \ \ \text{RD}_\text{exit}(5) \subseteq \text{RD}_\text{exit}^\prime(5)$$ imply $$\text{RD}_\text{exit}(2) \cup \text{RD}_\text{exit}(5) \subseteq \text{RD}^\prime_\text{exit}(2) \cup \text{RD}_\text{exit}^\prime(5)$$ and the details are left to the reader.

Appendix A gives the following definition for monotone function:

The function $$f$$ is monotone (or isotone or order-preserving) if $$\forall l, l^\prime \in L_1 : l \sqsubseteq_1 l^\prime \Rightarrow f(l) \sqsubseteq_2 f(l^\prime)$$

From earlier in the textbook:  I am trying to do as the author said, and show that $$F$$ is a monotone function. However, I have so far been unable to make progress. It seems to me that such a proof should proceed by showing that, for some arbitrary element of the set of elements $$F(\overrightarrow{\text{RD}})$$, if we use the fact that $$\overrightarrow{\text{RD}} \sqsubseteq \overrightarrow{\text{RD}}^\prime$$, then we can deduce that said arbitrary element is also an element of the set $$F(\overrightarrow{\text{RD}})^\prime$$, and so $$F(\overrightarrow{\text{RD}}) \sqsubseteq F(\overrightarrow{\text{RD}})^\prime$$. However, it seems to me that the textbook is very poorly written, and so it is difficult for me to even understand what said arbitrary elements of the set $$F(\overrightarrow{\text{RD}})^\prime$$ even are (they seem to be some kind of cartesian product, but I get very confused when trying to figure out precisely what they are). So how is it shown that $$F$$ is a monotone function?

Let me start by giving a formula for the function $$F$$: \begin{align*} \newcommand{\ent}{\mathsf{RD}_{\mathit{entry}}} \newcommand{\ext}{\mathsf{RD}_{\mathit{exit}}} \newcommand{\Lab}{\mathbf{Lab}} \newcommand{\bx}{\mathbf{x}} \newcommand{\by}{\mathbf{y}} \newcommand{\bz}{\mathbf{z}} &F(\ent(1),\ldots,\ent(6),\ext(1),\ldots,\ext(6)) = \\ (&\{(\bx,?),(\by,?),(\bz,?)\}, \ext(1), \ext(2) \cup \ext(5), \ext(3), \ext(4), \ext(3), \\ &(\ent(1) \setminus \{(\by,\ell) \mid \ell \in \Lab\}) \cup \{(y,1)\}, \\ &(\ent(2) \setminus \{(\bz,\ell) \mid \ell \in \Lab\}) \cup \{(z,2)\}, \\ &\ent(3), \\ &(\ent(4) \setminus \{(\bz,\ell) \mid \ell \in \Lab\}) \cup \{(z,4)\}, \\ &(\ent(5) \setminus \{(\by,\ell) \mid \ell \in \Lab\}) \cup \{(y,5)\}, \\ &(\ent(6) \setminus \{(\by,\ell) \mid \ell \in \Lab\}) \cup \{(y,6)\}). \end{align*} In order to show that $$F$$ is monotone, you need to show that the following hold whenever $$\ent(i) \subseteq \ent'(i)$$ and $$\ext(i) \subseteq \ext'(i)$$ for $$i \in \{1,\ldots,6\}$$:

• $$\{(\bx,?),(\by,?),(\bz,?)\} \subseteq \{(\bx,?),(\by,?),(\bz,?)\}$$.
• $$\ext(1) \subseteq \ext'(1)$$
• $$\ext(2) \cup \ext(5) \subseteq \ext'(2) \cup \ext'(5)$$
• $$\ext(3) \subseteq \ext'(3)$$
• $$\ext(4) \subseteq \ext'(4)$$
• $$\ext(3) \subseteq \ext'(3)$$
• $$(\ent(1) \setminus \{(\by,\ell) \mid \ell \in \Lab\}) \cup \{(y,1)\} \subseteq (\ent'(1) \setminus \{(\by,\ell) \mid \ell \in \Lab\}) \cup \{(y,1)\}$$
• $$(\ent(2) \setminus \{(\bz,\ell) \mid \ell \in \Lab\}) \cup \{(z,2)\} \subseteq (\ent'(2) \setminus \{(\bz,\ell) \mid \ell \in \Lab\}) \cup \{(z,2)\}$$
• $$\ent(3) \subseteq \ent'(3)$$
• $$(\ent(4) \setminus \{(\bz,\ell) \mid \ell \in \Lab\}) \cup \{(z,4)\} \subseteq (\ent'(4) \setminus \{(\bz,\ell) \mid \ell \in \Lab\}) \cup \{(z,4)\}$$
• $$(\ent(5) \setminus \{(\by,\ell) \mid \ell \in \Lab\}) \cup \{(y,5)\} \subseteq (\ent'(5) \setminus \{(\by,\ell) \mid \ell \in \Lab\}) \cup \{(y,5)\}$$
• $$(\ent(6) \setminus \{(\by,\ell) \mid \ell \in \Lab\}) \cup \{(y,6)\} \subseteq (\ent'(6) \setminus \{(\by,\ell) \mid \ell \in \Lab\}) \cup \{(y,6)\}$$

I'm sure you can work it out.

• This really clarifies what I need to do. And it's almost trivial. Thanks for the answer. Nov 26 '20 at 15:56