Based on the Asgard paper. Read the full paper (PDF). For more details see the Asgard website and the Asgard GitHub repo.

Asgard is a programming language for dynamical systems. You write the equations that govern a system in a LEAN-inspired notation, and Asgard provides the full toolchain around them: a parser that turns the notation into a typed intermediate representation — circuits; a rewrite engine that simplifies those circuits through symbolic identities; a compiler that lowers circuits to JAX; and a runtime that simulates them as fast, differentiable code.

Its defining idea is that the mathematical structure of the system is the primary object of computation. The structure stays explicit and typed all the way from the equation to execution: circuits compose through typed interfaces, can be rewritten algebraically while provably preserving their meaning, and run under a choice of calculus — real, stochastic, or discrete — without any change to the model itself.

The pipeline

Asgard takes a model from LEAN-style notation to simulation in four stages — with the typed circuit as the representation that everything else operates on.

1. Parse. Equations are written in a LEAN-inspired notation. For example, f = f0 + int(f, x) is the ODE \(f’ = f\) with \(f(0) = f_0\). The syntax supports integration, differentiation, stochastic processes, lambda abstractions, and named parameters. The parser turns this notation directly into a circuit — the typed signal-flow representation described in the next section — rather than a plain syntax tree.
2. Rewrite. Symbolic identities simplify the circuit — for example, the fundamental theorem of calculus: diff(int(f, x), x) → f. These rewrites operate directly on the circuit, before any numerics are involved, and provably preserve its meaning.
3. Compile. The simplified circuit is lowered to a JAX program. A calculus — real, stochastic, or discrete — fixes how each atomic is interpreted, so one circuit can compile to different programs without any structural change.
4. Simulate. The runtime runs the compiled program to produce results — Taylor coefficients, sample paths, or sequence terms, depending on the calculus. Every execution path is fully differentiable.

Circuits: a typed intermediate representation

The heart of Asgard is the circuit — a typed signal-flow network built from atomic operations and the combinators that wire them together.

Atomics are computational primitives with fixed type signatures \((d_\text{in}, d_\text{out})\):

Operation	Type	Meaning
const(c)	\((0, 1)\)	Constant stream
param(n)	\((0, 1)\)	Named parameter stream
sin, cos, exp	\((0, 1)\)	Transcendental coefficient streams
id	\((1, 1)\)	Identity (pass-through)
register(x)	\((1, 1)\)	Formal integration
deregister(x)	\((1, 1)\)	Formal differentiation
scalar(s)	\((1, 1)\)	Multiply by a scalar
add	\((2, 1)\)	Pointwise addition
multiplication	\((2, 1)\)	Cauchy product
var(n)	\((1, 1)\)	Variable reference (replaced by id during trace wiring)
split	\((1, 2)\)	Duplicate a signal
swap	\((2, 2)\)	Exchange two signals
terminal	\((1, 0)\)	Discard a signal
stochastic_register	\((1, 1)\)	Wiener integral \(\int \cdot \, dW\)
jump_register	\((1, 1)\)	Poisson integral \(\int \cdot \, dN\)
black_box(n)	\((1, 1)\)	External callable

Combinators are the wiring rules that compose atomics into larger circuits:

• Composition \(f \circ g\) — feeds the output of \(f\) into \(g\). Requires \(d_\text{out}(f) = d_\text{in}(g)\).
• Monoidal product \(f \otimes g\) — runs \(f\) and \(g\) in parallel. Degrees add: \(d_\text{in} = d_\text{in}(f) + d_\text{in}(g)\).
• Trace — feeds the last output back to the first input: a feedback loop / fixed point. Degrees decrease by one.
• Power series composition — computes \(f(g(x))\) in coefficient space, the power series analogue of function composition.

As a concrete example, the equation \(f = f_0 + \int f \, dx\) (i.e. \(f’ = f\)) compiles to:

The feedback variable \(f\) enters via the trace, passes through register (integration), runs in parallel with \(f_0\), and the two signals are summed. The output feeds back.

Categorical structure

These circuits form a traced monoidal category. That is not just a tidy way to organise the type system — it gives us a proof system for circuit equivalence. The categorical axioms (associativity of composition, the interchange law for the monoidal product, naturality and vanishing for trace) mean that two circuits connected by a chain of rewrites compute the same function.

