Differences

This shows you the differences between two versions of the page.

--- sav07_lecture_6_skeleton [2007/03/30 20:18]
vkuncak
+++ sav07_lecture_6_skeleton [2007/04/03 23:27]
vkuncak
@@ Line 1: / Line 1: @@
+====== Lecture 6 Skeleton ======
 ===== Resolution theorem proving =====
@@ Line 189: / Line 191: @@
+==== Background on Lattices ====
+Recall notions of [[preorder]], [[partial order]], [[equivalence relation]].
+Partial order where each two element set has
+  * supremum (least upper bound, join, $\sqcup$)
+  * infimum (greatest lower bound, meet, $\sqcap$)
+So, we have
+\begin{equation*}
+\begin{array}{ll}
+  x \sqsubseteq x \sqcup y & \mbox{(bound)} \\
+  y \sqsubseteq x \sqcup y & \mbox{(bound)} \\
+  x \sqsubseteq z \ \land\ y \sqsubseteq z\ \rightarrow\ x \sqcup y \sqsubseteq z & \mbox{(least)}
+\end{array}
+\end{equation*}
+and dually for $\sqcap$.
+See also [[wk>Lattice (order)]]
+Example [[wk>Hasse diagram]]s for powerset of {1,2} and for constant propagation.
+Properties of a lattice
+  * finite lattice
+  * finite ascending chain lattice
 ==== Basic notions of abstract interpretation ====
@@ Line 241: / Line 265: @@
 \end{equation*}
 and we call this "the best transformer".
-==== Lattices ====
-Recall notions of [[preorder]], [[partial order]], [[equivalence relation]].
-Partial order where each two element set has
-  * supremum (least upper bound, join, $\sqcup$)
-  * infimum (greatest lower bound, meet, $\sqcap$)
-So, we have
-\begin{equation*}
-\begin{array}{ll}
-  x \sqsubseteq x \sqcup y & \mbox{(bound)} \\
-  y \sqsubseteq x \sqcup y & \mbox{(bound)} \\
-  x \sqsubseteq z \ \land\ y \sqsubseteq z\ \rightarrow\ x \sqcup y \sqsubseteq z & \mbox{(least)}
-\end{array}
-\end{equation*}
-and dually for $\sqcap$.
-See also [[wk>Lattice (order)]]
-Example [[wk>Hasse diagram]]s for powerset of {1,2} and for constant propagation.
-Properties of a lattice
-  * finite lattice
-  * finite ascending chain lattice