This paper refines the existing axiomatic semantics of digital circuits with delay and feedback, in which circuits are constructed as morphisms in a freely generated cartesian traced (dataflow) category. First, we give a cleaner presentation, making a clearer distinction between syntax and semantics, including a full formalisation of the semantics as stream functions. As part of this effort, we refocus the categorical framework through the lens of string diagrams, which not only makes reading equations more intuitive but removes bureaucracy such as associativity from proofs. We also extend the existing framework with a new axiom, inspired by the Kleene fixed-point theorem, which allows circuits with non-delay-guarded feedback, typically handled poorly by traditional methodologies, to be replaced with a series of finitely iterated circuits. This eliminates the possibility of infinitely unfolding a circuit; instead, one can always reduce a circuit to some (possibly undefined) value. To fully characterise the stream functions that correspond to digital circuits, we examine how the behaviour of the latter can be modelled using Mealy machines. By establishing that the translation between sequential circuits and Mealy machines preserves their behaviour, one can observe that circuits always implement monotone stream functions with finite stream derivatives.
翻译:本文精细了数字电路现有的不言自明的语义,延缓和反馈,使电路在自由生成的卡通追踪(数据流)类别中作为形态构建。 首先,我们做了更清洁的演示,更清楚地区分语法和语义,包括将语义完全正规化作为流函数。作为这一努力的一部分,我们通过字符串图的透镜重新调整绝对框架,不仅使读取方程更直观,而且从证据中去除诸如连结性等官僚。我们还将现有的框架扩展为一个新的正态,由Kleene固定点理论所启发,允许以非脱节的反馈(通常由传统方法处理不善)的电路被替换为一系列有限迭代电路功能。这消除了无限展电路的可能性;相反,人们总是可以将电路路流降低到某些(可能无法定义的)价值。为了充分描述与数字电路相对应的流函数,我们检查如何使电流的电路流行为得以在使用连续的电路流中进行,我们检查如何以固定的电路流的机进行。