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. This mathematical structure provides:

A principled way to compose circuits
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!

Applications

The proof system enables:

Circuit Simplification: Reduce circuit complexity
Equivalence Proofs: Show two circuits compute the same function
Closed-Form Discovery: Find analytical solutions
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

LCL Introduction - Overview of LCL
Compilation Process - Equation to circuit translation
Operations Reference - Circuit operations