Theory

Mathematical foundations of Asgard and Linear Categorical Logic (LCL).

What is LCL?

Linear Categorical Logic (LCL) is a framework for modeling, simulating, and reasoning about dynamical systems. It has three main components:

Equations → Networks → Simulations

1. Equations: Define dynamical systems using standard mathematical notation
2. Networks: Computational circuits that represent the system uniformly
3. Simulations: Execute circuits under different mathematical interpretations

Key Features

Standard Mathematical Notation

Systems can be defined in many sensible ways:

• Differential equations
• Difference equations
• Closed-form solutions
• Composed and dependent systems

All using a standard, intuitive grammar similar to common mathematical notation.

Wide Range of System Types

LCL supports:

• Deterministic and stochastic systems
• Linear and non-linear
• Self-contained and composed systems
• Single and multi-dimensional dynamics

Calculus Independence

The definition and approximation steps are the same regardless of the underlying calculus:

• Real calculus (deterministic)
• Stochastic calculus (SDEs)
• Discrete calculus (sequences)

The difference only matters at simulation time.

Proof System

LCL comes with a built-in proof system for reasoning about dynamical systems. This enables:

• System Selection: Finding systems to fit datasets
• Reasoning: Proving properties about systems
• Algebraic Solving: Finding closed-form solutions mechanically

The LCL Pipeline

1. Define Equations

from gimle.asgard.equation.equation import Equation

# Define a differential equation
eq = Equation.from_string("diff(y, t) = scalar(-0.1, y)")

2. Compile to Circuit

from gimle.asgard.compile.compiler import compile_equation_to_circuit

# Translate to computational network
circuit, metadata = compile_equation_to_circuit(eq)

3. Execute with Calculus

from gimle.asgard.runtime.stream_evaluator import RealCalculus

# Choose mathematical interpretation
calculus = RealCalculus(center=0.0)

# Execute and evaluate
outputs, state = circuit.execute([input_stream], StreamState())
evaluator = StreamEvaluator(outputs[0], {"t": calculus})
values = evaluator.evaluate(t=time_points)

Translation Process

The translation from equations to circuits follows these steps:

1. Normalization: Normalize each equation according to axioms
2. Bounded Variables: Identify bounded variables for each equation
3. Isolation: Isolate each bounded variable on the left side
4. Resolution: Resolve operators and rewrite to isolate completely
5. Translation: Construct computational networks
6. Network Normalization: Apply rewrite rules
7. Unification: Connect identical inputs and outputs
8. Trace: Apply trace operators for feedback loops

Circuits as Categories

Computational circuits form a traced monoidal category. This mathematical structure provides:

• Composition: Sequential application (g ∘ f)
• Monoidal Product: Parallel application (f ⊗ g)
• Trace: Feedback loops (Tr(f))

These categorical properties enable formal reasoning and transformation of circuits.

Next Steps

• LCL Introduction - Detailed LCL overview
• Categorical Semantics - Category theory foundations
• Compilation Process - Equation to circuit translation