Lattice

Definition: A set $S$ together with a partial ordering $R$ is called a partially ordered set or poset for short

Definition: Given a poset $(P, ⊑)$ and its subset $S$ that $S \subseteq P$ , we say that

$u \in P$ is an upper bound of S, if $\forall x \in S, x ⊑ u$
$l \in P$ is a lower bound of S, if $\forall x \in S, l ⊑ x$
least upper bound (lub or join) of $S$ , written $⊔ S$ , if for every upper bound of $S$ , say $u$ , $⊔ S ⊑ u$
greatest lower bound (glb or meet) of $S$ , written $⊓ S$ , if for every lower bound of $S$ , say $l$ , $l ⊑ ⊔ S$

Usaually, if $S$ contains only two elements $a$ and $b$ ( $S = {a, b}$ ), then

$⊓ S$ can be written as $a ⊔ b$ (the join of $a$ and $b$ )
$⊔ S$ can be written as $a ⊓ b$ (the meet of $a$ and $b$ )

Note that not every poset has lub or glb, but if a poset has lub or glb, it will be unique
Proof. assume $a$ and $b$ are both glbs of poset $P$

because

a

is the glb then

b ⊑ a

; because

b

is the glb then

a ⊑ b

by the antisymmetry of partial order

a = b

, so the glb is unique.

Lattice

Definition: Given a poset, $\forall a, b \in P$ , if $a ⊔ b$ and $a ⊓ b$ exist, then its called a lattice

In other words, a poset is called lattice if every pair of its elements has a least upper bound and a greatest lower bound

Definition: All subsets of a lattice have a least upper bound and a greatest lower bound

the lub is called top
the glb is called bottom $⊥$

Definition: The height of a lattice h is the length of the longest path from Top to Bottom in the lattice

Definition: lattice $A$ 是分配的（distributive），当且仅当：

$(a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c)$
$(a ⊓ b) ⊔ c = (a ⊔ c) ⊓ (b ⊔ c)$

Definition: If only $a ⊔ b$ exists, then it's called a join semilattice

Definition: If only $a ⊓ b$ exists, then it's called a meet semilattice

Definition: Given a lattice, for arbitrary subset $S$ , if $⊓ S$ and $⊔ S$ exist, then it's called a complete lattice

e.g., $(S, ⊑)$ is not a complete lattice where $S$ is a set of integers and $⊑$ represents $\leq$
- the subset represents all even numbers has no least upper bound.

Theorem: Every finite lattice is a complete lattice. Proof. TODO

Definition: Given lattices $L 1 = (P_{1}, ⊑_{1}), \dots, L 1 = (P_{n}, ⊑_{n})$ , if $\forall i, L_{i}$ has least upper bound and greatest lower bound, then we can have a Product Lattice defined by

$P = P_{1} \times \dots \times P_{n}$
$(x_{1}, \dots, x_{n}) ⊑ (y_{1}, \dots, y_{n}) \Leftrightarrow (x_{1} ⊑ y_{1}) \land \dots \land (x_{n} ⊑ y_{n})$
$(x_{1}, \dots, x_{n}) ⊔ (y_{1}, \dots, y_{n}) = (x_{1} ⊔_{1} y_{1}, \dots, x_{n} ⊔_{n} y_{n})$
$(x_{1}, \dots, x_{n}) ⊓ (y_{1}, \dots, y_{n}) = (x_{1} ⊓_{1} y_{1}, \dots, x_{n} ⊓_{n} y_{n})$

Lemma: If all latices are complete lattices, then the product lattice is a complete lattice

Fixed-Point Theorem

A function $f : L \to L$ is monotone when $\forall x, y \in S : x ⊑ y \Rightarrow f (x) ⊑ f (y)$

e.g., a constant function
e.g., functions $⊔$ and $⊓$ are monotone in both arguments.

$\forall x, y, z \in L, x \subseteq y$ , we want to prove $x ⊔ z ⊑ y ⊔ z$

by definition of $⊔$ , $y \subseteq y ⊔ z$ , $z \subseteq y ⊔ z$
by transitivity of $\subseteq$ , $x \subseteq y \subseteq y ⊔ z$

thus $y ⊔ z$ is an upper bound for $x$ and also for $z$ , then we have $x ⊔ z ⊑ y ⊔ z$

Definition: In a lattice $L$ with finite height, every monotone function $f$ has a unique least fixed-point.
The least fixed point of $f$ can be found by iterating $f (⊥), f (f (⊥)), \dots, f^{k} (⊥)$ until a fixed point is reached.

We have an increasing chain:

⊥⊑ f (⊥) ⊑ f^{2} (⊥) ⊑ \dots

Since $L$ is assumed to have finite height, we must for some $k$ have that $f^{k} (⊥) = f^{k + 1} (⊥)$ .
We define $f i x (f) = f^{k} (⊥)$ and since $f (f i x (f)) = f^{k + 1} (⊥) = f^{k} (⊥) = f i x (f)$ , we know that $f i x (f)$ is a fixed-point.

Assume now that $x$ is another fixed-point. Since $⊥⊑ x$ it follows that $f (⊥) ⊑ f (x) = x$ , since $f$ is monotone and by induction we get that $f x (f) = f^{k} (⊥) ⊑ x$ . Hence, $f i x (f)$ is the least fixed-point. By anti-symmetry, it is also unique.

Similarly, the greatest fixed point of $f$ can be found by iterating $f (T), f (f (T)), \dots, f^{k} (T)$ until a fixed point is reached.

Closure Properties

Definition: If $L_{1}, L_{2}, \dots, L_{n}$ are lattices with finite height, then so is the product:

L_{1} \times L_{2} \times \dots \times L_{n} = {(x_{1}, x_{2}, \dots, x_{n}) ∣ x_{i} \in L_{i}}

where $⊑$ is defined pointwise. Note that $⊔$ and $⊓$ can be computed pointwise.

$h e i g h t (L_{1} \times \dots \times L_{n}) = h e i g h t (L_{1}) + \dots +$ height $(L_{n})$

Definition: If $L_{1}, L_{2}, \dots, L_{n}$ are lattices with finite height, then so is the sum:

L_{1} + L_{2} + \dots + L_{n} = {(i, x_{i}) ∣ x_{i} \in L_{i} \ {⊥, ⊤}} \cup {⊥, ⊤}

where $(i, x) ⊑ (j, y)$ iff $i = j$ and $x ⊑ y$

$h e i g h t (L_{1} + \dots + L_{n}) = max {height (L_{i})}$

Data Flow Analysis 可被看作沿某方向（正向分析或逆向分析），不停的应用 $F : V^{k} \to V^{k}$ 直到达到某不动点