I have the basic definition of Galois connection.
Let $(C,\leq)$ and $(A,\sqsubseteq)$ be partial orders and $\alpha: C \rightarrow A$, $\gamma: A \rightarrow C$ monotonic functions. They form a Galois connection if $\forall c,a. \alpha(c) \sqsubseteq a \iff c \leq \gamma(a)$ (*).
Then I was able to proof some properties on them:
- The condition (*) is equivalent to $\forall c,a. c \leq \gamma(\alpha(c)) \land \alpha(\gamma(a)) \sqsubseteq a$ (**).
- Given a Galois connection the following are equivalent:
2.1 $\alpha(\gamma(a)) = a \; \forall a \in A$.
2.2 $\alpha$ is a surjective function.
2.3 $\gamma$ is an injective function.
Now I have to proof the following more imprecise statement:
When does $c = \gamma(\alpha(c)) \; \forall c$ hold? Assuming that $C$ is the set of concrete states and $A$ is the domain of static analysis, what is more likely $c = \gamma(\alpha(c)) \; \forall c$ or $\alpha(\gamma(a)) = a \; \forall a \in A$.
So I need to give a necessary and sufficient condition for $c = \gamma(\alpha(c)) \; \forall c$ to hold. Any other intuition you may have is useful.
We will have $c=\gamma(\alpha(c))$ if and only if $c$ is in the range of $\gamma$.
If $\gamma\circ\alpha$ and $\alpha\circ\gamma$ are both identities, then - by definition - $(C,\le)$ and $(A,\sqsubseteq)$ are isomorphic.
In general, $T:=\gamma\circ\alpha$ will be a closure operator, i.e. idempotent ($T\circ T=T$), increasing, and preserving arbitrary meets.