### A question about Abstract Interpretation

This note deals with Section 7 of Cousot and Cousot, Abstract Interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints, POPL, 1977.

First, the context: at this point in the paper, the notion of refinement of abstract interpretations has already been defined: suppose $I=\langle\textsf{Cont},\ldots\rangle$ and $\overline{I}=\langle\overline{\textsf{Cont}},\ldots\rangle$ are two abstract interpretations.   Suppose $\alpha\colon \textsf{Cont}\rightarrow\overline{\textsf{Cont}}$, and $\gamma\colon\overline{\textsf{Cont}}\rightarrow \textsf{Cont}$ satisfy (6.2) $\alpha$ and $\gamma$ are order-preserving, (6.3) $\overline{x}=\alpha(\gamma(\overline{x}))$ for all $\overline{x}\in\overline{\textsf{Cont}}$, and (6.4) $x\leq\gamma(\alpha(x))$ for all $x\in\textsf{Cont}$.  We then write $I\leq(\alpha,\gamma)\overline{I}$.  We write $I\leq\overline{I}$, and say $I$ is a refinement of $\overline{I}$, if there exist maps $\alpha$ and $\gamma$ such that $I\leq(\alpha,\gamma)\overline{I}$.

Section 7 begins by pointing out that $\leq$ is reflexive and transitive and then defines $I\equiv I'$ to mean $I\leq I' \wedge I'\leq I$. The authors point out that $\equiv$ is an equivalence relation, which is not hard to see. (One quibble: I thought an equivalence relation required a set, and I don’t see why the class of all abstract interpretations of a program is a set. But ignore this for now.)

So far, so good.  But then comes the statement

We have:
$\{I\equiv(\beta) I'\} \Leftrightarrow \{\beta\ \text{is an isomorphism between the algebras}\ I\ \text{and}\ I'\}$
The proof gives some insight in the abstraction process :

I assume the word “algebra” in this context means “boolean algebra”, so that $\beta\colon\textsf{Cont}\rightarrow\textsf{Cont}'$ is an invertible map preserving order, etc.   But what is the meaning of “$I\equiv(\beta) I'$“? I don’t believe this notation has been defined. At first, I thought the excerpt above was the definition, but that can’t be right because then there would be no need for a proof!  Now, even though I am not sure what this notation means, and therefore I don’t know what the authors are trying to prove, it seems that the bulk of the proof (the part beginning “2 – reciprocally”) is an attempt to show the following: if $I\equiv I'$ then $I$ and $I'$ are isomorphic algebras.

The argument can be summarized as follows: suppose $I\leq (\alpha_1,\gamma_1)I'$. To simplify the notation, $I$ is identified with the set $\textsf{Cont}$ (and ditto for $I'$). It can be shown that $\alpha_1|_{\gamma_1(I')}$ (the restriction of $\alpha_1$ to the set $\gamma_1(I')$) is a bijection from $\gamma_1(I')$ to $I'$.   Supposing also that $I'\leq(\alpha_2,\gamma_2)I$, we have $\alpha_2|_{\gamma_2(I)}$ is a bijection from $\gamma_2(I)$ to $I$.  From this, the authors conclude

$\alpha_1|_{\gamma_1(I')} \circ \alpha_2|_{\gamma_2(I)}$ is a bijection between $\gamma_2(I)$ and $I'$.

The problem with this is that the composition $\alpha_1|_{\gamma_1(I')} \circ \alpha_2|_{\gamma_2(I)}$
is not defined, since the image of $\alpha_2|_{\gamma_2(I)}$ is $I$, which is not necessarily contained in $\gamma_1(I')$, the domain of $\alpha_1|_{\gamma_1(I')}$. There are other points in the proof that do not make sense to me, but this is enough to ruin the show.  (The proof then uses this claim to argue $\alpha_1$ is a bijection from $I$ to $I'$, yielding the desired algebra isomorphism.)

To make this concrete, let $S=\gamma_1(I')$ and $S'=\gamma_2(I)$. The authors have shown that $\alpha_1|_{S}$ is a bijection from $S$ to $I'$ and that $\alpha_2|_{S'}$ is a bijection from $S'$ to $I$. From this, they try to conclude that $\alpha_1$ is a bijection from $I$ to $I'$. A counterexample to this claim is obtained by letting $I=I'=\mathbb{Z}$ and $S=S'=2\mathbb{Z}$. Define $\alpha_i(n)=\lfloor n/2\rfloor$ ($i=1,2$). Then $\alpha_i|_{2\mathbb{Z}}$ is a bijection from $2\mathbb{Z}$ to $\mathbb{Z}$, but $\alpha_i$ is not a bijection from $\mathbb{Z}$ to $\mathbb{Z}$.

Now, it could be that I am just missing something, and if so, I would appreciate any clarification. And I would still like to know whether the statement “if $I\equiv I'$ then $I$ and $I'$ are isomorphic algebras” is a theorem.