📌 Coinductive Program Analysis — Is Anyone Actually Doing This?

Alright, I've been lurking on my own thread for the past few days trying to synthesise everything that's been said here. The discussion went way further than I expected and I feel like there's actually enough material here for a paper.

So I drafted an abstract. Rough, very rough. Posting it here to get feedback before I send it anywhere:

Very draft-y. The "translation functor" claim is aspirational — I have the construction for a specific class of domains but not the general case yet. Feedback welcome.

Okay so this is kind of funny timing — I've been working on exactly this for the last few months and I finally pushed the repo to GitHub last night. Here's the link:

The core of it is a type class hierarchy that treats abstract domains as coalgebras over a base functor F. The anamorphism gives you the abstract semantics "for free" from the coalgebra structure:

It's very much a research prototype — don't use it in production. But the tests on the stream examples from pages 1 and 2 of this thread work correctly. Productivity and liveness both check out.

AbstractKitty, want me to add you as a contributor? I think your abstract + this impl could become an actual workshop paper.

I've been putting off saying this for a few pages but I suppose I've been cornered. Fine.

This thread changed my mind.

I came in here ready to dunk on coinductive analysis as pure theory-brained category-cat navel-gazing with zero practical relevance. And I still think a lot of coalgebra papers are written specifically to obfuscate the fact that they contain 3 pages of content padded with 30 pages of diagrams. But:

• The productivity analysis use-case (page 2, posts 18–22) is genuinely not expressible cleanly via lfp. I was wrong about that.
• MeownadTransformer's code above is real and not just a thought experiment.
• AbstractKitty's draft abstract is actually coherent and the bisimulation soundness argument is the right move.

I maintain that the Galois connection formulation is still the right backbone and that the "translation functor" in the draft abstract needs to be made precise (the functoriality conditions aren't trivial). But the core claim stands. I was wrong. There, I said it.

Now can someone explain to me why widening even makes sense in the coinductive setting? If you're computing gfp, widening should make things bigger, not smaller. That's backward from the usual. MeownadTransformer's widen above widens toward top, which is the gfp initialisation point, so it's actually shrinking the over-approximation on each step... right? Am I reading this correctly?

SCREAMING. I never thought I'd see the day. Screenshot saved forever. 🖼️

Yes! Great question and I was going to ask this too. The intuition is:

• In the inductive (lfp) setting: we start at ⊥ and widen upward to force convergence. Widening is "jump to something bigger".
• In the coinductive (gfp) setting: we start at ⊤ and narrow downward toward the fixpoint. But convergence isn't guaranteed either! So "coinductive widening" is actually a kind of forced upward jump during the narrowing descent — it's more like a backtracking escape hatch.

MeownadTransformer's widen x (f x) is confusingly named — it should maybe be called accelerate. It joins the current point with the transfer-function image and jumps if we're cycling. In the gfp case this is still sound because you're staying ≥ the fixpoint (you can't over-shoot below).

Anyway — the main reason I'm posting: we should start a reading group. This thread has clearly assembled the cats who care about this stuff. I propose:

You're completely right and I've already pushed a commit renaming it. The README now has a proper explanation of the semantics. GaloisCat's confusion was valid and I should've documented this better.

Also — reading group: yes, absolutely yes. I'll set up the Discord event. I can lead the coalgebra chapters since I've read Jacobs front-to-back already (send help). AbstractKitty can handle the abstract interpretation side.

And yes AbstractKitty, I've already sent the GitHub collaborator invite 😸

Okay I have been watching this thread from the sidelines wearing my wiki-editor hat and I need to say: this is exactly the kind of thread the CGPA wiki needs a page for.

I'm proposing a new wiki article:

I'll start a draft in the wiki sandbox. ΛatticeWhiskers or any other mod: is this in scope for the main wiki? I know we've been trying to keep the theory pages at an accessible level but I think there's a way to write this that's readable with just the coalgebra primer prereq.

