Why does this being a finite set mean that it cannot be the case that all element of the sequence are distinct?

49 Views Asked by At

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:

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})$$

Why does $(\mathcal{P}(\mathbf{\text{Var}_\star \times \mathbf{\text{Lab}_\star}))}^{12}$ being a finite set mean that it cannot be the case that all elements of the sequence are distinct? Furthermore, $n$ wasn't even defined, so I'm not even sure what it's supposed to be.

1

There are 1 best solutions below

0
On BEST ANSWER

When they say "consider the sequence $(F^n(\overset{\to}{\emptyset}))_n$", they mean the infinite sequence where $n$ ranges over all of $\mathbb N$. Since this is defined for infinitely many values of $n$, and takes only finitely many values (values in that finite set), there must be two different natural numbers $n,n+k$ with the same value.

Now we need to show that there must be two consecutive numbers with the same value. This is because $F^n(\overset{\to}{\emptyset})\sqsubseteq F^{n+1}(\overset{\to}{\emptyset})$, so if the above holds with $k>1$ we have $F^n(\overset{\to}{\emptyset})\sqsubseteq F^{n+1}(\overset{\to}{\emptyset})\sqsubseteq\cdots\sqsubseteq F^{n+k}(\overset{\to}{\emptyset})$; since the first and last terms are equal, they must all be equal.

Finally, by definition the $(n+1)$th term is the image of the $n$th under $F$, so it must be fixed by $F$ (and all subsequent terms are equal).