🐾 Abstract Interpretation from Scratch

hewwo everyone!! (ᵒᵕᵒ) i keep seeing "abstract interpretation" mentioned in papers and in our reading list thread, but every time i try to read the Cousot & Cousot 1977 paper i get completely lost in the math notation ;;;

can anyone give me a ground-up intro? like i know what a partial order is, i've done a tiny bit of Haskell, and i understand what a program variable is. but terms like Galois connection and widening operator and collecting semantics just go right over my head 😿

specifically what i'd love to understand:

• what is a lattice and why does abstract interpretation care about them?
• what are monotone functions and why do we need them?
• what on earth is a Galois connection?
• what is "collecting semantics" and how does it relate to abstract transformers?
• what is widening and why do we need it?

i don't mind if it's long!! actually please make it long, i have the whole weekend 🐾

also if anyone has Haskell code examples that would be AMAZING, i learn best from code (///▽///)

Great question, LatticeTabby! Buckle up — this will be a long one. I'll build everything from scratch, piece by piece, so you can follow along. Get a warm drink and maybe a blanket 🐾

§1 — Why does abstract interpretation exist?

The core problem is this: we want to know things about a program without running it. For example, "does this variable ever go negative?" or "can this pointer be null here?" These are static analysis questions.

The trouble is that running every possible input would take forever (or literally be undecidable). Abstract interpretation, introduced by Patrick and Radhia Cousot in 1977, gives us a rigorous mathematical framework for trading precision for computability. We replace exact answers with safe approximations.

§2 — Partial Orders and Lattices

A partial order is a set L with a relation ⊑ ("less-than-or-equal in information") that is reflexive, antisymmetric, and transitive. You already know these!

A lattice extends this by requiring that any two elements a, b ∈ L have:

• Join (least upper bound): a ⊔ b — the "smallest thing above both"
• Meet (greatest lower bound): a ⊓ b — the "largest thing below both"

Example: The Sign Lattice

For tracking whether integers are positive, negative, or zero:

          ⊤  (unknown / could be anything)
         /|\
        / | \
      Neg Zero Pos
        \ | /
         \|/
          ⊥  (no possible value — bottom)

⊥ ⊑ Neg ⊑ ⊤, ⊥ ⊑ Zero ⊑ ⊤, ⊥ ⊑ Pos ⊑ ⊤. But Neg and Pos are incomparable — neither is "above" the other.

Example: The Interval Lattice

For tracking integer ranges: elements are [a, b] (where a ≤ b), plus ⊥ (empty, "unreachable") and ⊤ = (-∞, +∞). The ordering is: [a, b] ⊑ [c, d] iff c ≤ a and b ≤ d (i.e., one interval is contained in the other).

§3 — Monotone Functions

A function f : L → L is monotone if it preserves the ordering:

Why do we care? Because of the glorious Knaster-Tarski Fixed Point Theorem:

Why does this matter? Program semantics — what a program "does" — can be expressed as the least fixed point of a semantic function. The analysis finds an approximation of this fixed point in the abstract domain.

§4 — Collecting Semantics

Before we can abstract, we need to define what we're approximating. The collecting semantics is the "ideal" semantics: it collects all concrete program states reachable at each program point.

For a simple imperative program, if Σ is the set of all possible memory states, then the collecting semantics at program point p is a set of states C(p) ⊆ Σ. We model this as an element of the powerset lattice ⟨℘(Σ), ⊆⟩.

The collecting semantics is typically uncomputable (infinitely many states for programs with loops). Abstract interpretation replaces it with a computable approximation in a simpler abstract domain.

§5 — Galois Connections: The Bridge Between Worlds

This is the heart of the whole framework! A Galois connection is a formal link between the concrete domain (exact sets of states) and the abstract domain (our approximation).

Two key consequences fall out of this definition for free:

• α and γ are both monotone
• Unit laws: c ⊑_C γ(α(c)) and α(γ(a)) ⊑_A a

The first unit law says: abstracting and then concretising loses information (we might have a bigger set than we started with, because the abstraction was imprecise). The second says: concretising and then abstracting is at least as precise as the original abstract element.

Example: Sign Analysis Galois Connection

Concrete domain: ℘(ℤ) (sets of integers). Abstract domain: Signs = {⊥, Neg, Zero, Pos, ⊤}.

• α({...all negative integers...}) = Neg
• α({0}) = Zero
• α({-1, 0, 5}) = ⊤ (mixed signs → imprecise)
• γ(Pos) = {n ∈ ℤ | n > 0}
• γ(⊥) = ∅

§6 — Abstract Transformers

Now we're cooking! Given a Galois connection (α, γ) and a concrete semantic function f : C → C (like "what does this assignment statement do to the set of states?"), we want an abstract transformer f♯ : A → A that:

• Is computable (unlike f directly)
• Is sound: α(f(γ(a))) ⊑_A f♯(a) for all a

The best (most precise) sound abstract transformer is:

Example: Abstract Transformer for Addition

Concrete semantics of x := x + 1 on sign domain: if x is Pos, result is Pos. If x is Zero, result is Pos. If x is Neg... could be anything. So:

addOne♯ Pos  = Pos
addOne♯ Zero = Pos
addOne♯ Neg  = ⊤     -- could be negative, zero, or positive
addOne♯ ⊤    = ⊤
addOne♯ ⊥    = ⊥     -- unreachable stays unreachable

§7 — The Fixed Point Computation

Put it all together! For a program with loops, the analysis works by:

• Starting all program points at ⊥ (no information)
• Repeatedly applying the abstract transformers along control-flow edges
• Merging (joining ⊔) at join points (e.g. after an if/else)
• Iterating until no value changes — i.e., we reach a fixed point

This is guaranteed to terminate if the abstract lattice has finite height (no infinite ascending chains), because each iteration can only move values up in the lattice, and there's only finitely far to go.

§8 — Widening: Taming Infinite Lattices

But what about interval analysis? The interval lattice has infinite height — the chain [0,0] ⊑ [0,1] ⊑ [0,2] ⊑ ... never stabilises. Kleene iteration won't terminate!

The solution is a widening operator ▽ : A × A → A:

The classic interval widening: if the upper bound keeps increasing, jump it to +∞; if the lower bound keeps decreasing, jump it to -∞:

-- Widen [a,b] with [c,d]:
widen (a, b) (c, d) = (lower, upper)
  where
    lower = if c < a then -∞ else a
    upper = if d > b then +∞ else b

After widening, we've over-approximated — but we've guaranteed termination. We can then optionally narrow (refine the result) to recover some lost precision.

That's the full skeleton. GaloisCat will probably tighten up some of the formal definitions below, and MeownadTransformer will show you the Haskell. Ask follow-up questions freely! 🐾

As predicted 😼. Great writeup FixpointFeline! Let me add some formal precision and a few subtleties worth knowing.

On Galois Connections — the Adjunction Formulation

FixpointFeline gave the order-theoretic definition. There's an equivalent formulation as an adjunction that's worth knowing:

Galois Insertion vs. Galois Connection

Worth distinguishing these! A Galois connection can have "redundant" elements in the abstract domain — abstract elements that are the concretisation of no concrete value. A Galois insertion requires additionally that α ∘ γ = id_A, meaning every abstract element is "useful". Most well-designed abstract domains are insertions.

Key Structural Properties

Several important facts drop out of the definition for free. If (α, γ) is a Galois connection:

• α preserves all joins: α(⊔_C S) = ⊔_A {α(s) | s ∈ S} for all S ⊆ C. In particular, α(⊥_C) = ⊥_A.
• γ preserves all meets: γ(⊓_A S) = ⊓_C {γ(s) | s ∈ S}.
• α uniquely determines γ (and vice versa). You only need to specify one half!
• Both are monotone — this follows from the adjunction conditions, you don't need to verify it separately.

Soundness, Formally

An abstract transformer f♯ is sound for concrete f if:

The Widening-Narrowing Pair

FixpointFeline covered widening. Let me add: after widening to get a (possibly over-approximate) fixpoint x*, we can apply narrowing △ to improve precision:

• Start from the widened fixpoint x*
• Apply: x_0 = x*,   x_{n+1} = x_n △ f♯(x_n)
• Each step may only decrease (move down the lattice), improving precision
• The result is still a sound over-approximation

Narrowing doesn't guarantee reaching the exact fixpoint, but it often recovers significant precision cheaply. See our thread on widening/narrowing for worked examples.

Composing Galois Connections

Galois connections compose! If (α₁, γ₁) : C ⇌ A and (α₂, γ₂) : A ⇌ B, then (α₂ ∘ α₁, γ₁ ∘ γ₂) : C ⇌ B is also a Galois connection. This lets you build abstract domains compositionally — the sign domain can be an abstraction of an interval domain, which is an abstraction of the powerset domain. Each layer is individually verifiable!

Haskell time!! ٩(◕‿◕｡)۶ I'll implement the concepts above step by step.

Step 1: Lattice Typeclass

-- A type class for lattices
class Eq a => Lattice a where
  bot   :: a                 -- ⊥
  top   :: a                 -- ⊤
  join  :: a -> a -> a    -- ⊔ (least upper bound)
  meet  :: a -> a -> a    -- ⊓ (greatest lower bound)
  leq   :: a -> a -> Bool -- ⊑
  leq x y = join x y == y  -- default: x ⊑ y iff x ⊔ y = y

Step 2: The Sign Domain

data Sign = SBot | SNeg | SZero | SPos | STop
  deriving (Eq, Show, Ord)

instance Lattice Sign where
  bot = SBot
  top = STop

  join SBot y    = y
  join x    SBot = x
  join STop _    = STop
  join _    STop = STop
  join x    y
    | x == y    = x
    | otherwise = STop  -- incomparable elements join to ⊤

  meet STop y    = y
  meet x    STop = x
  meet SBot _    = SBot
  meet _    SBot = SBot
  meet x    y
    | x == y    = x
    | otherwise = SBot

Step 3: The Interval Domain

data Bound = NegInf | Finite Int | PosInf
  deriving (Eq, Ord, Show)

data Interval
  = IBot              -- ⊥ (unreachable)
  | IVal Bound Bound  -- [lo, hi]
  deriving (Eq, Show)

-- Smart constructor: normalise empty intervals to ⊥
iVal :: Bound -> Bound -> Interval
iVal lo hi
  | lo > hi   = IBot
  | otherwise = IVal lo hi

instance Lattice Interval where
  bot = IBot
  top = IVal NegInf PosInf

  join IBot y           = y
  join x    IBot        = x
  join (IVal l1 h1) (IVal l2 h2)
    = IVal (min l1 l2) (max h1 h2)

  meet IBot _           = IBot
  meet _    IBot        = IBot
  meet (IVal l1 h1) (IVal l2 h2)
    = iVal (max l1 l2) (min h1 h2)

Step 4: Galois Connection as a Type

-- A Galois connection between concrete type c and abstract type a
data GaloisConn c a = GC
  { abstFn  :: c -> a   -- α
  , concFn  :: a -> c   -- γ
  }

-- Sign analysis Galois connection
-- Concrete: sets of integers (represented as [Int] for demonstration)
signGC :: GaloisConn [Int] Sign
signGC = GC
  { abstFn = alphaSign
  , concFn = gammaSign
  }

alphaSign :: [Int] -> Sign
alphaSign [] = SBot
alphaSign xs =
  let hasNeg  = any (< 0) xs
      hasZero = any (== 0) xs
      hasPos  = any (> 0) xs
  in case (hasNeg, hasZero, hasPos) of
       (True,  False, False) -> SNeg
       (False, True,  False) -> SZero
       (False, False, True ) -> SPos
       _                      -> STop

gammaSign :: Sign -> [Int]
gammaSign SBot  = []
gammaSign SNeg  = [minBound..(-1)]  -- conceptually all negatives
gammaSign SZero = [0]
gammaSign SPos  = [1..maxBound]  -- conceptually all positives
gammaSign STop  = [minBound..maxBound]

Step 5: Computing Fixed Points

-- Least fixed point by Kleene iteration
-- Works on any lattice with finite height
lfp :: (Lattice a) => (a -> a) -> a
lfp f = go bot
  where
    go x =
      let x' = f x
      in if x' == x
         then x           -- fixed point reached!
         else go (join x x')  -- move up the lattice

-- Fixed point with widening (for infinite lattices like intervals)
lfpWiden :: (Lattice a)
         => (a -> a -> a)  -- widening operator ▽
         -> (a -> a)        -- transfer function f♯
         -> a
lfpWiden widen f = go bot
  where
    go x =
      let x' = widen x (f x)
      in if x' == x
         then x
         else go x'

-- Interval widening: accelerate infinite chains
widenInterval :: Interval -> Interval -> Interval
widenInterval IBot y = y
widenInterval x IBot = x
widenInterval (IVal l1 h1) (IVal l2 h2) =
  IVal lo hi
  where
    lo = if l2 < l1 then NegInf else l1  -- lower bound shrinking? go to -∞
    hi = if h2 > h1 then PosInf else h1  -- upper bound growing? go to +∞

Step 6: Abstract Transformers for a Tiny Language

-- Abstract state: map from variable names to Signs
import qualified Data.Map.Strict as Map
type AbsState = Map.Map String Sign

-- Transfer function for: x := x + 1
absAddOne :: String -> AbsState -> AbsState
absAddOne var st =
  Map.insertWith (const id) var result st
  where
    s = Map.findWithDefault SBot var st
    result = case s of
      SBot  -> SBot   -- unreachable
      SNeg  -> STop   -- neg + 1 = anything
      SZero -> SPos   -- 0 + 1 = positive
      SPos  -> SPos   -- pos + 1 = positive
      STop  -> STop   -- unknown stays unknown

-- Abstract multiplication sign rule: sign(a * b)
absMul :: Sign -> Sign -> Sign
absMul SBot _    = SBot
absMul _    SBot = SBot
absMul SZero _  = SZero
absMul _  SZero = SZero
absMul SPos SPos  = SPos
absMul SNeg SNeg  = SPos
absMul SPos SNeg  = SNeg
absMul SNeg SPos  = SNeg
absMul _    _     = STop

Putting It All Together: A Mini Analyser

-- Example: analyse the loop  while (x > 0) { x := x - 1 }
-- Starting assumption: x is Pos

loopTransfer :: Sign -> Sign
loopTransfer s =
  let -- guard: x > 0 restricts to Pos
      guarded = meet s SPos
      -- body: x := x - 1
      result  = case guarded of
        SBot -> SBot
        SPos -> STop   -- pos - 1 could be zero or still positive
        _    -> STop
  in result

analyseLoop :: Sign
analyseLoop = lfp (\s -> join SPos (loopTransfer s))
-- Result: STop — we lose track of the sign through the loop
-- (sign analysis is not precise enough to handle this loop)

This is the key thing to understand: the choice of abstract domain determines what properties you can precisely track. Sign analysis tells us about positivity/negativity but loses precise range information. Interval analysis would let us track that x goes from some positive value down to 0. See the Abstract Domain Zoo thread for more domains!

Hope this helps LatticeTabby!! feel free to ask any questions about the code (づ｡◕‿‿◕｡)づ

omg omg omg this is SO good 😭😭 thank you all so much!!! i've been reading through everything and it's finally clicking.

i have a question about the Galois connection for Haskell — in the sign GC, gammaSign SNeg returns [minBound..(-1)]. but doesn't that create an infinite list (or at least a huge one)? how would a real implementation handle this?

also i'm confused about one thing in §5: when FixpointFeline says "merge with join at join points" — does that mean at if/else merge points in the CFG we take the ⊔ of the two branches? so if one branch says x is Pos and the other says x is Zero, we join them to get... STop? that seems like a big precision loss just from a simple if-else!

Great catch! Yes — in a real implementation, the concrete domain wouldn't be [Int] at all. It would be a predicate or a mathematical set that you reason about on paper. The concrete domain is theoretical; only the abstract domain needs to be computable. The Haskell code was just for illustration! In practice you only ever execute the abstract transformer α ∘ f ∘ γ symbolically.

Almost! join SPos SZero = STop in my implementation — yes, that's the imprecision of sign analysis. But notice: in a real analyser, you'd usually track a full abstract state (map from variables to abstract values). If only x differs between branches, you only lose precision on x. Other variables are fine.

Also, smarter analyses would track more! With the interval domain, the join of [1, +∞) and [0, 0] is [0, +∞) — that's much more informative than ⊤. And some analyses (like relational domains) track relationships between variables, so they wouldn't lose precision at all in some cases.

The moral: sign analysis is very fast but coarse. Interval analysis is more precise but harder. Polyhedra are even more precise but exponentially expensive. There's always a precision/cost tradeoff — and abstract interpretation gives you the framework to navigate it rigorously ✨

One more thing worth adding for LatticeTabby: the sign domain is not a disjunctive domain — it can't tell apart "x is Pos OR x is Zero" from "x is any sign". That's what ⊤ means. Domains based on sets of abstract values (disjunctive completion) can express this, but they're more expensive.

For reading, I'd suggest going through these in order:

• Our resources thread — has links to Cousot's original 1977 paper and Blanchet's intro notes
• Sign Analysis Worked Example thread — walks through a full program by hand
• Interval Analysis Deep Dive
• Then the Cousot '77 reading group thread — the paper will be readable after the above prep!

Great thread. Bookmarked 🐾