<p>You need to identify the lattices involved in each case. </p>

<p>Let $(\wp(S),\subseteq)$ be the lattice of all subsets of a set $S$ ordered by subset inclusion. A function $f:\wp(S) \to \wp(S)$ is <em>monotone</em> if for every pair of sets $x$ and $y$, if $x \subseteq y$ it also holds that $f(x) \subseteq f(y)$. The definition applies more generally to functions $f: L \to M$ between partially ordered sets $L$ and $M$. </p>

<p>Let $Stmt$ be the set of statements occurring in a program and let $(\wp(Stmt),\subseteq)$ be the lattice of subsets of statements ordered by subset inclusion. Let us assume for simplicity that a statement in $Stmt$ is either an assignment $x:= e$ or a Boolean expression $b$ (representing the entry of a conditional or head of a loop). </p>

<p>A control flow graph has the form $G = (Stmt,E)$ where $E$ is an edge relation over statements. The following definitions are extremely standard:</p>

<p>$succ: \wp(Stmt) \to \wp(Stmt)$ maps a set of statements to their successors.</p>

<p>$succ(X) = \{ y \in Stmt | \text{ there exists } x \text{ in } X \text{ such that } (x,y) \text{ is in } E\}$</p>

<p>$pred: \wp(Stmt) \to \wp(Stmt)$ maps a set of statements to their predecessors.</p>

<p>$pred(X) = \{ y \in Stmt | \text{ there exists } x \text{ in } X \text{ such that } (y,x) \text{ is in } E\}$</p>

<p>It is a standard exercise to show that these are monotone functions. </p>

<p>Consider the set $Exp$ of all arithmetic and Boolean expressions occurring in a program. The structure $(\wp(Exp),\subseteq)$ is a lattice with the subset inclusion order.</p>

<p>For the <em>available expressions</em> analysis, we can define two functions $Gen$ and $Kill$ in two steps as follows.</p>

<p>First define $Gen: Stmt \to \wp(Exp)$ as a function that maps a statement to the set of expressions generated by that statement. We can define $Gen$ inductively and lift it to sets as follows.</p>

<p>$Gen(x := e) = \{e\}$ and  $Gen(b) = \{b\}$</p>

<p>The lifted function $Gen: \wp(Stmt) \to \wp(Exp)$  is obtained in a standard manner by taking the union of $Gen$ sets for every statement in a given set.</p>

<p>$$ Gen(S) = \bigcup_{s \in S} Gen(s) $$</p>

<p>You can now ask whether this function is monotone.</p>

<p><strong>A note about the slides</strong></p>

<p>The slides you are studying do not contain sufficient information to deduce everything I have said here from first principles and I doubt they are meant to be read that way. I would consult the lecture notes or the section on data flow analysis in a  standard compilers textbook for a thorough treatment with complete definitions.</p>

CC BY-SA 3.0
2013-04-15T10:45:35.397Z
2013-04-15T10:45:35.397Z
Vijay D
<p>I am studying program analysis and synthesis, I was reading a presentation
about some data flow analysis.</p>

