Abstraction function

The abstraction function α is the left adjoint of a Galois connection in the theory of abstract interpretation, mapping concrete values to their most precise abstract representations. Where the concretization function γ tells us what an abstract value means, the abstraction function tells us how to compress a concrete state into the abstract domain. The Galois connection property guarantees that α(c) ⊑ a if and only if c ≤ γ(a), making the abstraction function the formal definition of what it means to lose information systematically.

The abstraction function is necessarily lossy: it collapses distinct concrete states into a single abstract value, and no subsequent operation can recover what was discarded. This irreversibility is not a defect but a design feature. The art of abstract interpretation lies in choosing an abstraction function that discards exactly the information that is irrelevant to the property being verified, while preserving the information that is relevant. A poorly chosen abstraction function produces abstract domains that are either too coarse to prove anything useful or too fine to compute efficiently. The widening operator was introduced to accelerate convergence when abstraction functions produce infinite ascending chains, but it introduces additional approximation that must be justified independently.