patternMinor
Abstract Interpretation: Connection between soundness relation and a Galois connection
Viewed 0 times
galoisabstractsoundnessbetweenandrelationinterpretationconnection
Problem
I am currently studying the paper "Abstract Interpretation Frameworks" by Cousot and Cousot from 1992 (https://doi.org/10.1093/logcom/2.4.511) to gain an understanding of the theory behind abstract interpretation.
One concept in abstract interpretation is the "soundness relation" (local page 6 in above paper). As I understand it, the soundness relation specifies if some object in the abstract domain $\mathcal{D}$ is a valid abstraction of some object in the concrete domain $\mathcal{C}$.
For special cases, you can describe an abstract interpretation using a Galois connection having an abstraction function $\alpha$ and a concretisation function $\gamma$. These form a Galois connection iff:
$$
\forall c \in \mathcal{C}: \forall d \in \mathcal{D}: \alpha(c) \sqsubseteq_{\mathcal{D}} d \Leftrightarrow c \sqsubseteq_{\mathcal{C}} \gamma(d)
$$
Compare: equation 4.12 in above paper.
Now the paper states right below that equation that:
The soundness relation is $\langle c, d\rangle \in \sigma \stackrel{def}{=} \alpha(c) \sqsubseteq_{\mathcal{D}} d \Leftrightarrow c \sqsubseteq_{\mathcal{C}} \gamma(d)$
where $\sigma$ is the soundness relation. This really puzzles me now. Doesn't this say that for a Galois connection that $\sigma = \mathcal{C}\times\mathcal{D}$ since due to equation 4.12, the right hand side of the definition holds for any combination of objects from the abstract and concrete domains? Do we want that?
It would make some sense to me if we defined $\langle c, d\rangle \in \sigma \stackrel{def}{=} \alpha(c) \sqsubseteq_{\mathcal{D}} d \wedge c \sqsubseteq_{\mathcal{C}} \gamma(d)$, so only if both sides are true. Yet this appears not to be the way to go.
As a side node, if you know another resource that covers these topics on abstract interpretation and is available online freely, please let me know :)
One concept in abstract interpretation is the "soundness relation" (local page 6 in above paper). As I understand it, the soundness relation specifies if some object in the abstract domain $\mathcal{D}$ is a valid abstraction of some object in the concrete domain $\mathcal{C}$.
For special cases, you can describe an abstract interpretation using a Galois connection having an abstraction function $\alpha$ and a concretisation function $\gamma$. These form a Galois connection iff:
$$
\forall c \in \mathcal{C}: \forall d \in \mathcal{D}: \alpha(c) \sqsubseteq_{\mathcal{D}} d \Leftrightarrow c \sqsubseteq_{\mathcal{C}} \gamma(d)
$$
Compare: equation 4.12 in above paper.
Now the paper states right below that equation that:
The soundness relation is $\langle c, d\rangle \in \sigma \stackrel{def}{=} \alpha(c) \sqsubseteq_{\mathcal{D}} d \Leftrightarrow c \sqsubseteq_{\mathcal{C}} \gamma(d)$
where $\sigma$ is the soundness relation. This really puzzles me now. Doesn't this say that for a Galois connection that $\sigma = \mathcal{C}\times\mathcal{D}$ since due to equation 4.12, the right hand side of the definition holds for any combination of objects from the abstract and concrete domains? Do we want that?
It would make some sense to me if we defined $\langle c, d\rangle \in \sigma \stackrel{def}{=} \alpha(c) \sqsubseteq_{\mathcal{D}} d \wedge c \sqsubseteq_{\mathcal{C}} \gamma(d)$, so only if both sides are true. Yet this appears not to be the way to go.
As a side node, if you know another resource that covers these topics on abstract interpretation and is available online freely, please let me know :)
Solution
It appears like I have simply misunderstood the expression: $\langle c, d\rangle \in \sigma \stackrel{def}{=} \alpha(c) \sqsubseteq_{\mathcal{D}} d \Leftrightarrow c \subseteq_{\mathcal{C}} \gamma(d)$.
What I read is: $\langle c, d\rangle \in \sigma$ is defined to hold if and only if $\alpha(c) \sqsubseteq_{\mathcal{D}} d \Leftrightarrow c \subseteq_{\mathcal{C}} \gamma(d)$.
In this interpretation all concrete and all abstract elements are in relation with each other.
What the paper probably is trying to say instead is: $\langle c, d\rangle \in \sigma \stackrel{def}{=} \alpha(c) \sqsubseteq_{\mathcal{D}} d$, so a concrete and an abstract element are in relation if the abstract element "contains" the abstraction of the concrete element.
The second part $\Leftrightarrow c \subseteq_{\mathcal{C}} \gamma(d)$ then refers to that expression saying that $\langle c, d\rangle \in \sigma$ is also equivalent to saying that $c \subseteq_{\mathcal{C}} \gamma(d)$, following from equation 4.12.
What I read is: $\langle c, d\rangle \in \sigma$ is defined to hold if and only if $\alpha(c) \sqsubseteq_{\mathcal{D}} d \Leftrightarrow c \subseteq_{\mathcal{C}} \gamma(d)$.
In this interpretation all concrete and all abstract elements are in relation with each other.
What the paper probably is trying to say instead is: $\langle c, d\rangle \in \sigma \stackrel{def}{=} \alpha(c) \sqsubseteq_{\mathcal{D}} d$, so a concrete and an abstract element are in relation if the abstract element "contains" the abstraction of the concrete element.
The second part $\Leftrightarrow c \subseteq_{\mathcal{C}} \gamma(d)$ then refers to that expression saying that $\langle c, d\rangle \in \sigma$ is also equivalent to saying that $c \subseteq_{\mathcal{C}} \gamma(d)$, following from equation 4.12.
Context
StackExchange Computer Science Q#148426, answer score: 3
Revisions (0)
No revisions yet.