Trace Elimination
Closed-form solutions, framed as a question about the rewrite theory of circuits.
This page is exploratory. It sketches a research direction, not settled Asgard machinery, and it assumes some background (traced monoidal categories, and — toward the end — the Curry–Howard correspondence). The central characterisation is stated as a conjecture, and the connections to programs and proof theory are analogies we find suggestive, not theorems we have mechanised.
Closed-form solutions as trace elimination
A circuit that contains trace represents a system defined by a fixed-point
equation — an ODE, a recurrence, a feedback loop. The trace feeds part of a
circuit's output back to its input, and the runtime solves for the fixed point
(under the real calculus, by Picard iteration in coefficient space).
A trace-free circuit is different: it maps inputs to outputs by a direct computation, with no feedback and no iteration. It is a closed form.
That suggests a structural way to think about "solving". Fix an elementary vocabulary — the atomics you allow in an answer (say ${+, \times, \exp, \sin, \cos}$). Then:
Conjecture. A closed-form solution (relative to that vocabulary) exists if and only if the traced circuit has a trace-free equivalent built from the vocabulary.
Two cautions keep this honest. First, "has a trace-free equivalent" is a semantic statement (some trace-free circuit computes the same function); whether Asgard's rewrite system can actually find it is a separate question of rewrite-system completeness. Second, solvability is always relative to the vocabulary — the same system can be closed-form over one set of elementary operations and not another (see below). With those caveats, the reframing turns "does this ODE have a closed form?" into a question about the rewrite theory of traced monoidal categories.
A duality between dynamical systems and programs
The reframing is suggestive because circuits are not the only things that form a traced monoidal category. Sequential programs do too:
Dynamical systems (Circ) |
Programs (Prog) |
|
|---|---|---|
| Objects | wire counts | state spaces (types) |
| Composition | sequential wiring | sequential execution |
| Monoidal product | parallel wiring | branching (sum types) |
| Trace | feedback loop | loop iteration |
| Trace-free morphism | closed-form solution | straight-line program |
In both settings the "hard" morphisms are the ones with trace, and the "solved" morphisms are trace-free; in both, trace elimination — going from a traced morphism to a trace-free one — is a natural notion of solving. Solving an ODE and eliminating a loop from a program start to look like the same move.
One piece of this is solid: in the category Rel of relations, the trace is literally existential quantification over the fed-back wire,
$$x ;\mathrm{Tr}(r); y \iff \exists z.\ (x, z), r, (y, z),$$
so eliminating a trace there means resolving that $\exists z$ with an explicit
witness $z = \varphi(x)$. Whether both Circ and Prog map into a common
relational target by structure-preserving functors — so that a single
"witness-elimination" problem underlies both — is a construction we find
plausible but do not prove here.
Undecidability — where it is established, and where it is conjectural
On the program side the story is a theorem. Encode a Turing machine $M$ on input $w$ as a program morphism $f_{M,w}$ that performs one step of $M$: if $M$ has not halted, the output feeds back through trace; if it has halted, the loop exits with a fixed value. Assuming the atomics are total:
- If $M$ halts on $w$, $\mathrm{Tr}(f_{M,w})$ denotes a constant function, which has a trace-free equivalent.
- If $M$ does not halt, $\mathrm{Tr}(f_{M,w})$ denotes the undefined partial function; since trace-free morphisms here are total, no trace-free equivalent exists.
So $\mathrm{Tr}(f_{M,w})$ is trace-eliminable exactly when $M$ halts on $w$, and
deciding trace elimination in Prog would decide the halting problem — hence
it is undecidable.
Does that transfer to circuits? Not automatically: sharing traced-monoidal structure is not enough (plenty of traced monoidal categories are perfectly decidable). The transfer needs Asgard's circuit language to be expressive enough to encode these Turing-machine computations — plausible, since circuits under the discrete calculus can simulate arbitrary recurrences, but not something we establish here. So:
Conjecture. For a sufficiently expressive circuit vocabulary, deciding whether a given traced circuit has a closed-form solution is undecidable.
A related but separate fact is worth not conflating with this one: that most ODEs have no elementary closed form. That is a genericity result from differential Galois theory (Liouville, Morales–Ramis) — a statement about how rare solvable systems are, not a corollary of the halting problem. The two sit side by side: one says deciding solvability is hard, the other says solutions are usually absent.
Closed-form is relative to a vocabulary
Trace-eliminability is not intrinsic to a system; it is relative to the elementary operations you allow in the answer. The ODE $f' = f$ has a closed-form solution relative to ${\exp}$ (namely $f = c,e^x$) but not relative to polynomials and ${+, \times}$ alone. Enlarging the vocabulary of elementary circuits enlarges the set of systems you can solve in closed form.
This reframes solver design — classical or learned — as the search for a sub-theory on which trace elimination is total: the dynamical analogue of a total (strongly-normalising) programming language. Linear ODEs with constant coefficients (matrix exponentials) are a clean example of the solvable side; integrable Hamiltonian systems are solvable by quadratures, which is weaker than elementary closed form.
An analogy with cut elimination
The same shape appears in proof theory, and we offer it as an analogy rather than a theorem. Gentzen's cut rule combines two proofs through a shared formula that then disappears. Its Hauptsatz — every proof reduces to a cut-free one — plays, for proofs, the role trace elimination plays for circuits: removing the detour and leaving a direct object. Under Curry–Howard, cut-free normalisation corresponds to strong normalisation of $\beta$-reduction. (The standard categorical reading of cut is composition and of the Hauptsatz normalisation; reading the shared formula as a trace is the nonstandard lens we are trying on here.)
The trade-off that lens highlights is real, though: within a strongly-normalising calculus every expressible recursion terminates, so "solving" is total — but such a calculus cannot be Turing-complete. Outside it — in Turing-complete programs, in nonlinear ODEs — solving is at best partial, and deciding when it succeeds is as hard as deciding halting. Closed-form solvability is bought at the price of computational strength.
Why it matters for Asgard
Even as a conjecture, keeping the trace explicit in the circuit makes these questions things you can compute on:
- Simplification and equivalence are exact, axiom-justified rewrites (see
Categorical Semantics). Finding a closed form
is the special case that removes every
trace. - Structure search — beam search, genetic algorithms, or RL over the rewrite system — is a search for a trace-eliminating rewrite path. The conjectured undecidability in general is exactly why this is a search, not a decision procedure.
- Restricting to a solvable sub-theory (e.g. linear systems) is what makes closed-form discovery tractable where it is tractable.
Next Steps
- Categorical Semantics — the traced monoidal structure and the exact rewrite laws.
- Compilation Process — how an equation becomes a traced circuit in the first place.
- Coefficient Semantics — what the trace computes numerically, coefficient by coefficient.