<p>I can't seem to understand why $$\bigcap_{s'\in\text{pred (s)}}\text{Out}(s')$$
and $$\operatorname{Gen}(s)\cup(\operatorname{In}(s)\setminus \operatorname{Kill}(s))$$ is monotone, as claimed in
<a href="http://www.cs.umd.edu/class/fall2003/cmsc631/lectures/l02.pdf" rel="nofollow noreferrer">slide 22</a>.</p>

<p>I don't even understand exactly what is the function that is claimed to be monotone.
Can anyone please help ? any help is greatly appreciated! </p>

<p>*This was <a href="https://math.stackexchange.com/questions/354001/monotonicity-in-dfa-analysis">cross-posted </a>on Math.SE a couple of days ago</p>

CC BY-SA 3.0
2013-04-14T23:41:16.880Z
More appropriate for cs.stackexchange.
Yuval Filmus
CC BY-SA 3.0
2013-04-15T03:20:48.013Z
slides are from a graduate level class. seems research level to me. as for your question, think it would be better to define the functions. also try reading about monotone circuit theory which has same defn
vzn
CC BY-SA 3.0
2013-04-15T04:13:45.430Z
I am willing to bet 99 out of 100 would think that DFA is Deterministic Finite Automata. I am one of the 99.
Nobody
CC BY-SA 3.0
2013-04-15T05:01:57.700Z
A set function $f(s)$ is monotone if $s \subseteq t$ implies $f(s) \subseteq f(t)$. Oftentimes if a function is monotone then it's obvious, for example it's probably obvious that $\mathrm{Gen}(s)$ is monotone.
Yuval Filmus
CC BY-SA 3.0
2013-04-15T05:02:26.983Z
@vzn I stick to my claim that this question is not research level.
Yuval Filmus
CC BY-SA 3.0
2013-04-15T05:47:58.177Z
saying that graduate class implies research level is quite silly imo
Sasho Nikolov
CC BY-SA 3.0
2013-04-15T10:20:37.970Z
As someone working in the area, I can say that this is not a research question. The Gen-Kill data flow analysis is described in almost every compiler text book and the theoretical framework exists since 1973. It is undergraduate level material but is sometimes not taught because there is too much material to cram into a single compiler course and not for difficulty reasons.
Vijay D
<compilers><program-analysis>
Monotonicity in data flow analysis
Belgi
# Monotonicity in data flow analysis

(Asked by: username_0 on 2013-04-14)

I am studying program analysis and synthesis, I was reading a presentation
about some data flow analysis.

I can't seem to understand why $$\bigcap\_{s'\in\text{pred (s)}}\text{Out}(s')$$
and $$\operatorname{Gen}(s)\cup(\operatorname{In}(s)\setminus \operatorname{Kill}(s))$$ is monotone, as claimed in
[slide 22](http://www.cs.umd.edu/class/fall2003/cmsc631/lectures/l02.pdf).

I don't even understand exactly what is the function that is claimed to be monotone.
Can anyone please help ? any help is greatly appreciated!

\*This was [cross-posted](https://math.stackexchange.com/questions/354001/monotonicity-in-dfa-analysis) on Math.SE a couple of days ago

**Tags:** compilers, program-analysis
> **Comments:**
> **username_1**: More appropriate for cs.stackexchange.  
> **username_2**: slides are from a graduate level class. seems research level to me. as for your question, think it would be better to define the functions. also try reading about monotone circuit theory which has same defn  
> **username_3**: I am willing to bet 99 out of 100 would think that DFA is Deterministic Finite Automata. I am one of the 99.  
> **username_1**: A set function $f(s)$ is monotone if $s \subseteq t$ implies $f(s) \subseteq f(t)$. Oftentimes if a function is monotone then it's obvious, for example it's probably obvious that $\mathrm{Gen}(s)$ is monotone.  
> **username_1**: @vzn I stick to my claim that this question is not research level.  
> **username_4**: saying that graduate class implies research level is quite silly imo  
> **username_5**: As someone working in the area, I can say that this is not a research question. The Gen-Kill data flow analysis is described in almost every compiler text book and the theoretical framework exists since 1973. It is undergraduate level material but is sometimes not taught because there is too much material to cram into a single compiler course and not for difficulty reasons.  

---

## 1 answers

### Answer by username_5 on 2013-04-15. Score: 7 | Accepted answer

You need to identify the lattices involved in each case.

Let $(\wp(S),\subseteq)$ be the lattice of all subsets of a set $S$ ordered by subset inclusion. A function $f:\wp(S) \to \wp(S)$ is *monotone* if for every pair of sets $x$ and $y$, if $x \subseteq y$ it also holds that $f(x) \subseteq f(y)$. The definition applies more generally to functions $f: L \to M$ between partially ordered sets $L$ and $M$.

Let $Stmt$ be the set of statements occurring in a program and let $(\wp(Stmt),\subseteq)$ be the lattice of subsets of statements ordered by subset inclusion. Let us assume for simplicity that a statement in $Stmt$ is either an assignment $x:= e$ or a Boolean expression $b$ (representing the entry of a conditional or head of a loop).

A control flow graph has the form $G = (Stmt,E)$ where $E$ is an edge relation over statements. The following definitions are extremely standard:

$succ: \wp(Stmt) \to \wp(Stmt)$ maps a set of statements to their successors.

$succ(X) = \{ y \in Stmt | \text{ there exists } x \text{ in } X \text{ such that } (x,y) \text{ is in } E\}$

$pred: \wp(Stmt) \to \wp(Stmt)$ maps a set of statements to their predecessors.

$pred(X) = \{ y \in Stmt | \text{ there exists } x \text{ in } X \text{ such that } (y,x) \text{ is in } E\}$

It is a standard exercise to show that these are monotone functions.

Consider the set $Exp$ of all arithmetic and Boolean expressions occurring in a program. The structure $(\wp(Exp),\subseteq)$ is a lattice with the subset inclusion order.

For the *available expressions* analysis, we can define two functions $Gen$ and $Kill$ in two steps as follows.

First define $Gen: Stmt \to \wp(Exp)$ as a function that maps a statement to the set of expressions generated by that statement. We can define $Gen$ inductively and lift it to sets as follows.

$Gen(x := e) = \{e\}$ and $Gen(b) = \{b\}$

The lifted function $Gen: \wp(Stmt) \to \wp(Exp)$ is obtained in a standard manner by taking the union of $Gen$ sets for every statement in a given set.

$$ Gen(S) = \bigcup\_{s \in S} Gen(s) $$

You can now ask whether this function is monotone.

**A note about the slides**

The slides you are studying do not contain sufficient information to deduce everything I have said here from first principles and I doubt they are meant to be read that way. I would consult the lecture notes or the section on data flow analysis in a standard compilers textbook for a thorough treatment with complete definitions.


---

