CGPA

I am already writing Haskell. You cannot stop me.

Okay but actually, Haskell's lazy evaluation already gives you coinductive data "for free" in a certain sense — infinite lists, streams, cyclic structures are all natural. The key insight that applies to analysis is that codata types are greatest fixpoints:

-- Inductive (least fixpoint): finite trees
data Tree a = Leaf | Node a (Tree a) (Tree a)

-- Coinductive (greatest fixpoint): potentially infinite trees (codata)
data CoTree a = CoNode a (CoTree a) (CoTree a)
-- In Haskell this "just works" because laziness

-- A simple abstract domain for an analyser:
-- Instead of iterating UP to a fixpoint, we iterate DOWN from Top
type Narrowing a = Stream a  -- a (potentially infinite) descending chain

newtype Stream a = Cons { runStream :: (a, Stream a) }
-- this IS a final coalgebra for the functor F(X) = A × X

The point is: when you want to compute the greatest fixpoint of an abstract transformer F, you iterate F from ⊤ downward: ⊤, F(⊤), F²(⊤), ... This is a descending chain. If the lattice has finite depth (DCC), it stabilises. If not, you need narrowing — the dual of widening.

I'm currently hacking on a tiny interval analyser that tries to compute the greatest fixpoint of the "stay in bounds" transformer rather than widening toward the least. Early results: precision is actually better for safety-style queries. Obviously doesn't terminate without narrowing for loops though. More results incoming once I stop yak-shaving the typeclass hierarchy...

I'm going to push back slightly on the framing here, not because I think coinductive analysis is uninteresting, but because I want to make sure we're being precise about what "coinductive" actually buys you computationally vs. just being a different presentation of the same fixpoint computation.

The standard Galois connection framework can handle both μF and νF. Cousot & Cousot's 1979 paper already discusses greatest fixpoints in the context of safety. The question isn't really "inductive vs. coinductive" — it's about which fixpoint you want, and what your abstract domain approximates it.

This is the part where I want to see evidence. An anamorphism is just an unfold — it's the unique coalgebra homomorphism into the final coalgebra. The question is whether framing things this way gives you a better implementation strategy or better compositional structure, not whether it "works" in principle. In principle, everything is just a fixpoint iteration.

That said — bisimulation-based equivalence checking is a real thing and does use the coinductive structure non-trivially. Partition refinement algorithms (Paige-Tarjan, etc.) are essentially computing the greatest fixpoint of a bisimulation relation. The coinductive framing there is genuinely illuminating because it tells you you're looking for the largest relation with the bisimulation property, not building up evidence inductively.

