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.

翻译：数字电路尽管已研究近一个世纪并大规模应用约半个世纪，但直到近期才建立起完全组合化的理论框架，使得任意电路无需查阅内部结构即可自由组合。近期研究通过展示数字电路可组合地表示为自由生成对称迹范畴中的态射，弥补了这一理论缺陷。然而该工作仅以非形式化方式完成；本文通过多个方向对前期工作进行提炼与扩展，最终提出数字电路的三种可靠且完备的语义：指称语义、操作语义与代数语义。在指称语义方面，我们建立了具有特定性质的流函数与语法构造电路之间的对应关系。在操作语义方面，我们提出了电路处理值所需的重写规则，包括新增用于消除非延迟保护反馈的重写规则，从而获得数字电路观测等价的充分概念。最后，我们定义了一组新的方程，用于将电路转换为双模拟的"范式"电路，从而建立了时序电路的完备代数语义。