daitai-algebra
The mathematical core. State × Event → State, with proofs.
What it is
daitai-algebra is the formal system underneath everything else. It defines a small set of sorts — Scalar, Distribution, RandomVar, Operator, State, Event — and a small set of operators that compose them: expectation E, Kullback–Leibler divergence KL, mutual information MI, entropy H, and the canonical step relation Step(q, L, η).
The algebra is closed under a published set of rewrite rules. That means a compiler, a prover, or a human reader can transform an expression into a canonical form and be certain the result is observationally equivalent — not by convention, but by construction.
Version 1.4 adds the quantum extension: the same rewrite system covers bra-ket states, unitary operators, and measurement collapse, with the classical algebra as the obvious limiting case.
Why it exists
Production software talks about distributions, gradients, expectations, and information all day long — in machine learning, in trading, in forecasting, in fraud detection — but the languages that ship that software treat all of these as untyped floats. The algebra exists to give those domains the same compiler-level guarantees that integer arithmetic has had for sixty years.
It is also the contract between daitai-lang and the rest of the platform. DPW reads it, the CGF signs against it, and any third party can publish a new module by declaring its sorts and proving its rewrites — no plugin framework, no runtime registration, no surprises.
A code example
# Canonical step relation, version 1.4.
sort State, Event, Lens, Rate
op Step : State × Lens × Rate -> State
# Composition law.
axiom step-compose :
∀ q L₁ L₂ η. Step(Step(q, L₁, η), L₂, η)
= Step(q, L₁ ∘ L₂, η)
# Information-theoretic refinement.
theorem step-monotone :
∀ q L η. H(Step(q, L, η)) ≤ H(q)