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 and are two abstract interpretations. Suppose , and satisfy (6.2) and are order-preserving, (6.3) for all , and (6.4) for all . We then write . We write , and say is a refinement of , if there exist maps and such that .
Section 7 begins by pointing out that is reflexive and transitive and then defines to mean . The authors point out that 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
The proof gives some insight in the abstraction process :
I assume the word “algebra” in this context means “boolean algebra”, so that is an invertible map preserving order, etc. But what is the meaning of ““? 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 then and are isomorphic algebras.
The argument can be summarized as follows: suppose . To simplify the notation, is identified with the set (and ditto for ). It can be shown that (the restriction of to the set ) is a bijection from to . Supposing also that , we have is a bijection from to . From this, the authors conclude
is a bijection between and .
The problem with this is that the composition
is not defined, since the image of is , which is not necessarily contained in , the domain of . 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 is a bijection from to , yielding the desired algebra isomorphism.)
To make this concrete, let and . The authors have shown that is a bijection from to and that is a bijection from to . From this, they try to conclude that is a bijection from to . A counterexample to this claim is obtained by letting and . Define (). Then is a bijection from to , but is not a bijection from to .
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 then and are isomorphic algebras” is a theorem.