一句话：为时序数字电路建立指称、操作与代数三种可靠且完备的语义，并给出观察等价与范式代数理论。
数字电路虽被研究近一个世纪并大规模使用，却长期缺乏完全组合式的理论，使任意电路可自由组合而无需查看内部；近期工作将其表述为自由生成的对称迹范畴中的态射，但仍是非形式化的。本文精炼并扩展该工作，给出时序数字电路的指称、操作与代数三种可靠且完备的语义。指称语义建立具有特定性质的流函数与语法构造电路之间的对应；操作语义给出电路处理值所需的归约，并新增消除非延迟保护反馈的归约，从而得到适当的观察等价；代数语义定义一族方程，将电路翻译为双相似的范式电路，形成完备代数理论。
Digital circuits, despite having been studied for nearly a century and used at scale for about half that time, have until recently evaded a fully compositional theoretical in which arbitrary circuits may be freely composed together without consulting their internals. Recent work remedied this theoretical shortcoming by showing how digital circuits can be presented compositionally as morphisms in a freely generated symmetric traced category. However, this was done informally; in this paper we refine and expand the previous work in several ways, culminating in the presentation of three sound and complete semantics for digital circuits: denotational, operational and algebraic. For the denotational semantics, we establish a correspondence between stream functions with certain properties and circuits constructed syntactically. For the operational semantics, we present the reductions required to model how a circuit processes a value, including the addition of a new reduction for eliminating non-delay-guarded feedback; this leads to an adequate notion of observational equivalence for digital circuits. Finally, we define a new family of equations for translating circuits into bisimilar circuits of a 'normal form', leading to a complete algebraic semantics for sequential circuits.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{GhicaKS26,
title = {A Complete Theory of Sequential Digital Circuits: Denotational, Operational and Algebraic Semantics},
author = {Dan R. Ghica and George Kaye and David Sprunger},
journal = {Logical Methods in Computer Science},
volume = {Volume 22, Issue 2},
year = {2026},
doi = {10.46298/lmcs-22(2:34)2026}
}