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.
Consider the sequence $(F^n(\overrightarrow{\emptyset}))_n$ and note that $\overrightarrow{\emptyset} \sqsubseteq F(\overrightarrow{\emptyset})$. Since $F$ is monotone, a straightforward mathematical induction (see Appendix B) gives that $F^n(\overrightarrow{\emptyset}) \sqsubseteq F^{n + 1}(\overrightarrow{\emptyset})$ for all $n$. All the elements of the sequence will be in $(\mathcal{P}(\mathbf{\text{Var}_\star \times \mathbf{\text{Lab}_\star}))}^{12}$ and since this is a finite set it cannot be the case that all elements of the sequence are distinct so there must be some $n$ such that: $$F^{n+1}(\overrightarrow{\emptyset}) = F^n(\overrightarrow{\emptyset})$$ But since $F^{n + 1}(\overrightarrow{\emptyset}) = F(F^n(\overrightarrow{\emptyset}))$ this just says that $F^n(\overrightarrow{\emptyset})$ is a fixed point of $F$ and hence that $F^n(\overrightarrow{\emptyset})$ is a solution to the above equation system.
I am confused by this part:
But since $F^{n + 1}(\overrightarrow{\emptyset}) = F(F^n(\overrightarrow{\emptyset}))$ this just says that $F^n(\overrightarrow{\emptyset})$ is a fixed point of $F$ and hence that $F^n(\overrightarrow{\emptyset})$ is a solution to the above equation system.
How do we know that $F^{n + 1}(\overrightarrow{\emptyset}) = F(F^n(\overrightarrow{\emptyset}))$, and how does this then imply that $F^n(\overrightarrow{\emptyset})$ is a fixed point of $F$ and therefore that $F^n(\overrightarrow{\emptyset})$ is a solution to the above equation system?
I've read a number of seemingly relevant facts, but I'm struggling to put them together to clarify my above confusion. In Appendix A.1 Basic Definitions, the textbook (see the above link) says that $\perp = \sqcup \emptyset = \sqcap L$ is the least element. And, in the above excerpt, the authors tell us that $(\mathcal{P}(\mathbf{\text{Var}_\star \times \mathbf{\text{Lab}_\star}))}^{12}$ is a complete lattice with least element $\overrightarrow{\emptyset} = (\emptyset, \dots, \emptyset)$. Then, in Appendix A.4 Fixed Points, the textbook says that, if $L$ satisfies the Ascending Chain Condition, then there exists $n$ such that $f^n (\perp) = f^{n + 1} (\perp)$ and hence $\text{lfp}(f) = f^n(\perp)$, where lfp stands for "least fixed point".
