Galois Connections and Soundness

Our abstract lattice is lossy — but whenever we can determine something using only the abstract representation, that conclusion also holds in the precise powerset version. The abstraction may know less, but it never lies. This "does not lie" quality is called soundness.

For example: an algorithm spots the missing number on a row. If it concludes "3 goes at (2,3)" in the abstract lattice, that's true in the concrete lattice too.

Both α and γ must be monotone (order-preserving). Their key properties:

γ ∘ α is extensive: γ(α(S)) ⊇ S — going abstract and back, we get at least what we started with. We never lose a valid solution by abstracting.
α ∘ γ is reductive: α(γ(a)) ⊑ a — going concrete and back, we never end up with a worse abstraction.

When α and γ are monotone and satisfy these two conditions, they form a Galois connection. We denote this with the barbed half-arrow notation from before:

concrete abstract

Notice how the notation captures exactly the two properties. Each barbed arrow only points one way — start in the concrete, follow α to the abstract, then γ back: tracing the arrows, we can only go up (γ ∘ α is extensive). Start in the abstract, follow γ to the concrete, then α back: we can only go down (α ∘ γ is reductive).

These are two sides of the same coin: abstraction and representation.

The abstraction side (γ ∘ α extensive) says: we never lose a valid solution by going abstract.

The representation side (α ∘ γ reductive) says: the abstract may carry extraneous representational structure that a round-trip through the concrete can eliminate.

To illustrate this, let's think of other ways of representing numbers in a Sudoku. Suppose we describe each cell by two properties: its parity (odd or even) and a range [lo, hi]. Now watch what happens when we round-trip:

The range tightened from [3, 6] to [4, 6] — the round-trip squeezed out the slack. We got a strictly more precise abstract element.

See the round-trip in action on our Sudoku grids. Step through S → α(S) → γ(α(S)) and watch the set grow:

A Galois connection is the setting where for every concrete state of affairs, there is always one ideal (most precise) abstract representation — even though many non-ideal abstract elements may represent the same concrete set.

Our earlier observation that meets are precise but joins are lossy in the abstract lattice falls out of the math — it is a structural consequence of the Galois connection, not a coincidence.

This entire section dualizes. The dual of soundness is completeness — we never add a solution candidate that isn't an actual solution. In that setting, α and γ swap roles. This is beyond the scope of this tutorial.

The intuitive notions of "abstraction" and "representation" can be formalized by Galois connections.

The use of Galois connections to soundly analyze the behavior of computational systems through abstraction is called abstract interpretation. It was invented by Patrick and Radhia Cousot, originally for analyzing computer programs — but as we've seen, the framework applies to any setting where we want to approximate a complex system soundly. See: P. Cousot & R. Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, POPL 1977.