Is the difficulty of solving differential equations a law of nature? It certainly seems so those unfortunate ones of us who have had to do it! And I have done a little bit of writing on the topic that I thought might be interesting to share.
With the help of ☀️, Claude Code and a few holidays, I have gotten back into some of my old research topics around dynamical systems, category theory and simulations.
As part of that of that I have been building a new typed compositional language for dynamical systems, based on research that goes 20 years back to my PhD under Prof Ursula Martin. I am calling it Gimle (
gimlelabs.com).
As I work on Gimle, I keep discovering new side-quests, some of which I then turn into working papers or notes:
gimlelabs.com/papers/
One of these was to try to better understand the difficulty of finding solutions to dynamical systems and the link between this and reasoning about the termination of loops in programs.
The gist of the link goes like this:
When we describe dynamical systems in the terms of category theory, we compose them from a set of atomic operations, like integrators, adders, and multipliers, and we then compose using the structure of a traced monoidal category. Feedback then creates differential equations. In programming, we likewise compose programs from atomics, sequential and parallel composition and feedback. Both form traced monoidal categories. Trace = differential = programmatic loops.
In both worlds, the "hard to solve" objects are the ones with trace. The "solved" objects are trace-free. A trace-free dynamical system is a closed-form solution, no iteration needed. A trace-free program is a straight-line program, no loops. In both cases, "Solving" the system or program means eliminating the trace.
The bridge between these two already exists going back to Bainbridge (1972), and extended as part of my PhD project. Through this work we have a formal trace-preserving mapping from these two worlds into a common program logic, based on Hoare Logic. Since this mapping preserves trace, trace elimination on either side projects to the same problem in the middle.
This reframes "closed-form solvability" as a definability question: does the implicit function defined by the fixed point lie in your vocabulary of elementary functions?
f' = f is solvable if {exp} is in your vocabulary.
∫e^(-x²)dx is not if you only have elementary functions.
Same question on the program side — does your loop have a formula?
`for i in 1..n: s = i` → `s = n(n 1)/2` ✓
`for i in 1..n: s = f(i)` → ??? (generally no)
Now it gets interesting.
Trace elimination for programs is undecidable, it reduces to the halting problem. A loop has a closed-form replacement iff the computation terminates. The categorical bridge transfers this to the continuous side: determining whether an ODE has a closed-form solution is also undecidable.
This formalises something most mathematician intuitively feels: "most differential equations can't be solved in closed form." It's not just that we haven't found the right tricks. The impossibility is structural, connected to the halting problem not by analogy, but by traced monoidal functors.
The deeper view comes from Bainbridge's coalgebra/algebra duality. Traced morphisms are coalgebraic: they describe systems dynamically, via feedback. Trace-free morphisms are algebraic: they describe systems statically, via direct expressions. "Solving" is the action of mapping from coalgebra to algebra.
Still a lot of hand-waving around this, but I thought it was such an interesting observation that I wrote it up.
It is also the basis for another, more powerful, side-quest, that I call Simulation Learning. The idea being that perhaps to find these closed form solutions we need to be able to temporarily branch out and weaken the strict logic of our proofs to perform non-trivial trace-elimination that then inform the main proof.
Anyway, more on that later :)
If you are interested, here is the a short blog write-up and a link to the pdf note: "Trace Elimination as Closed-Form Discovery: A Duality Between Dynamical Systems and Programs"
gimlelabs.com/papers/trace-e…
gimlelabs.com/assets/papers/…