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 understanding, 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
翻译:数字电路尽管已被研究了近一个世纪,并在约半个世纪前开始大规模应用,但直到最近才被赋予完全组合性的理论基础——即任意电路无需查看其内部结构即可自由组合。近期研究通过展示数字电路如何作为自由生成的对称迹范畴中的态射进行组合呈现,弥补了这一理论缺陷。然而,该研究仍属非正式阐述;本文从多个方面对先前工作进行提炼和拓展,最终为数字电路提出三种可靠且完备的语义:指称语义、操作语义与代数语义。针对指称语义,我们建立了具有特定性质的流函数与语法构造电路之间的对应关系。针对操作语义,我们提出了模拟电路处理值所需的重写规则,包括新增一种消除非延迟保护反馈的规约;这为数字电路提供了恰当的可观察等价性概念。最后,我们定义了将电路转换为双模拟"范式"电路的新方程组,从而为时序电路建立了完备的代数语义。