A Detector Error Model (DEM) is a structured representation of error mechanisms in quantum circuits, which has gained popularity in quantum compilation pipelines for its ability to capture fault-tolerance at a circuit level. It lists error mechanisms as instructions targeting detectors and observables, specifying for each physical fault channel the probability that the fault fires, the detectors it triggers, and the observables it flips. In this paper, we develop an equational theory for DEMs, with its associated categorical semantics. We present a sound, terminating, confluent rewriting system for DEM terms, formulating it as a symmetric monoidal theory (a PROP) over the Giry monad. We prove that every DEM term has a unique normal form, which can be computed efficiently in quasilinear time $O(k|E|\log|E|)$, where $|E|$ is the number of instructions and $k$ bounds the size of a target set. This provides a complete set of invariants (via Tanner graphs) for structural DEM equivalence. We provide the first static decision procedure for DEM equivalence, with rigorous correctness guarantees. It is complete (decides full decoder-equivalence exactly) for non-adaptive quantum error correction (QEC) pipelines, and scales to a sound and applicable decision procedure for partially-adaptive circuits (lattice surgery, distributed QEC, ...) without suffering exponential overhead. We discuss its application to the verification and optimisation of quantum compilers.

翻译：探测器误差模型（DEM）是量子电路中错误机制的一种结构化表示，因其能够在电路层面捕获容错性而在量子编译流水线中广受欢迎。该模型将错误机制列为针对探测器和可观测量指令，具体说明每个物理故障通道的触发概率、所触发的探测器以及所翻转的可观测量。本文为DEM建立了一个带范畴语义的等式理论。我们提出一个基于Giry单子、以对称幺半群理论（PROP）形式表述的、可判定、可终止、可合流的DEM项重写系统。我们证明每个DEM项都有唯一范式，可在准线性时间$O(k|E|\log|E|)$内高效计算，其中$|E|$是指令数量，$k$为目标集大小上界。这通过Tanner图为结构DEM等价性提供了完整的恒等不变量集合。我们给出了首个具有严格正确性保证的DEM等价性静态判定过程：该过程对非自适应量子纠错（QEC）流水线是完备的（可精确判定完整解码器等价性），并可扩展到部分自适应电路（晶格手术、分布式QEC等）的可靠实用判定过程，且无需承受指数级开销。我们讨论了该方法在量子编译器验证与优化中的应用。