Gimle Papers Working Paper
Trace Elimination as Closed-Form Discovery
A duality between dynamical systems and programs — where finding a closed-form solution to a differential equation is the same problem as eliminating a loop from a program. We show that both are undecidable in general, by reduction from the halting problem.
Two Worlds, One Structure
Dynamical systems and programs share the same categorical anatomy
Two fields reason about systems with feedback using strikingly similar mathematical structures, apparently without recognising the connection.
In dynamical systems, signal-flow circuits compose atomic operations (integration, addition, multiplication) via sequential wiring, parallel wiring, and a feedback operator called trace. In programming, sequential programs compose primitives (arithmetic, conditionals, assignments) via sequential execution, branching, and loops.
Both form traced monoidal categories. And in both, the “hard” morphisms are those with trace, while the “solved” morphisms are trace-free.
| Circuits (continuous) | Programs (discrete) | |
|---|---|---|
| Objects | Wire counts (degrees) | State spaces (types) |
| Morphisms | Signal-flow circuits | State transformers |
| Composition | Sequential wiring | Sequential execution |
| Monoidal | Parallel wiring | Disjoint union |
| Trace | Feedback / fixed-point | Loop / iteration |
| Trace-free | Closed-form solution | Straight-line program |
Solving an ODE = eliminating a loop.
In both categories, trace elimination — going from a traced morphism to a trace-free one — is the universal notion of “solving.”
The Two Categories
Circuits with feedback, programs with loops
$\mathbf{Circ}$ — signal-flow circuits
The continuous side
Objects are natural numbers (wire counts). Morphisms $f : m \to n$ are circuits with $m$ input wires and $n$ output wires, built from atomic operations: generators ($\exp$, $\sin$, $\cos$, constants), transformers (register, deregister, scalar), binary operations ($+$, Cauchy product), and routing (split, swap).
Under the real calculus, streams are Taylor coefficient sequences and register is formal integration. Trace implements Picard iteration: the fixed-point equation $Y = F(X, Y)$ is solved coefficient-by-coefficient.
A closed-form solution is a trace-free circuit — it computes the same function without feedback.
$\mathbf{Prog}$ — sequential programs
The discrete side
Objects are state spaces (types). Morphisms are state transformers. Atomic operations: arithmetic, conditionals, assignments, library calls. Composition is sequential execution; the monoidal product is disjoint union (branching over sum types).
Trace is loop iteration: $\mathrm{Tr}(f)$ repeatedly applies $f$, feeding part of the output back as input, until a termination condition is met. Hoare triples $\{P\}\, f \,\{Q\}$ express partial correctness.
A straight-line program is a trace-free morphism — it computes a direct mapping without iteration.
The Bridge
Verification functors land both categories in a common Hoare category
What might seem like a loose analogy turns out to be a formal correspondence, established by the Hoare category framework.
The Hoare category $\mathbf{H}$ has pre-ordered sets as objects and monotone relations as morphisms. Its trace is defined by existential quantification over the feedback variable:
Both $\mathbf{Circ}$ and $\mathbf{Prog}$ admit verification functors — strict traced monoidal functors that preserve all structure — into this common target.
Key property
Trace elimination in $\mathbf{H}$ amounts to showing that the existential quantifier $\exists z$ can be resolved by an explicit witness $z = \varphi(x)$. Since both verification functors preserve trace, a trace-elimination proof in either source category maps to the same existential-elimination problem in $\mathbf{H}$.
Bainbridge Duality
The coalgebra/algebra duality underlying the correspondence
The bridge through $\mathbf{H}$ has a deeper explanation in the coalgebra/algebra duality identified by Bainbridge and refined by Rutten and Turi–Plotkin.
Coalgebraic descriptions view systems as state-based machines that produce output and transition to new states — the “dynamic” view. Algebraic descriptions view systems as elements of algebras satisfying equational laws — the “static” view.
Trace elimination is the passage from coalgebra to algebra. The Hoare category sits at the junction: its objects carry both structure.
Coalgebraic (dynamic)
Traced circuits in Asgard: systems described via feedback and state transitions. Programs with loops: systems described via iteration and state updates.
“Run the system and watch what happens.”
Algebraic (static)
Closed-form solutions: direct expressions using elementary functions. Straight-line programs: direct computation without iteration.
“Write down the answer directly.”
Closed-Form Solvability
A definability property — relative to a choice of elementary functions
When does trace elimination succeed? The answer is uniform across both categories: a traced morphism is solvable if and only if the implicit function defined by its fixed point lies in a designated elementary subalgebra.
“Closed-form” is not intrinsic to the system — it is relative to a vocabulary. The ODE $f' = f$ has a closed-form solution relative to $\{\exp\}$ (namely $f = ce^x$) but not relative to $\{+, \times, \text{polynomials}\}$ alone.
In the Hoare category
Trace eliminability corresponds to resolving the existential $\exists z.\; (x,z) \; r \; (y,z)$ with an explicit witness $z = \varphi(x)$ expressible in the image of the elementary subalgebra.
Liouville’s theorem
The integral $\int e^{-x^2}\, dx$ is not expressible in classical elementary functions. The vocabulary $\mathcal{E}$ is fixed; the integral falls outside it.
Differential Galois theory
Characterises when a linear ODE has solutions in a given differential field extension. The “closed-form” question is always relative to the base field.
Loop optimisation
A compiler can eliminate for i in 1..n: s += i using $s = n(n+1)/2$, which requires quadratic polynomials in $\mathcal{E}$. But for i in 1..n: s += f(i) for arbitrary $f$ cannot be eliminated in general.
Undecidability
Trace elimination is undecidable — by reduction from the halting problem
For each Turing machine $M$ and input $w$, construct a morphism $f_{M,w}$ in $\mathbf{Prog}$ that performs one step of $M$'s computation: if $M$ has not halted, the output feeds back via trace; if $M$ has halted, it exits the loop with a fixed value $v$.
If $M$ halts on $w$: $\mathrm{Tr}(f_{M,w})$ is the constant function returning $v$ — a trace-free morphism.
If $M$ does not halt on $w$: $\mathrm{Tr}(f_{M,w})$ is the undefined partial function $\bot$. Since trace-free morphisms are total, no trace-free equivalent exists.
Therefore: $\mathrm{Tr}(f_{M,w})$ is trace-eliminable if and only if $M$ halts on $w$.
Theorem
The problem “given a traced morphism $\mathrm{Tr}(f)$ in $\mathbf{Prog}$, does there exist a trace-free morphism $g$ such that $[\![ \mathrm{Tr}(f) ]\!] = [\![ g ]\!]$?” is undecidable.
Corollary
If $\mathbf{Circ}$ is sufficiently expressive to encode the computations of $\mathbf{Prog}$ (which is plausible: the circuit language under the discrete calculus can simulate arbitrary recurrences), then the problem “does a given traced circuit have a closed-form solution?” is also undecidable.
“Most ODEs don’t have closed-form solutions” is a consequence of the halting problem.
This is not merely an analogy. The undecidability of trace elimination in $\mathbf{Prog}$ transfers to $\mathbf{Circ}$ via the structure-preserving span of verification functors through $\mathbf{H}$.
The Solvability Hierarchy
A classification that mirrors the arithmetic hierarchy
Trace-free
Already in the elementary subalgebra. No fixed-point iteration needed. Closed-form solutions, straight-line programs.
Trace-eliminable
Uses trace, but can be rewritten to a trace-free equivalent. The fixed point exists and is expressible. Solvable ODEs, eliminable loops.
Provably non-eliminable
Can be proved that no trace-free equivalent exists. ODEs with no elementary closed form, provably infinite loops.
Undecidable
The general problem of determining which level a morphism belongs to is undecidable.
Classical negative results
Richardson’s theorem (1968): it is undecidable whether an expression involving $+$, $\times$, $\sin$, $\exp$, $|\cdot|$, $\pi$, $\ln 2$ is identically zero. Even verifying a proposed closed-form is undecidable.
Pour-El & Richards (1981): the 3D wave equation can have computable initial data but non-computable solutions, showing continuous dynamics can amplify computational complexity.
Kovacic’s algorithm (1986): decidable criteria exist for second-order linear ODEs. The general nonlinear case remains open.
Cut-Elimination as Trace-Elimination
A third instance of the same structural pattern, from proof theory
In Gentzen's sequent calculus, the cut rule combines a proof of $\Gamma \vdash \Delta, A$ with a proof of $A, \Gamma' \vdash \Delta'$ into a proof of $\Gamma, \Gamma' \vdash \Delta, \Delta'$, with $A$ no longer appearing. Read categorically, this is a trace:
$$\mathrm{cut}_A(\pi_1, \pi_2) \;=\; \mathrm{Tr}^A\!\big(\pi_1 \otimes \pi_2\big).$$
The cut formula is the feedback variable. Gentzen's Hauptsatz — that every proof reduces to a cut-free (analytical) proof — is exactly trace-elimination in the category of sequents. Under Curry–Howard, this becomes $\beta$-reduction, and the Hauptsatz becomes strong normalisation.
| $\mathbf{Circ}$ | $\mathbf{Prog}$ | Sequent | $\lambda$-calc. |
|---|---|---|---|
| trace | loop | cut | $\beta$-redex |
| trace-free | straight-line | cut-free | normal form |
| trace elim. | loop elim. | cut elim. | normalisation |
| closed-form | terminating | analytic proof | strong norm. |
The halting problem breaks the symmetry.
Within a strongly-normalising calculus, trace-elimination is total: every fixed point is solvable, every proof reduces to an analytical one. Outside it — in Turing-complete programs, in nonlinear ODEs — trace-elimination is at best partial, and deciding when it succeeds is exactly as hard as deciding halting. By the same trade-off, a calculus that guarantees strong normalisation cannot be Turing-complete: closed-form solvability is bought at the price of computational strength.
This raises a natural question on the continuous side: which sub-PROs of $\mathbf{Circ}$ are “strongly normalisable” — the dynamical analogues of total programming languages? Linear ODEs with constant coefficients (matrix exponentials), polynomial vector fields with nilpotent linearisation, and Liouville–Arnold integrable Hamiltonian systems all sit on this side. Characterising the maximal tractable sub-PROs frames solver design — classical or learned — as the search for the largest sub-PRO on which trace-elimination is total.
Conclusion
Trace — whether as feedback, recursion, or iteration — is the universal mechanism for systems that refer to themselves. Eliminating it is the universal notion of “solving.”
The impossibility of eliminating trace in general connects the classical unsolvability of most differential equations to the undecidability of the halting problem — not by analogy, but by categorical structure.