柱 · 03代数
daitai-algebra
数学的中核。状態 × 事象 → 状態、証明付き。
これは何か
daitai-algebra は他のすべての基礎となる形式系です。 少数のソート — Scalar、Distribution、RandomVar、Operator、State、Event — と、それらを合成する少数の演算子を定義します。 期待値 E、KLダイバージェンス KL、相互情報量 MI、エントロピー H、そして正準ステップ関係 Step(q, L, η) です。
代数は公開された書き換え規則の集合の下で閉じています。つまり、コンパイラ、証明器、人間の読者が式を正準形に変換し、その結果が観測等価であることを確信できます。慣習ではなく、構成によってです。
バージョン1.4は量子拡張を追加しました。同じ書き換え系がブラケット状態、ユニタリ演算子、測定崩壊をカバーし、古典代数は明らかな極限ケースとなります。
なぜ存在するか
本番ソフトウェアは — 機械学習、トレーディング、予測、不正検知において — 分布、勾配、期待値、情報について一日中話していますが、それを動かす言語はすべて型なしの浮動小数点として扱います。 代数は、整数算術が60年間享受してきたコンパイラレベルの保証を、これらの領域に与えるために存在します。
これはdaitai-langとプラットフォームの他の部分との間の契約でもあります。DPWはそれを読み、CGFはそれに対して署名し、サードパーティはソートを宣言し書き換えを証明することで新しいモジュールを公開できます。プラグインフレームワークも、ランタイム登録も、サプライズもありません。
コード例
step.algebradaitai-algebra
# 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)