A question about Abstract Interpretation

by Stephen Siegel

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.

Advertisements