A handful of the laws:

• Identity — \(\text{comp}(\text{id},\; f) = f\)
• Scalar fusion — \(\text{comp}(\text{scalar}(a),\; \text{scalar}(b)) = \text{scalar}(ab)\)
• Cancellation — \(\text{comp}(\text{register},\; \text{deregister}) = \text{id}\)
• Associativity — \(\text{comp}(f,\; \text{comp}(g,\; h)) = \text{comp}(\text{comp}(f,\; g),\; h)\)

Because rewrites preserve meaning, the same machinery supports a range of operations on models:

• Simplification — reduce circuits to simpler equivalent forms, eliminating redundant operations, fusing scalars, and cancelling inverse operations.
• Equivalence proofs — show that two differently structured circuits compute the same function, without running them, by exhibiting a rewrite path between them.
• Approximation — rewrite a circuit into a structurally simpler, approximately equivalent form, truncating higher-order terms or replacing subnetworks.
• Formal composition — build complex models by wiring simpler circuits. The type system guarantees input/output degrees match at every connection point.
• Closed-form solutions — a trace-free circuit is a direct computation; finding a closed form is equivalent to finding a rewrite that eliminates the trace.
• Structure search — the rewrite system defines a search space over circuit topologies, each move a valid, typed rewrite, enabling beam search, genetic algorithms, or RL.

Closed-form solutions as trace elimination. A circuit containing trace represents a system defined by a fixed-point equation — an ODE, a recurrence, a feedback loop. A trace-free circuit is a direct computation: it maps inputs to outputs without iteration. We conjecture that a closed-form solution exists if and only if there is a valid rewrite from the traced circuit to a trace-free equivalent — reframing “does this ODE have a closed-form solution?” as a question about the rewrite theory of traced monoidal categories.

One circuit, many meanings

A compiled circuit is semantics-free. It describes structure, not numbers. To get a result you select a calculus, and the same circuit produces different results under different calculi without any structural change.

• Real \(\texttt{register} \to \int dt\) — streams are Taylor coefficients. Solves deterministic ODEs via Picard iteration in coefficient space, producing the full analytic structure rather than trajectories at discrete time points.
• Stochastic \(\texttt{register} \to \int dW,\; \int dN\) — multi-index expansion with Monte Carlo sampling. Supports Itô, Stratonovich, and jump-diffusion processes (Merton, Kou, Bates).
• Discrete \(\texttt{register} \to \text{unit delay}\) — streams are sequence terms. The same circuit structure that solves an ODE can generate the Fibonacci sequence. Multiplication becomes convolution.

In practice that’s really useful: you can build and validate a model deterministically, then run the exact same circuit stochastically to study noise — or discretely to get a recurrence — without changing anything. The circuit that solves \(f’ = f\) under the real calculus (giving the Taylor coefficients \(c_n = 1/n!\) of \(e^x\)) becomes a recurrence under the discrete one.

Execution model

Asgard offers several execution strategies, all fully differentiable — including through feedback loops.

Stream calculus (deterministic ODEs). Computes Taylor coefficients via Picard iteration in coefficient space, JIT-compilable as a single JAX loop. It produces the full analytic structure — all coefficients — rather than trajectories at discrete time points. Adaptive truncation order detects when coefficients become negligible and stops early.

Stochastic Taylor expansion (stream calculus meets Monte Carlo). Deterministic coefficients \(c_\alpha\) are computed once via Picard iteration over a multi-index tree. Each Monte Carlo path then samples iterated integrals \(I_\alpha\) and evaluates the sum. Because coefficients are shared across all paths, this is efficient for large ensembles. The multi-index tree encodes iterated integrals against \(dt\), \(dW\) (Wiener), and \(dN\) (Poisson), so jump-diffusion processes are handled natively. Antithetic variates provide up to 2× variance reduction, and convergence tiling handles long time horizons.

Time-stepping integrators (classical and stochastic schemes). The same circuit can be run under different numerical schemes without any structural change. Both Itô and Stratonovich interpretations are available — the Stratonovich variants use a Heun predictor-corrector.

