论文标题
顺序数字电路的完整理论：表示，操作和代数语义
A Complete Theory of Sequential Digital Circuits: Denotational, Operational and Algebraic Semantics
论文作者
论文摘要
数字电路尽管已经进行了将近一个世纪的研究，并且在那个时间进行了大约一半的时间使用，但直到最近才逃避了一个完全的构图理论，在该理论中，任意电路可以自由地组合在一起而无需咨询其内部。最近的工作通过表明如何在自由产生的对称跟踪类别中以形态形式出现数字电路来纠正这一理论上的缺点。但是，这是非正式的。在本文中，我们以多种方式完善和扩展了先前的工作，最终是在三种声音和数字电路的完整语义的介绍中：eNotational，Operational和代数。对于表示的语义，我们在句法构建的某些属性和电路之间建立了对应关系。对于操作语义，我们介绍了建模电路如何处理值所需的减少，包括增加了新的减少以消除非延迟保护反馈的反馈；这导致了足够的数字电路观测等效概念。最后，我们定义了一个新的方程家族，用于将电路转换为“正常形式”的生物型电路，从而导致完整的代数语义用于顺序电路。
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.
