LCL Introduction Categorical Semantics Compilation

Introduction to Linear Categorical Logic

LCL is a framework for modeling, simulating, and reasoning about dynamical systems.

Components

LCL has three main components: equations, networks, and simulations.

Equations

A dynamical system is defined as a system of equations that describe its dynamics. Examples include:

Networks

Equations are translated into computational networks - a unified representation of dynamical systems. Networks can be used to:

Simulations

Networks allow simulation to a given precision, approximating the evolution of a dynamical system given initial conditions and a choice of calculus.

Features and Advantages

Standard Mathematical Notation

Systems can be defined using intuitive mathematical notation:

# Differential equation
"diff(y, t) = scalar(-0.1, y)"

# Integral equation
"int(f, x) = g"

# System of equations
"diff(x, t) = y"
"diff(y, t) = scalar(-1.0, x)"

Wide Range of System Types

LCL supports:

Type Example
Deterministic ODEs, closed-form solutions
Stochastic SDEs, Brownian motion
Linear dy/dt = ay
Non-linear dy/dt = y²
Single-dimensional One variable
Multi-dimensional Coupled systems

Calculus Independence

Key insight: The definition and approximation steps are independent of the underlying calculus.

The same equation:

eq = Equation.from_string("diff(S, t) = scalar(0.05, S)")

Can be simulated as:

Mixed Calculi

Different dimensions can use different calculi:

evaluator = StreamEvaluator(
    stream,
    calculi={
        "t": DiscreteCalculus(),    # Discrete time
        "x": RealCalculus()         # Continuous space
    }
)

Proof System

LCL includes a proof system for reasoning about networks based on categorical semantics:

From Equations to Networks

Translation Process

  1. Normalization

    • Apply differential ring axioms
    • Simplify equation structure

  2. Variable Binding

    • Identify bounded variables for each equation
    • Solve boundedness constraints across system

  3. Isolation

    • Isolate bounded variable on left side
    • Apply algebraic rewrites

  4. Resolution

    • Resolve operators on LHS
    • Complete variable isolation

  5. Translation

    • Apply rewrite rules to produce circuit
    • Each equation becomes a circuit fragment

  6. Network Normalization

    • Apply categorical axioms
    • Simplify circuit structure

  7. Unification

    • Connect matching inputs and outputs
    • Use monoidal products

  8. Trace Application

    • Apply trace for feedback loops
    • Connect outputs back to matching inputs

Translation Rules

Equation Translation

<1> = <2>  →  composition(<2>, <1>)

Arithmetic Translation

<1> + <2>  →  composition(monoidal(<1>, <2>), add)
<1> - <2>  →  composition(monoidal(<1>, composition(scalar(-1.0), <2>)), add)
<1> * <2>  →  composition(monoidal(<1>, <2>), multiplication)

Integral Translation

∫ <1> d<2>  →  composition(<1>, register(<2>))

Derivative Translation

d/d<2> <1>  →  composition(<1>, deregister(<2>))

Simulating Networks

Approximation Steps

  1. Set truncation length - Determine coefficient expansion order
  2. Setup initial conditions - Free variables and fixed functions
  3. Apply calculus-specific rules - E.g., Itô to Stratonovich translation
  4. Compute coefficients - Run circuit on inputs
  5. Evaluate at points - Apply basis functions

Monte Carlo Simulation

For stochastic systems:

Reasoning About Networks

The categorical structure enables formal reasoning:

Identity Laws

composition(f, id) = f
composition(id, f) = f

Associativity

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

Interchange Law

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

Trace Properties

trace(composition(f, g)) can be rewritten using categorical rules

Example: Exponential Decay

Step 1: Define Equation

eq = Equation.from_string("diff(y, t) = scalar(-0.1, y)")

Mathematical form: dy/dt = -0.1y

Step 2: Compile to Circuit

circuit, metadata = compile_equation_to_circuit(eq)

The circuit uses trace for the feedback: y = -0.1 ∫y dt

Step 3: Execute

outputs, state = circuit.execute([input_stream], StreamState())

Step 4: Evaluate

evaluator = StreamEvaluator(outputs[0], {"t": RealCalculus()})
y_values = evaluator.evaluate(t=jnp.linspace(0, 10, 100))

Result: Exponential decay y(t) = y₀ e^(-0.1t)

Next Steps