ステップ意味論を 5 分で

daitai 代数には、正準的な状態遷移関係が一つあります:

Step : State × Lens × Rate -> State

こう読みます — 状態を進めるには、状態のどの部分を更新するつもりかを示すレンズと、どれだけ進めるかを示すレートを与えよ。

daitai-lang のあらゆる効果 — UI 更新、訓練ステップ、市場イベント、センサー読取値、AI 推論出力 — は Step 呼出しに脱糖されます。状態を進める方法は他にありません。

なぜ一つの関係か？

法則について書く対象の関係が一つしかないとき、法則は単純になるからです。単一の Step のもとで、二つの短い公理と一つの定理を公開でき、それらをすべてのプログラムが無償で継承します。

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

同じレートでの連続する二つのステップは、合成されたレンズによる一つのステップに常に融合できます。コンパイラはこれを更新の併合に使い、証明器は証明義務の削減に使います。

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

ステップは、自らが触れるレンズに関するシステムのエントロピーを増やすことはできません。これは「有用な仕事は不確実性を減らす」という代数による言い換えであり、型検査時に強制されます。

訓練ループが Step 呼出しの列として書かれているなら、コンパイラは:

これらに注釈を書く必要はありません。証明義務は代数が担い、コンパイラがそれを読みます。