Categorical Semantics

Mathematical foundations of Asgard circuits using category theory.

Computational Networks as Categories

Computational networks form a traced monoidal category over domain and target calculi. That structure pays off in two ways.

The first is a type system. Every atomic carries a fixed input/output degree, and every composition(f, g) requires d_out(f) = d_in(g) — checked statically, before any numerics run. Wiring errors surface at compile time as degree mismatches, not several layers into a simulation as a cryptic shape error.

The second is a proof system for circuit equivalence: two circuits connected by a chain of meaning-preserving rewrites compute the same function. Together they provide:

A static, principled way to compose circuits — with degrees checked at every connection point
Formal proof systems for circuit equivalence
Algebraic laws for circuit transformation

Network Grammar

Networks are defined using:

NETWORK:      <COMPOSITION> | <MONOIDAL> | <TRACE> | <ATOMIC>
COMPOSITION:  composition(<NETWORK>, <NETWORK>)
MONOIDAL:     monoidal(<NETWORK>, <NETWORK>)
TRACE:        trace(<NETWORK>)
ATOMIC:       var(<IDENTIFIER>) | const(<NUMBER>) | add
              | convolution(<NUMBER>) | id | multiplication
              | scalar(<NUMBER>) | split
              | deregister(<IDENTIFIER>) | register(<IDENTIFIER>)

Category Structure

Objects

Objects in the circuit category are types - specifications of input/output structure:

Number of streams
Dimension labels
Coefficient shapes

Morphisms

Morphisms are circuits - transformations between types:

f : A → B takes inputs of type A and produces outputs of type B
Morphisms compose: if f : A → B and g : B → C, then g ∘ f : A → C

Identity

For each object A, there is an identity morphism id_A : A → A:

circuit = Circuit.from_string("id")

The identity circuit passes inputs through unchanged.

Composition

Sequential composition: composition(f, g) means "apply f, then apply g".

composition(f, g) = g ∘ f : A → C

where f : A → B and g : B → C.

Identity Laws

composition(f, id) = f    (right identity)
composition(id, f) = f    (left identity)

Associativity

composition(f, composition(g, h)) = composition(composition(f, g), h)

This allows rewriting nested compositions without changing semantics.

Monoidal Structure

Parallel composition: monoidal(f, g) means "apply f and g independently".

monoidal(f, g) = f ⊗ g : A⊕C → B⊕D

where f : A → B and g : C → D.

Unit Object

The unit object I represents "no inputs/outputs":

monoidal(f, I) ≅ f
monoidal(I, f) ≅ f

Associativity

monoidal(f, monoidal(g, h)) ≅ monoidal(monoidal(f, g), h)

Interchange Law

The key property connecting composition and monoidal:

composition(monoidal(f, g), monoidal(h, k)) = monoidal(composition(f, h), composition(g, k))

This enables important circuit optimizations and transformations.

Diagram:

    A ─── f ─── B         A ─────────── B
        ⊗           →         f;h
    C ─── g ─── D         C ─────────── D
        ;                     ⊗
    B ─── h ─── E         B ─────────── E
        ⊗                     g;k
    D ─── k ─── F         D ─────────── F

Trace Structure

Feedback loops: trace(f) connects the last output back to the last input.

trace(f) : A → B

where f : A⊕X → B⊕X.

Trace Axioms

Naturality: The trace commutes with composition:

trace(composition(monoidal(f, id), g)) = composition(f, trace(g))

Vanishing: Trace of identity:

trace(id_{A⊕I}) = id_A

Superposing: Trace with monoidal:

trace(monoidal(f, g)) can be computed in terms of traces of f and g

Fixed-Point Interpretation

The trace computes a fixed point:

y = f(x, y)  →  y = trace(f)(x)

This is how differential equations become circuits:

dy/dt = g(y) becomes y = ∫g(y)dt
The integral creates a feedback loop requiring trace

Proof System

The categorical structure gives rise to a proof system for circuits:

Axioms

Identity laws: composition(f, id) = f, composition(id, f) = f
Associativity: Compositions can be re-parenthesized
Interchange: Monoidal and composition interact predictably
Trace axioms: Traces can be manipulated algebraically

Rewrite Rules

Circuits can be transformed using categorical axioms:

# Before: nested composition
"composition(composition(f, g), h)"

# After: re-associated
"composition(f, composition(g, h))"

# These are semantically equivalent!

Exact vs. approximate rewrites

The rewrites above are justified by the categorical axioms, so they provably preserve meaning — the transformed circuit computes the same function (denotationally; reordering operations can still change floating-point roundoff).

Other candidate identities depend on boundary/initial conditions. With fresh zero boundary state, composition(deregister(x), register(x)) removes the initial coefficient, so Asgard does not rewrite it to identity. The opposite order is identity for infinite streams, with equality limited to retained orders for finite buffers.

Approximate rewrites trade exactness for simplicity: truncating higher-order terms or replacing a subnetwork with a simpler one is not justified by the axioms alone. Such rewrites need numerical validation — for example, bounding the error by simulation.

Applications

The proof system enables:

Circuit Simplification: Reduce circuit complexity
Equivalence Proofs: Show two circuits compute the same function
Closed-Form Discovery: A circuit's trace encodes a feedback loop (an ODE, a recurrence); a trace-free circuit is a direct computation. Finding a closed-form solution amounts to finding a rewrite that eliminates the trace. We conjecture that, for expressive-enough circuits, this is as hard as eliminating a loop from a program — undecidable in general. (That most ODEs lack a closed form is a separate, differential-Galois genericity fact, not a corollary of that undecidability.) See Trace Elimination.
Optimization: Restructure for better performance

Atomic Morphisms

The category is extended with atomic morphisms that provide computational primitives:

Morphism	Type	Semantics
`add`	2 → 1	Element-wise addition
`multiplication`	2 → 1	Element-wise multiplication
`scalar(c)`	1 → 1	Multiply by constant
`const(c)`	0 → 1	Generate constant
`var(x)`	1 → 1	Variable lookup
`register(d)`	1 → 1	Integration
`deregister(d)`	1 → 1	Differentiation
`split`	1 → 2	Duplicate
`id`	1 → 1	Identity

Atomic Axioms

Each atomic has its own axioms:

Register/Deregister:

composition(register(x), deregister(x)) ≈ id  (up to boundary)

Scalar:

composition(scalar(a), scalar(b)) = scalar(a * b)
scalar(1) = id
scalar(0) = const(0)  (zeroing)

Add:

composition(monoidal(id, const(0)), add) = id  (additive identity)

Example: Circuit Transformation

Original Circuit

# (2x + 3y) computed inefficiently
circuit1 = Circuit.from_string(
    "composition("
    "  composition("
    "    monoidal(scalar(2.0), scalar(3.0)),"
    "    add"
    "  ),"
    "  id"
    ")"
)

Simplified Circuit

Using identity law composition(f, id) = f:

# Equivalent but simpler
circuit2 = Circuit.from_string(
    "composition("
    "  monoidal(scalar(2.0), scalar(3.0)),"
    "  add"
    ")"
)

Both circuits compute the same function, but circuit2 is simpler.

Next Steps

Compilation Process - Equation to circuit translation
Circuits - Circuit operations and combinators
Theory Overview - All theory topics