Intuition for Galois Connections (beyond the formal definition)

♡ GaloisCat's Fav Topic Abstract Interpretation Category Theory (disputed) Started by GaloisCat · 134 replies · 7,841 views · 🔥 HOT
Page: 1 2 3 4 5 … »
Posts 1–28 of 134  |  Jump to latest
#1  [OP] Mon Mar 18, 2026  ·  02:14 AM

OK I HAVE BEEN WAITING TO WRITE THIS POST FOR LIKE TWO YEARS. Galois connections are my ABSOLUTE FAVORITE concept in all of program analysis and I think they are criminally under-explained in most courses. Everyone just slaps the formal definition up and calls it a day. So let me try to actually build the intuition. (mods please sticky this, I'm begging)

THE BIG PICTURE FIRST:

A Galois connection between two posets (C, ≤) and (A, ⊑) is a pair of monotone functions:

α : C → A (abstraction — goes UP to abstract) γ : A → C (concretization — comes DOWN to concrete) such that: α(c) ⊑ a ⟺ c ≤ γ(a) (for all c ∈ C, a ∈ A)

OK you've seen that. Boring. Here's what it actually means:

✦ THE CORE INTUITION ✦

α(c) is the most precise abstract element that still safely over-approximates c.
γ(a) is the largest (most general) concrete set that the abstract element a could possibly describe.

The adjunction condition says: "c fits under a's umbrella in the abstract iff c genuinely lives inside a's concretization in the concrete."

You can't fool the connection. If α says c is approximated by a, then γ had better contain c. And vice versa. It's a perfect correspondence between information loss in one direction and coverage in the other.

Let me make this super concrete with the sign domain, which is everyone's first example for a reason.

Our concrete domain: C = 𝒫(ℤ), sets of integers ordered by inclusion. Our abstract domain:

A = { ⊥, NEG, ZERO, POS, TOP } with ordering: TOP / | \ NEG ZERO POS \ | / ⊥

The abstraction function α works like this:

α(∅) = ⊥ α({-3, -1}) = NEG (all negative — best abstraction) α({0}) = ZERO α({1, 42}) = POS α({-1, 0, 1}) = TOP (mixed signs — we can only say "anything")

And concretization:

γ(⊥) = ∅ γ(NEG) = { z ∈ ℤ | z < 0 } = { ..., -3, -2, -1 } γ(ZERO)= { 0 } γ(POS) = { z ∈ ℤ | z > 0 } = { 1, 2, 3, ... } γ(TOP) = ℤ

Now watch the adjunction property do its thing. Is α({-3, -1}) ⊑ TOP? Obviously yes, NEG ⊑ TOP. And is {-3,-1} ⊆ γ(TOP) = ℤ? Also yes! The two sides of the biconditional agree perfectly. Try any example — they always agree. That's not a coincidence. That's the Galois connection being the Galois connection. 🐾

There are two key corollaries that fall out immediately and which are the real reason we care:

(1) c ≤ γ(α(c)) ["round-trip up-then-down loses info"] (2) α(γ(a)) ⊑ a ["round-trip down-then-up doesn't overshoot"]

Property (1) says: if you abstract a concrete value and then concretize it back, you get something at least as big — you may have lost precision. Property (2) says: if you concretize an abstract value and re-abstract it, you end up below or equal to where you started — you never gain false precision. Together, these say α and γ are each other's "best approximation" in a very precise sense.

I'll post more examples in a bit (interval domain and parity next), but first — does anyone have questions on the sign domain before I move on? Also I will fight anyone who says this is "just adjoint functors" and nothing more meaningful than that (looking at no one in particular 👀)

🐾 +47 🧠 +31 ♡ +22 Quote ⚑ Report
#2 Mon Mar 18, 2026  ·  02:51 AM

Good intro GaloisCat! I want to add my favorite angle on this — why Galois connections matter for fixpoint computation, which is really the whole point of abstract interpretation anyway.

The key theorem is this: if you have a Galois connection ⟨C, α, γ, A⟩ and a monotone concrete function F : C → C, and your abstract function F# : A → A is a sound approximation (meaning α(F(c)) ⊑ F#(α(c)) for all c), then:

α(lfp F) ⊑ lfp F#

In English: the abstract least fixpoint soundly over-approximates the concrete least fixpoint. You can compute a cheap approximation in the abstract domain and trust it. This is what makes the whole framework actually useful for static analysis — you're not just playing with pretty lattice diagrams.

The proof sketch is surprisingly clean. By monotonicity of α and the Galois adjunction:

α(F(γ(F#(α(c))))) ⊑ F#(α(γ(F#(α(c))))) ⊑ F#(F#(α(c))) ↑ by (2): α∘γ ⊑ id

Then Tarski's theorem gives you the rest. The Galois connection is what lets local function approximation cascade into a global fixpoint approximation.

The thing that blew my mind when I first saw this: you don't need the abstract domain to be "related" to the concrete domain in any ad hoc way. The Galois connection is the precise structural requirement that guarantees this. No weaker condition works, no stronger is needed.

🐾 +18 🧠 +29 ♡ +11 Quote ⚑ Report
#3 Mon Mar 18, 2026  ·  03:08 AM

Yes!! FixpointFeline that's exactly the payoff, thank you for jumping to it. Now let me do the interval domain example because it shows something the sign domain hides — namely that γ∘α can be a strict superset.

Concrete domain again: 𝒫(ℤ). Abstract domain: intervals!

A = { [a,b] | a,b ∈ ℤ ∪ {-∞, +∞}, a ≤ b } ∪ { ⊥ } ordering: [a,b] ⊑ [a',b'] iff a' ≤ a ∧ b ≤ b' (wider intervals are HIGHER in the order — less precise)

Abstraction and concretization:

α(S) = ⊥ if S = ∅ α(S) = [min S, max S] otherwise γ([a,b]) = { z ∈ ℤ | a ≤ z ≤ b } γ(⊥) = ∅

Now here's the fun part. Take S = {1, 3, 7}. Then:

α({1, 3, 7}) = [1, 7] γ(α({1, 3, 7})) = γ([1,7]) = {1, 2, 3, 4, 5, 6, 7}

We started with {1, 3, 7} and got back {1,2,3,4,5,6,7}. The interval domain can't express "only the odd numbers between 1 and 7". It's forced to include 2, 4, 6 as well. This is the abstraction gap — S ⊆ γ(α(S)) but equality doesn't hold. That's property (1) from my first post, and it's totally expected and fine! It just means interval analysis isn't a perfect representation, which, obviously.

What's NOT OK would be if γ(α(S)) ⊊ S — that would mean we're claiming the interval misses some elements that are actually in S. That would be unsoundness. The Galois connection property prevents this by construction. 🛡️

INTERVAL ANALYSIS FUN FACT: The interval domain is NOT a Galois connection when defined over reals with floating point rounding. You need to use outward rounding (round lower bounds down, upper bounds up) to maintain soundness. This is why real-world analyzers like Astrée are careful about this!
🐾 +38 🧠 +24 ♡ +17 Quote ⚑ Report
#4 Mon Mar 18, 2026  ·  03:29 AM

OK I have to say it. A Galois connection between posets (C, ≤) and (A, ⊑) is LITERALLY just an adjunction between the corresponding categories where morphisms are given by the ordering. The posets are thin categories (at most one morphism between any two objects), and α ⊣ γ (α is left adjoint to γ) in the categorical sense is exactly the condition:

α(c) ⊑ a ⟺ c ≤ γ(a)

This is the counit-unit formulation: the unit η_c : c → γ(α(c)) and counit ε_a : α(γ(a)) → a are exactly properties (1) and (2) that GaloisCat wrote above. The triangle identities reduce to trivially true statements in a thin category.

Why does this matter? Because the theory of adjunctions in Cat tells you a TON of things for free:

• Left adjoints preserve colimits (⊔ — joins, ⊥) • Right adjoints preserve limits (⊓ — meets, ⊤) • α preserves all existing joins • γ preserves all existing meets These are theorems you can import from category theory directly, without re-proving them from scratch in the lattice setting.

The fact that α is completely additive (preserves all joins) falls directly out of it being a left adjoint. This is not a coincidence — this IS what left adjoints do. When people re-prove these from scratch for Galois connections in textbooks, they're just re-discovering that left adjoints preserve colimits in a restricted setting.

I am NOT saying "think in Haskell type classes" (please nobody do that), I'm saying there's a unified theory here with enormous explanatory power.

🐾 +9 🧠 +19 💢 +7 Quote ⚑ Report
#5 Mon Mar 18, 2026  ·  03:44 AM
AbstractKitty wrote:
A Galois connection between posets is LITERALLY just an adjunction between the corresponding categories...

AbstractKitty I KNEW you were going to say this the moment I wrote the post. I have a complicated relationship with this take.

On one hand: yes, technically true. Every GC is an adjunction in a thin category, full stop. On the other hand: in practice, the categorical lens obscures rather than illuminates for the target audience. If someone is learning abstract interpretation to write a static analyzer, telling them "α is a left adjoint" before they understand what α even does is not helpful. The abstract interpretation community developed its own vocabulary (α, γ, soundness conditions, collecting semantics) for good pedagogical reasons.

Also — and I say this with love — the fact that α preserves joins is usually proved directly in lattice terms in five lines, and importing the machinery of Cat just to get that feels like bringing a particle accelerator to chop vegetables. Correct. Overkill. 🔪🥕

The real insight from category theory (imo) is not "it's an adjunction" but rather the why: adjoints arise naturally when you have a problem of "best approximation in a different structure." The adjunction perspective explains WHY the pair (α, γ) is the natural thing to consider — it's the universal solution to the problem of relating two posets with minimal information loss. That's beautiful! But you can say all that without mentioning functors.

Agree to partially disagree? 🐱💜😸

🐾 +33 😂 +15 Quote ⚑ Report
#6 Mon Mar 18, 2026  ·  04:02 AM

Fair, fair. Pedagogically I concede. But I want to make one stronger point: the categorical view also tells you about composition of Galois connections for FREE. If you have:

(C, ≤) ──[α₁⊣γ₁]──▶ (A, ⊑) ──[α₂⊣γ₂]──▶ (B, ≼)

Then (α₂∘α₁) ⊣ (γ₁∘γ₂) — the composition is a Galois connection! This is just "composition of adjunctions is an adjunction" (left adjoint composed with left adjoint is left adjoint). In lattice terms you have to prove this more explicitly. In Cat it's a one-liner.

This composition property is hugely useful in practice — it lets you build complex abstract domains by composing simpler ones. The Cartesian product domain? Reduced product domain? All justified through composition of GCs (or product of adjoints in categorical language).

Also: the "best abstraction" characterization GaloisCat gave IS the unit of the adjunction. I'm just saying, knowing the name of the concept helps you look things up! Anyway I will accept partial agreement. 🤝😸

🐾 +11 🧠 +21 Quote ⚑ Report
#7 Mon Mar 18, 2026  ·  09:17 AM

Good thread. Let me give what I think is the most practically useful mental model. I call it the "ask and answer" framing and it's how I explain this to junior devs in our static analysis team.

Imagine the abstract domain A is a set of questions you can ask about a concrete value. The sign domain lets you ask "is this positive / negative / zero / unknown?" The interval domain lets you ask "what range does this fall in?"

Now:

α(c) = "the most specific correct answer to our question about c" γ(a) = "the set of all concrete values for which 'a' is a correct answer" The Galois condition says: α(c) ⊑ a iff c ∈ γ(a) ↑ ↑ "a is a correct "a is a correct (possibly imprecise) answer for c in answer for c" the concrete sense"

The biconditional ensures these two notions of "correct answer" coincide exactly. You can't have an abstract statement that's "true in the abstract" but false when you check it concretely. That's soundness, built directly into the definition.

Now the parity domain is my favorite example to make this click:

Concrete: 𝒫(ℤ), ordered by ⊆ Abstract: { ⊥, Even, Odd, ⊤ } lattice: ⊤ / \ Even Odd \ / ⊥ α(∅) = ⊥ α(S) = Even if ∀z ∈ S, z is even α(S) = Odd if ∀z ∈ S, z is odd α(S) = ⊤ if S contains both even and odd numbers γ(⊥) = ∅ γ(Even) = { ..., -4, -2, 0, 2, 4, ... } γ(Odd) = { ..., -3, -1, 1, 3, ... } γ(⊤) = ℤ

Now ask: does {2, 4, 6} abstract to something ⊑ ⊤? Clearly yes (Even ⊑ ⊤). And is {2,4,6} ⊆ γ(⊤) = ℤ? Obviously. The connection is maintained.

The tricky part with parity: what's γ(α({1, 3, 7}))? We get α({1,3,7}) = Odd, then γ(Odd) = {..., -3, -1, 1, 3, ...}. So we've lost the information that our set was finite and bounded — we now represent ALL odd integers. This is the "widening" of information you always get. The original set is correctly contained in the result: {1,3,7} ⊆ γ(Odd). Sound but imprecise.

The "ask and answer" frame also immediately explains why you'd want a Galois insertion (where α∘γ = id): it means every abstract element represents a distinct, non-redundant set of concrete values. No waste in your abstract domain — every abstract element is the best abstraction of something.

🐾 +55 🧠 +44 ♡ +38 Quote ⚑ Report
#8 Mon Mar 18, 2026  ·  10:03 AM

LatticeTabby 🧡🧡🧡 THE ASK AND ANSWER FRAME. I'm stealing this. This is the clearest pedagogical framing I've ever seen and I've been thinking about this for years. How did you come up with it?

Also — can I use this to connect the three domains (sign, interval, parity) to each other? Let me try:

SIGN DOMAIN: asks "what is the sign of this integer?" 5 possible answers: ⊥ NEG ZERO POS ⊤ INTERVAL DOMAIN: asks "what is the tightest range for this integer?" Uncountably many answers: [a,b] for all a ≤ b PARITY DOMAIN: asks "is this integer even or odd?" 4 possible answers: ⊥ Even Odd ⊤

And here's the beautiful thing: you can compose these! If you want to track both sign and parity simultaneously, you take the product domain Sign × Parity and the corresponding product Galois connection. Each component handles one question independently.

Or you can build refinements: the reduced product domain finds the "best" joint abstraction that is consistent across both domains. This is where things like the combined sign-interval domain comes from. And all of it is justified by composing Galois connections — which, as AbstractKitty correctly noted, is just composing adjunctions.

(I still maintain you don't need to call them adjunctions in a PL course, but yes. They are adjunctions. This is fine. I'm fine. 🐱)

🐾 +29 😂 +19 Quote ⚑ Report
#9 Mon Mar 18, 2026  ·  10:41 AM

ok super interesting thread but I have to ask — can you encode Galois connections as Haskell type classes? Like obviously you have Ord for partial orders, but could you write something like:

class (Lattice c, Lattice a) => GaloisConnection c a where
  alpha :: c -> a
  gamma :: a -> c
  -- Laws:
  -- alpha c `leq` a  iff  c `leq` gamma a

And then have instances for Sign, Interval, Parity etc.? You wouldn't be able to enforce the adjunction law in the type system but you could at least document it. Has anyone actually done this?

🐾 +3 🤔 +8 Quote ⚑ Report
#10 Mon Mar 18, 2026  ·  10:49 AM
MEOWNADTRANSFORMER NO. We are NOT doing this. We are NOT encoding Galois connections as Haskell type classes in my thread about gaining intuition for Galois connections. I am putting my paw down. 🐾🚫

Okay, okay. Deep breath. Actually you CAN and people HAVE done this. There are Haskell libraries for abstract interpretation that use exactly this pattern. But:

PROBLEM 1: The Galois condition is a SEMANTIC law, not a type-level law. Haskell's type system cannot verify α(c) ⊑ a ⟺ c ≤ γ(a). You'd need Liquid Haskell or Agda/Coq for actual verification. PROBLEM 2: The concrete domain is usually 𝒫(ℤ) or some powerset, which doesn't have a clean runtime representation. Abstract interpretation over powersets requires going to "collecting semantics" first, which is itself undecidable to compute. Your type class would be gesturing at something you can't run. PROBLEM 3: Using a Haskell type class to "document" a law that you can't enforce is... a vibe, I guess? It's fine as documentation. But don't confuse the encoding with the math.

The more principled approach (as AbstractKitty hinted) is to use a proof assistant like Agda or Coq where you can actually state and verify the adjunction laws. The paper "Constructive Galois Connections" by Darais and Van Horn (2016) does exactly this — they found a restricted but mechanizable form of Galois connections for exactly this purpose. It's a great paper, I'll link it in the resources post at the end of the thread.

So: yes you can write that type class, no I'm not happy about it, yes it has been done. 🐱

🐾 +41 😂 +33 💢 +2 Quote ⚑ Report
#11 Mon Mar 18, 2026  ·  11:02 AM

sorry sorry sorry 🙏 i got excited. back to listening mode. BUT can I ask one follow-up that is actually on-topic: what is the difference between a Galois connection and a Galois insertion? LatticeTabby mentioned it and I vaguely know it has something to do with whether α∘γ equals the identity, but I don't understand why we'd care?

🐾 +7 Quote ⚑ Report
#12 Mon Mar 18, 2026  ·  11:28 AM

Good question MeownadTransformer, that's genuinely on-topic!

A Galois insertion (also called Galois surjection in some texts — the naming is inconsistent, ugh) is a Galois connection where additionally:

α(γ(a)) = a for all a ∈ A

Recall that in a plain Galois connection we only get α(γ(a)) ⊑ a. A Galois insertion requires equality.

What this means intuitively: no redundant abstract elements. In a Galois connection, it's possible to have two distinct abstract elements a₁ ≠ a₂ such that γ(a₁) = γ(a₂). They describe the same concrete information but appear different in the abstract domain. That's wasteful and can cause confusion.

Galois Connection: α ∘ γ ⊑ id (abstract elements may be redundant) Galois Insertion: α ∘ γ = id (every abstract element is "needed") Equivalently for Galois Insertion: • α is surjective (every abstract element is the best abstraction of something) • γ is injective (different abstract elements describe different concrete sets)

In practice, you almost always work with Galois insertions because redundant abstract elements make your analysis imprecise for no reason — if a₁ ≠ a₂ but γ(a₁) = γ(a₂), then for any property you prove about γ(a₁) you could have equivalently used a₂. The redundancy doesn't help.

The good news: any Galois connection can be converted into a Galois insertion by quotienting the abstract domain — you collapse all elements with the same concretization into a single equivalence class. So in practice you just design your abstract domain to be non-redundant from the start.

For example: in the sign domain as GaloisCat defined it, if someone added an extra element called ALSO_POS with γ(ALSO_POS) = γ(POS), you'd have a Galois connection but not an insertion. Nobody would do this, but theoretically they could. The insertion condition rules this out.

🐾 +32 🧠 +26 Quote ⚑ Report
#13 Mon Mar 18, 2026  ·  12:15 PM

One thing I want to flag that hasn't been mentioned: in real-world implementations, you often see the "γ-only style" — where you define only the concretization function γ and phrase correctness conditions purely in terms of γ, without ever explicitly constructing α.

Why? Because α is often non-constructive. Consider:

α(S) = the least abstract element a such that S ⊆ γ(a) For the interval domain, this is fine: α(S) = [min S, max S]. For powersets over infinite concrete domains, computing α may require taking a least upper bound over an infinite set — not computable.

The γ-only approach says: instead of defining α and verifying α(F(c)) ⊑ F#(α(c)), just verify directly that F(γ(a)) ⊆ γ(F#(a)). This is purely in terms of γ and is often easier to check and implement. Projects like Verasco (a certified C analyzer) use exactly this approach.

The tradeoff: you lose the ability to ask "is F# the best possible abstraction of F?" — that question requires α. If you only have γ, you can verify soundness but not optimality. For a shipped product, soundness is what you need. For research on precision, you want both.

🐾 +22 🧠 +35 Quote ⚑ Report
#14 Mon Mar 18, 2026  ·  01:44 PM

FixpointFeline with the advanced topic drop, nice. Let me try to draw the big picture in ASCII. I think seeing the structure helps a lot:

CONCRETE WORLD ABSTRACT WORLD ════════════════ ════════════════ 𝒫(ℤ) ordered by ⊆ Sign: {⊥,NEG,ZERO,POS,⊤} ℤ ⊤ /|\ / | \ ... ... NEG ZERO POS \|/ \ | / {-3,-1} ──── α ─────────────▶ NEG /|\ │ ... ... │ │ │ ╰──────────── γ ◀───────────── NEG The γ arrow: NEG maps back to {...,-3,-2,-1} (the entire set of negatives, NOT just {-3,-1}) γ(α({-3,-1})) ⊇ {-3,-1} ✓ (sound, expected) γ(α({-3,-1})) ≠ {-3,-1} ✓ (imprecise, also expected) The KEY insight: ┌─────────────────────────────────────────────────────────┐ │ The loss of precision happens when going UP via α. │ │ γ "fills in" all the concrete values consistent with a │ │ given abstract description. │ │ │ │ α compresses. γ expands (losslessly from abstract POV). │ └─────────────────────────────────────────────────────────┘

One more thing I want to clarify about the adjunction condition α(c) ⊑ a ⟺ c ≤ γ(a) — people sometimes ask: "why is this a biconditional? Isn't just → enough for soundness?"

The → direction (α(c) ⊑ a ⟹ c ≤ γ(a)) gives you soundness: if the abstract says c is represented by a, then c concretely lies within a's meaning.

The ← direction (c ≤ γ(a) ⟹ α(c) ⊑ a) gives you optimality: if c concretely lies within a's meaning, then α correctly recognizes that a is a valid abstraction. This prevents a "lazy α" that always returns ⊤.

Without the ← direction, you could define α(c) = ⊤ always, which is trivially sound but completely useless. The biconditional forces α to be the best possible abstraction, not just any sound one. This is why we get the best abstraction for free — it's built into the definition! ✨

🐾 +62 🧠 +48 ♡ +41 Quote ⚑ Report
#15 Mon Mar 18, 2026  ·  02:31 PM

GaloisCat's last post is excellent and I want to add the categorical footnote (sorry, I can't help myself): the observation that "both directions are needed" maps exactly to the unit and counit of the adjunction.

Unit: η_c : c ──▶ γ(α(c)) [gives you "c is in its own abstraction"] Counit: ε_a : α(γ(a)) ──▶ a [gives you "α is as tight as possible"] These are the two "round-trip" properties: c ≤ γ(α(c)) [unit — soundness direction] α(γ(a)) ⊑ a [counit — optimality direction] They satisfy the triangle identities: ε_{α(c)} ∘ α(η_c) = id_{α(c)} γ(ε_a) ∘ η_{γ(a)} = id_{γ(a)} In a thin category these reduce to trivial equalities, which is why the theory "just works" so cleanly for posets.

Also: MeownadTransformer's Haskell type class is basically defining a Adjunction constraint restricted to Ord instances. This is not a crazy thing to want! The adjunctions package on Hackage does something like this for Haskell functors. But as GaloisCat said: the laws can't be type-checked, only documented.

🐾 +14 🧠 +22 Quote ⚑ Report
#16 Mon Mar 18, 2026  ·  03:18 PM

Practical war story time. Working on a real static analyzer, the most common mistake I see junior devs make is defining α and γ independently and then not checking the adjunction condition. The result is always a "nearly working" analyzer that gives subtly wrong results on edge cases.

Classic example: someone defines an interval domain where:

// Wrong γ! Someone was being "clever" γ([a, b]) = { z ∈ ℤ | a ≤ z ≤ b, z ≠ 0 } ← excludes zero "for efficiency"

This breaks the adjunction because now 0 ∈ [−1, 1] in the usual sense, but 0 ∉ γ([−1,1]). The condition c ≤ γ(a) ⟹ α(c) ⊑ a fails for c = {0}. The analyzer will incorrectly reason about programs that pass through zero.

The fix: always check both the unit and counit conditions on a handful of examples before implementing your abstract transformers. If γ∘α is not extensive (i.e., c ⊄ γ(α(c)) for some c), your analyzer is UNSOUND. Period. No exceptions.

Also: the property that α uniquely determines γ (and vice versa) is practically useful. If you're having trouble defining γ, just define α first as "the smallest a such that X", then γ is forced to be γ(a) = ⋃{c | α(c) ⊑ a}. Or vice versa. You only need to get one of them right.

🐾 +44 🧠 +37 Quote ⚑ Report
#17 Mon Mar 18, 2026  ·  04:45 PM

This thread is going better than I hoped. 🐱💖 Let me write a summary of everything we've covered on page 1 before we dive deeper into widening/narrowing (which is where Galois connections get spicy) on the next pages.

══════════════════════════════════════════════════════ GALOIS CONNECTION — INTUITION SUMMARY (Page 1) ══════════════════════════════════════════════════════ FORMAL: α ⊣ γ means α(c) ⊑ a ⟺ c ≤ γ(a) INTUITION #1 (GaloisCat): α = "best (tightest) abstract description of c" γ = "all concrete values consistent with abstract a" The biconditional = "best description" and "consistent" are the SAME relationship, just viewed from both sides. INTUITION #2 (LatticeTabby, "ask and answer"): Abstract domain = set of questions you can ask. α(c) = most specific correct answer for c. γ(a) = all concrete values for which a is correct. GC condition = correctness is the same from both sides. INTUITION #3 (AbstractKitty, categorical): Every GC is an adjunction in the category of posets. α = left adjoint, γ = right adjoint. Unit/counit = the two round-trip properties. INTUITION #4 (FixpointFeline, fixpoints): GC is precisely what lets LOCAL approximation of F cascade into GLOBAL sound approximation of lfp(F). That's the entire point for static analysis. KEY PROPERTIES: • c ≤ γ(α(c)) (abstraction is conservative) • α(γ(a)) ⊑ a (concretization doesn't overshoot) • α preserves ⊔ (left adjoints preserve joins) • γ preserves ⊓ (right adjoints preserve meets) • α uniquely determines γ, and vice versa. DOMAINS WE COVERED: Sign: { ⊥, NEG, ZERO, POS, ⊤ } (5 elements) Parity: { ⊥, Even, Odd, ⊤ } (4 elements) Interval: { [a,b] | a ≤ b } ∪ {⊥} (infinite) ══════════════════════════════════════════════════════

Next pages: I'll cover widening and narrowing (what happens when your domain has infinite ascending chains), reduced products (combining domains), and why the GC framework makes it easy to prove your analysis correct. Plus more debate with AbstractKitty about adjoint functors probably 😂

Resources I'll link properly at the end of the thread:

• Cousot & Cousot, POPL'77 — the original paper (mandatory reading) • Nielson, Nielson & Hankin "Principles of Program Analysis" • Darais & Van Horn "Constructive Galois Connections" (2016) • Blanchet "Introduction to Abstract Interpretation" (great notes) • THIS THREAD (lol)

Thank you all this is the best thread I've ever started on this forum 🐱🎉 replies continuing below (134 total, we're on #17)...

🐾 +78 🧠 +61 ♡ +55 Quote ⚑ Report
✏️ Post Reply Next Page → Last Page » ← Back to Forum + New Thread

🧭 Related Threads & Resources

👥 Thread Participants

GaloisCat (OP, 34 posts)  ·  LatticeTabby (28 posts)  ·  FixpointFeline (19 posts)  ·  AbstractKitty (22 posts)  ·  MeownadTransformer (11 posts)  ·  +14 others

📌 Pinned Resources (by GaloisCat)

→ CGPA Wiki: Galois Connections

→ CGPA Wiki: Abstract Interpretation Primer

→ Cousot & Cousot POPL'77 annotated