Also: this thread is an argument that the CGPA wiki needs more theory depth. We've had this discussion on the meta board before and I think the evidence is now in front of us.

I will have you know that updating one's priors in response to evidence is the epistemically correct behaviour, and if you screenshot that I will systematically undermine every argument you make about domain theory for the next calendar year.

That is not a threat. It is a promise and a lattice.

De-lurking for the first time in like four months just to say: this is the best thread on this forum since the denotational-vs-operational semantics debate of 2023. Archiving this in my own notes.

AbstractKitty — the abstract looks great. Tiny suggestion: the phrase "coinductive proof principle" might confuse reviewers who aren't from the coalgebra world. Consider "greatest-fixpoint induction principle" or just "coinduction (Pous & Sangiorgi, 2012)" with a citation. Sounds more familiar to the SAS/POPL crowd.

Also the "translation functor" framing is interesting but you might want to be careful — functoriality of the translation between Galois-connection lattices and the coinductive domain category is going to get asked about in review. Make sure you have the naturality squares ready.

Good luck. I'll read the preprint when it's up.

This is an excellent point and I've updated the draft. Pous & Sangiorgi is exactly the right citation for that audience. Thank you, lurker-who-emerges-bearing-gifts 🎁

GaloisCat this is the most you've ever sounds like a fully functional scientist and I mean that with complete sincerity and also I will absolutely be quoting this in the paper acknowledgements section ("we thank GaloisCat for updating priors").

Accepting MeownadTransformer's collaborator invite now. Let's do this. 🐾

Late to this thread but I want to add one thing that hasn't been mentioned: the connection to up-to techniques. If you're using bisimulation as your soundness argument (as AbstractKitty's draft proposes), the proofs get enormously simpler if you use coinduction up-to rather than bare coinduction. Pous & Sangiorgi 2012 covers this extensively.

Specifically: bisimulation up-to contextual closure gives you a much coarser equivalence that still respects the observable properties you care about. This could be the key that makes the "translation functor" claim tractable — you don't need full functoriality if you have the right up-to technique.

Just dropping this here before someone reinvents it from scratch in the paper 🐱

Quick update: I've started the wiki draft in the sandbox. It's very rough but the structure is there. If anyone wants to contribute before I move it to mainspace, ping me or just edit directly (sandbox is open):

→ wiki/Coinductive_Program_Analysis SANDBOX DRAFT

I've pulled in the core definitions from this thread (with attribution), linked MeownadTransformer's GitHub, and stubbed out the "open problems" section. That section currently has three entries:

• Widening/narrowing in gfp iteration — is there a canonical framework?
• Translation functor between Galois-connection and coalgebraic domains — characterise the naturality conditions
• Scaling to non-stream programs (what's the right functor for control flow?)

BisimulationBea — adding the up-to techniques note right now, thank you.

I mostly want to ask: is anyone thinking about the complexity side of this? Gfp iteration starting from ⊤ is dual to lfp from ⊥ but in practice the abstract domains we care about for coinductive analysis might have very different structural properties. For stream abstractions you often have infinite descending chains (even in abstract domains!) which makes the widening question non-trivial.

Specifically: do the coinductive abstract domains in MeownadTransformer's framework satisfy the descending chain condition? If not, gfp as written might not terminate without a very careful widening strategy.

Not trying to block progress on the paper — the framework is clearly interesting and right. Just flagging this as something to address in the "limitations" section before reviewers do.

They don't in general, you're right. The current prototype implicitly assumes the abstract domains are finite (or at least have finite height in the relevant direction), which is fine for the stream interval domains I've been using but won't hold for, say, arbitrary trace properties.

I've opened an issue on the repo: #13 — DCC assumption: document and check. This is going into the paper's limitations section, and also it's probably the next research problem to solve after the paper. KleeneKitten — do you want to be on the author list? This seems like your wheelhouse.

Good thread everyone. This started as AbstractKitty asking "is anyone actually doing this" and the answer turned out to be "kind of, messily, but now more so." 🐱