README.md

adaptive-msm Documentation

Complete documentation for the crate: theory, design, architecture, engineering, usage, science, and machine-checked proofs. Start with the reading path that matches your goal.

Reading paths

I want to…	Path
use the crate	Getting started → Learner guide / WFST guide → Cookbook
understand the ideas	MSM metric → Tropical semiring → WFST foundations → Online learning / FPTL
understand the code	Design overview → Module structure → Data flow
evaluate correctness	Formal verification map → Embedding proof → Regret & the honest gap
judge performance	Complexity & performance → Benchmarks
know the caveats	Known issues → ADRs

Contents

Theory — what the ideas are

• MSM metric — Move/Split/Merge, the $C(a,b,c)$ cost function, the DP recurrence, and why MSM (unlike DTW) is a true metric.
• Tropical semiring — min-plus algebra; why shortest path is minimum-cost alignment.
• WFST foundations — weighted transducers, path weight, lazy composition, and the trait contracts.
• Online learning / FPTL — FPL → tropical losses; and the honest gap between that theory and this learner.

Design — why it is built this way

• Overview — the two subsystems; the package cycle this crate exists to break.
• The learner — config, the explore/observe loop, the FPTL gradient bug and its fix.
• MsmWeight semiring — data-dependent costs; where the algebra is lawful and where it is not.
• MSM-as-WFST embedding — the lattice, the two engines, correctness.
• Decisions (ADRs) — 0001 extract to break the cycle · 0002 scalar FD vs. FPL · 0003 label quantization

Architecture — how the pieces fit

• Module structure — layout, the feature-gated boundary, the public API surface.
• Data flow — the learner round and the WFST build→expand→search flows.

Engineering — how it behaves in practice

• Build & features — wfst (default) vs. learner-only; dependencies.
• Complexity & performance — $O(mn)$ distance, $O(n^2)$ lattice, measured.
• Caching — CachePolicy, eviction, memory bounds.
• Security & robustness — no unsafe, NaN/∞ handling, determinism, resource caps.
• Known issues — resolved robustness items and remaining, intentional trade-offs.

Usage — how to drive it

• Getting started · Learner guide · WFST guide · Cookbook

Scientific — evidence, not assertion

• Methodology — CPU pinning, determinism, reproduction (scripts/run-experiments.sh).
• Benchmarks — measured timings on real hardware.
• Ledger — FPTL gradient bug · E1 learner convergence · E2 WFST state scaling
• Raw data in scientific/data/; figures in scientific/figures/.

Formal — machine-checked proofs

• Map — what is proven, where, by whom.
• Upstream references — the liblevenshtein / lling-llang theorems we cite (with re-check commands).
• MsmWeight homomorphism — proof (mechanized: formal/rocq/MsmWeightHomomorphism.v).
• Embedding equivalence — shortest path = MSM distance (mechanized: formal/rocq/EmbeddingEquivalence.v).
• Regret & the honest gap — a convergence theorem is proven; the FPTL regret bound is not claimed.
• Gate: docs/formal/verify.sh (Rocq coqc axiom-freeness + TLA+ TLC).

Diagrams & archive

• diagrams/ — PlantUML sources (.puml) and rendered SVGs.
• archive/ — the superseded ancestor design doc, kept for lineage.

Conventions

• Math is MathJax with GitHub delimiters: inline $`x`$, display fenced ```math.
• Diagrams are PlantUML (with LaTeX labels) for concepts; matplotlib SVG only for empirical data plots.
• Every claim is sourced: code claims cite file.rs; formal claims cite a theorem name; performance claims cite measured data.