Differences

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

--- sav08:galois_connection_on_lattices [2008/05/07 23:45]
giuliano
+++ sav08:galois_connection_on_lattices [2015/04/21 17:30]
@@ Line 1: / Line 1: @@
-==== Galois Connection ====
-Galois connection is defined by two monotonic functions $\alpha : C \to A$ and $\gamma : A \to C$ between [[:partial order]]s $\leq$ on $C$ and $\sqsubseteq$ on $A$, such that
-\begin{equation*}
-  \alpha(c) \sqsubseteq a\ \iff\ c \leq \gamma(a) \qquad (*)
-\end{equation*}
-for all $c$ and $a$ (intuitively, the condition means that $c$ is approximated by $a$).
-**Lemma:** The condition $(*)$ holds iff the conjunction of these two conditions:
-\begin{eqnarray*}
-  c &\leq& \gamma(\alpha(c)) \\
-  \alpha(\gamma(a)) &\sqsubseteq& a
-\end{eqnarray*}
-holds for all $c$ and $a$.
-**Lemma:** Let $\alpha$ and $\gamma$ satisfy the condition of Galois connection.  Then the following three conditions are equivalent:
-  * $\alpha(\gamma(a)) = a$ for all $a$
-  * $\alpha$ is a [[wk>surjective function]]
-  * $\gamma$ is an [[wk>injective function]]
-===== Using Galois Connection =====
-Terminology:
-  * $C$ - concrete domain
-  * $A$ - abstract domain
-  * $\gamma$ - concretization function
-  * $\alpha$ - abstraction function
-  * $sp$ - (the usual) strongest postcondition (or just "strongest post"), also called
-  * $sp^{\#}$ - abstract post, abstract transformer (transforms one abstract element into another)
-Abstraction function for sign analysis.
-Define $sp^\#$ using $\alpha$ and $\gamma$:
-++++|
-\[
-    sp^\#(a,r) = \alpha(sp(\gamma(a),r)
-\]
-++++
-===== Best Abstract Transformer =====
-$sp^{\#}$ can in general be arbitrarily precise while preserving correctness.
-Given $\gamma$, we would like $sp^{\#}$ to be as precise as possible while being correct.
-The most precise $sp^{\#}$ is called "best abstract transformer".