Method	Order	Notes
Deterministic
RK4	4.0	Classical fixed-step, four evaluations per step
RK45	5.0	Adaptive step-size via embedded 4th/5th-order pair
Stochastic
Euler–Maruyama	0.5	Default for SDEs, single evaluation per step
Milstein	1.0	Uses JAX autodiff for \(\partial\sigma/\partial x\)
SRK1 (Platen)	1.0	Derivative-free, works with non-differentiable diffusions

Differentiability through feedback. Because all execution paths compile to JAX, circuits are fully differentiable — including through trace (feedback loops). At the converged fixed point, gradients are computed analytically via the implicit function theorem, \(\partial x^* / \partial \theta = -(I - \partial F / \partial x)^{-1} \, \partial F / \partial \theta\), implemented as a jax.custom_vjp. This enables gradient-based parameter identification and end-to-end optimisation of hybrid models.

Hybrid systems

Not every part of a dynamical system has a known analytic form. A chemical reaction rate, a turbulence closure, or a control policy may be best represented by a learned function.

Asgard supports this via the black_box atomic — a typed slot in the circuit that applies an external function (neural network, lookup table, any callable) to its input, with gradients flowing through automatically. The explicit structure captures what is known; the black box captures what is not. Crucially, the overall circuit remains typed and composable: the black box participates in the same categorical algebra as any other atomic.

That makes a spectrum of workflows possible within a single framework:

• Fit parameters of a known model structure — inverse problems solved by gradient descent through the full circuit.
• Train neural networks embedded within an otherwise explicit circuit — hybrid physics-ML with end-to-end differentiation.
• Search for structure using the rewrite system as a neighbourhood operator — beam search, genetic algorithms, or RL over circuit topologies.
• Couple systems — multiple interacting equations, each its own circuit, with correlated Brownian motions, jump processes, and bidirectional coupling via simultaneous Picard iteration.

The optimiser sees the entire circuit as a differentiable function from parameters to predictions, regardless of internal complexity. Known physics provides inductive bias; learned components fill in the gaps — explicit where possible, learned where necessary.

Three examples through the pipeline

The same structure means different things under different calculi. Three examples make the syntax–semantics separation concrete.

Deterministic ODE — the exponential, \(f’ = f,\; f(0) = 1\).

• Syntax. f = f0 + int(f, x)
• Circuit. trace(comp(mon(var(f0), comp(id, register(x))), add))
• Real calculus. Picard iteration yields \(c_n = 1/n!\) — the Taylor coefficients of \(e^x\), exact within the convergence radius.
• Discrete calculus. The same circuit computes a discrete recurrence. The structure is unchanged; the meaning depends on the calculus.

Stochastic process — geometric Brownian motion.

• Syntax. Y = sde(mu * X, sigma * X, X)
• Circuit. Contains register (drift \(\int \mu S\,dt\)) and stochastic_register (diffusion \(\int \sigma S\,dW\)), wired with trace for feedback.
• Execution. Stream calculus, Milstein (strong order 1.0), Euler–Maruyama, or Stratonovich — same circuit, different semantics. Both Itô and Stratonovich interpretations available.

Discrete recurrence — Fibonacci, \(f_n = f_{n-1} + f_{n-2}\).

• Circuit. Uses trace for feedback, register for the unit delay, and multiplication for sequence convolution with recurrence coefficients \(\sigma = (1, 1)\).
• Discrete calculus. Produces \(0, 1, 1, 2, 3, 5, 8, 13, \ldots\). Note the structural parallel with the exponential: both use trace and register, but the calculus determines continuous function vs discrete sequence.

Why it matters

Keeping the structure explicit means a model is more than something you run. The same circuit you simulate can also be inspected, composed with others, simplified, checked for equivalence, or re-interpreted under a different calculus — and because everything compiles to JAX, it stays fast and differentiable throughout.

That’s what makes Asgard a good foundation for the rest of the Gimle stack: together with Hugin (agentic reasoning) and Mimir (foundation model), it’s the layer that represents, manipulates, and runs the dynamical systems the others reason about and learn.

• Read the full paper (PDF) — the complete treatment, including the categorical foundations.
• Asgard website — documentation, the equation/circuit grammar, and worked examples.
• Asgard on GitHub — the source, the rewrite system, and the JAX runtime. Clone it and run uv run asgard ... to compile an equation and watch it execute.