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".

  • $\begingroup$ What is your definition of $F^n$? $\endgroup$ Nov 28 '20 at 9:24
  • $\begingroup$ I think that instead of reading this textbook, you should start with a textbook on discrete mathematics. $\endgroup$ Nov 28 '20 at 9:24
  • $\begingroup$ @YuvalFilmus I'm studying Introduction to Lattices and Order, Second Edition, by B. A. Davey, H. A. Priestley, as well, but this textbook by Flemming Nielson, Hanne R. Nielson, and Chris Hankin is very lacking in explanations, so it's difficult to follow along for someone new to program analysis. My understanding is that $F^n$ infinite sequence, where $n$ ranges over all of $\mathbb{N}$. And [...] $\endgroup$ Nov 28 '20 at 9:30
  • $\begingroup$ [...] $F$ is defined as stated above, $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}$, along with the clarity you provided here cs.stackexchange.com/a/132687/66333 $\endgroup$ Nov 28 '20 at 9:31
  • $\begingroup$ You won't be able to get far unless you have a good grasp of the basics. The necessary background is usually taught in classes on discrete mathematics. $\endgroup$ Nov 28 '20 at 9:33

In this case, the notation $F^n$ denotes iterated composition, that is, repeatedly applying the function $F$, for $n$ iterations:

  • $F^0(x) = x$.
  • $F^1(x) = F(x)$.
  • $F^2(x) = F(F(x))$.
  • $F^3(x) = F(F(F(x)))$.
  • $F^4(x) = F(F(F(F(x))))$.
  • $F^5(x) = F(F(F(F(F(x)))))$.

And so on.

There are two common ways to define function iteration inductively: \begin{align} F^0(x) &= x, & F^{n+1}(x) &= F^n(F(x)) \\ F^0(x) &= x, & F^{n+1}(x) &= F(F^n(x)) \end{align} Both definitions are equivalent, and you can show the following property under both: $$F^{i+j}(x) = F^i(F^j(x))$$

Now suppose that $F^n(x) = F^{n+1}(x)$, and let $y = F^n(x)$. Then $$ F(y) = F(F^n(x)) = F^{n+1}(x) = y, $$ and so $y$ is a fixed point of $F$ (which, by definition, is an element $y$ such that $F(y) = y$).


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.