So: interested but skeptical. Convince me there's something you can do with the coalgebraic framing that you can't do (or can't easily explain) without it.

Sorry to be the obvious question person but — can someone give a really concrete example of what a coinductive analysis would look like on an actual small program? Like, an actual piece of code with actual abstract states? I have a decent grip on the lattice theory but the coalgebra framing is still fuzzy for me.

I understand that bisimilarity is defined as the greatest fixpoint of some operator on binary relations. But I don't see how that directly maps to, e.g., "analyse this C function for buffer overruns."

Good question! Let me try. Consider a simple loop: while (x > 0) { x = x - 1; }

Standard abstract interpretation asks: what is the least invariant holding at the loop head? You iterate the abstract transformer from ⊥ upward. With intervals you'd eventually get something like [0, x_init].

The coinductive/greatest-fixpoint approach asks instead: what is the largest set of states from which the safety property "x stays non-negative" holds forever? You start from ⊤ (all states) and intersect backwards. For this example:

-- Abstract transformer post(S) = { x - 1 | x ∈ S, x > 0 } ∪ { x | x ≤ 0 }
-- Greatest fixpoint of the "safety" operator T(X) = X ∩ pre(X)
-- where pre(X) = { s | post(s) ⊆ X }

T(⊤)   = { x | x ≥ 0 }           -- ⊤ intersected with "stays safe from ⊤"
T²(⊤)  = { x | x ≥ 0 }           -- already stabilised!
-- νT = { x | x ≥ 0 }  ✓ the exact invariant, no widening needed

In this simple case the greatest fixpoint gives you the exact invariant immediately because the lattice is well-founded enough. The interesting (hard) cases are with complex loops where the descending chain from ⊤ doesn't stabilise — and that's where narrowing comes in. Narrowing is the dual of widening: instead of making sets bigger to force stabilisation, you make them smaller.

The coalgebra framing makes this natural: your program is a coalgebra c : S → F(S) (a transition structure). The safety property is a subset P ⊆ S that is a sub-coalgebra — i.e., it maps to F(P) ⊆ F(S). Finding the largest such P is finding the final object among all "safe" sub-coalgebras, i.e., the greatest fixpoint. @GaloisCat this is what the framing buys you: the compositional structure on sub-coalgebras is exactly the right structure to reason about safety modularly.

Okay, this is a fair point and I'll concede ground here. The modularity argument is real. If you have a coalgebra morphism f : (S, c) → (S', c'), then safety properties (sub-coalgebras) pull back along f. This is not obvious at all in the "just iterate your abstract transformer" framing — you'd have to argue separately about how your abstractions compose.

But here's my remaining concern: the concrete computation is still fixed-point iteration, just starting from ⊤ instead of ⊥. The coalgebraic framing provides beautiful semantic foundations and helps you understand what you're computing. But does it suggest different algorithms? Does it tell you anything new about convergence or precision?

I'll grant that for bisimulation-based analysis, the coinductive framing absolutely changes the algorithm. Partition refinement doesn't have a natural "just iterate from ⊥" dual. The coinductive structure there is computationally essential, not just semantically convenient.

Grudgingly warming up to this. Don't tell anyone.

Coming in from the automata theory angle: the entire framework of language equivalence checking via bisimulation is a direct practical application of coinduction. When you want to check if two NFAs accept the same language, the coinductive approach is to look for a bisimulation relation between their states.

There's beautiful work by Bonchi & Pous ("Checking NFA equivalence with bisimulations up to congruence", POPL 2013) on making this efficient via up-to techniques — enhancements of the coinduction proof method where instead of finding a full bisimulation you find a weaker relation that is nonetheless "contained in" bisimilarity. This is way faster in practice.

The up-to framing is interesting for program analysis too: rather than computing the full greatest fixpoint (which might be expensive), you compute a relation that's "almost" a bisimulation and use the up-to machinery to certify it. There's a nice categorical treatment via the "companion" — the largest compatible function, which subsumes most useful up-to techniques.

Does this count as "practical"? I think checking NFA equivalence is program analysis in some sense — you're checking if two regex-like patterns describe the same behaviour. And it ships in tools.

Update from the Haskell mines: I've got a minimal working example. Here's a coinductive interval analysis that computes the greatest fixpoint of a "stays safe" predicate for a simple counter program:

module CoinductiveInterval where

import Data.Maybe (fromMaybe)

-- Abstract domain: closed intervals (possibly empty)
data Interval = Empty | Iv Int Int  -- [lo, hi]
  deriving (Show, Eq)

-- Meet (intersection) — key operation for greatest fixpoint iteration
meet :: Interval -> Interval -> Interval
meet Empty _ = Empty
meet _ Empty = Empty
meet (Iv a b) (Iv c d) =
  let lo = max a c; hi = min b d
  in if lo > hi then Empty else Iv lo hi

-- "Pre-image" of safety property P under transition x -> x - 1
-- pre(P) = { x > 0 | x-1 ∈ P } ∪ { x ≤ 0 }
preSafe :: Interval -> Interval
preSafe (Iv lo hi) = Iv (lo + 1) (hi + 1)  -- shift by 1 for decrement
preSafe Empty     = Empty

-- Greatest fixpoint iteration: start from Top, apply T(X) = X ∩ pre(X)
-- This descends to the largest safe invariant
greatestFixpoint :: Interval -> [Interval]
greatestFixpoint top = iterate step top
  where step x = meet x (preSafe x)

-- νT for our example: [0, MAX_INT]  (non-negative reals stay non-negative)

Obviously this is a toy, but the structure is real. The iterate here gives you the descending chain — it's lazy (coinductive!) so you don't need to know in advance where it stabilises. You can check equality between consecutive elements to detect the fixpoint.

The thing I find elegant: the descending chain from ⊤ is a codata structure — it's potentially infinite, and you consume it lazily. The analysis itself is coinductive in the implementation sense, not just the semantic sense.

Ok I think I'm starting to get it. So the functor F determines the "type" of transitions? For a deterministic program F(S) = S (just a next state). For a nondeterministic program F(S) = 𝒫(S) (a set of possible next states). For a probabilistic program F(S) = 𝒟(S) (a distribution). And the final coalgebra in each case captures the "full observable behaviour" of any system of that type?

And then a Galois connection between the concrete domain (coalgebras over ℘(S)) and an abstract domain is just... abstract interpretation but for coalgebras? Is that the right mental model?

Sorry if this is basic, I'm genuinely trying to build intuition here.

Yes, exactly right! You've got it. The functor F encodes the "shape" of the transition step. Different choices of F give you different classes of systems:

• F(X) = X → deterministic transition systems (plain coalgebras)
• F(X) = 𝒫(X) → nondeterministic (powerset coalgebras)
• F(X) = A × X → streams / Mealy machines outputting from alphabet A
• F(X) = 𝒟(X) → Markov chains (probabilistic)

And yes — abstract interpretation over coalgebras is a real research direction. There's work on "coalgebraic abstract interpretation" where you define a Galois connection between the category of F-coalgebras (or some slice of it) and an abstract domain. The advantage is that you get correctness of the abstract analysis "for free" from the structure of the Galois connection, exactly as in Cousot-style abstract interpretation, but now uniformly over all system types determined by F.

This is not just theory. The μ-calculus model checker design is essentially this: you have a coalgebra (your Kripke structure), you have properties expressed in the μ-calculus (alternating least/greatest fixpoints), and the model checking algorithm is computing those fixpoints — using the coalgebra structure to decide what states to explore.

Can I bring up coinductive type systems specifically? Because I think this is an underexplored connection to program analysis.

In type theory, a coinductive type is exactly the carrier of a final coalgebra. If you have a coinductive type for, say, "infinite streams of integers," the type checker is essentially verifying that your corecursive definitions are productive — that every observation terminates. That's a form of guardedness analysis.

Now, guardedness checking is a program analysis! You're statically verifying a property (productivity/totality) of potentially infinite computation. The criterion used by Agda (and discussed in various papers) is a syntactic/semantic approximation of the coinductive property you care about. Sized types (Abel & Pientka) give you a more precise, type-theoretic handle on this.

So coinductive type systems → coinductive program analysis → actual practical tool (Agda). QED? 🐱

Also worth mentioning: the type theory / program analysis duality runs deep. A coinductive type system for a language where programs can diverge is essentially embedding liveness analysis into the type system. Whether a term has a "coinductive" type tells you something about its infinite behaviour. I keep meaning to write a post about this on the CGPA blog.

Fine. Fine! I'm convinced this is a real research area with real practical applications. Let me summarise what I think the thread has established so far:

Definitely practical, coinductive structure is essential:

• Bisimulation-based equivalence checking (NFA equivalence, process equivalence) — partition refinement is computing νF
• μ-calculus model checking — explicitly alternates μ and ν iterations
• Guardedness/productivity checking in Agda/Coq — coinductive type systems

Practical but coinductive framing is "optional" (semantically illuminating, not computationally essential):

• Safety invariant analysis via greatest fixpoint / backward iteration from ⊤
• Narrowing-based abstract interpretation

Promising but I want to see it ship:

• Coalgebraic abstract interpretation as a unified framework
• Anamorphism-based analysis algorithms
• MeownadTransformer's interval analyser

Good thread. AbstractKitty you owe me a reference list.