Step semantics in 5 minutes

The daitai algebra has one canonical state-transition relation:

Step : State × Lens × Rate -> State

Read it as: to advance the state, supply a lens that names which part of the state you intend to update, and a rate that says by how much.

Every effect in daitai-lang — UI updates, training steps, market events, sensor readings, AI inference outputs — is desugared to a Step call. There is no other way to advance state.

Why one relation?

Because the laws are simpler when there is only one relation to write laws about. With a single Step, we can publish two short axioms and a theorem that every program inherits for free.

Composition law

∀ q L₁ L₂ η.  Step(Step(q, L₁, η), L₂, η)
            = Step(q, L₁ ∘ L₂, η)

Two consecutive steps with the same rate can always be fused into one step with the composed lens. The compiler uses this to merge updates; the prover uses it to reduce proof obligations.

Information monotonicity

∀ q L η.  H(Step(q, L, η)) ≤ H(q)

A step cannot increase the entropy of the system relative to the lens it touches. This is the algebra's way of saying useful work decreases uncertainty, and it is enforced at type-check time.

A practical implication

If your training loop is written as a sequence of Step calls, the compiler can:

• fuse adjacent steps when their lenses commute,
• parallelize steps whose lenses are disjoint,
• and refuse to compile a loop whose composed step would violate monotonicity.

None of this requires you to write an annotation. The algebra carries the proof obligation; the compiler reads it.

Reading next

• The bra-ket primitives — the smallest interesting fragment of the algebra.
• The principles — where Step sits in the constitution.