一句话:将弦图超图重写推广到 traced comonoid 范畴,建立完全性并适配 DPO 重写,附顺序电路案例。
论文把先前基于超图重写弦图的工作推广到基础范畴具有 traced comonoid 结构的情形:连线可分叉,态射输出可连回输入;任何 traced Cartesian(数据流)范畴都有此底层结构。作者证明某些超图子类对 traced comonoid 范畴完全完备:每个项在同构意义下唯一对应一个超图,每个满足条件的超图也可在公理意义下还原出唯一项。文章还刻画该设定下有效的 pushout complement,使双推重写(DPO)适配该结构。最后以带延迟和反馈的逻辑门构成的顺序电路等式理论为案例,说明图重写可为顺序电路定义操作语义。
In this paper we adapt previous work on rewriting string diagrams using hypergraphs to the case where the underlying category has a traced comonoid structure, in which wires can be forked and the outputs of a morphism can be connected to its input. Such a structure is particularly interesting because any traced Cartesian (dataflow) category has an underlying traced comonoid structure. We show that certain subclasses of hypergraphs are fully complete for traced comonoid categories: that is to say, every term in such a category has a unique corresponding hypergraph up to isomorphism, and from every hypergraph with the desired properties, a unique term in the category can be retrieved up to the axioms of traced comonoid categories. We also show how the framework of double pushout rewriting (DPO) can be adapted for traced comonoid categories by characterising the valid pushout complements for rewriting in our setting. We conclude by presenting a case study in the form of recent work on an equational theory for sequential circuits: circuits built from primitive logic gates with delay and feedback. The graph rewriting framework allows for the definition of an operational semantics for sequential circuits.