paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Rewriting Modulo Traced Comonoid Structure

模 traced comonoid 结构的重写
LMCS vol.Volume 22, Issue 12026匹配度 2/10 · 该论文属于纯范畴论/形式语义方向,研究 traced comonoid 结构下的弦图超图重写与 DPO 适配,与用户关注的 PL 与 AI/LLM 交叉、静态分析、浮点程序分析、贝叶斯程序分析均无直接关联。虽然涉及形式化验证的理论基础,但没有 LLM/Agent 应用或工业落地场景。引用 6 inbox
Dan R. Ghica, George Kaye
crossref: 2026-09-10

AI 速览

一句话:将弦图超图重写推广到 traced comonoid 范畴,建立完全性并适配 DPO 重写,附顺序电路案例。

论文把先前基于超图重写弦图的工作推广到基础范畴具有 traced comonoid 结构的情形:连线可分叉,态射输出可连回输入;任何 traced Cartesian(数据流)范畴都有此底层结构。作者证明某些超图子类对 traced comonoid 范畴完全完备:每个项在同构意义下唯一对应一个超图,每个满足条件的超图也可在公理意义下还原出唯一项。文章还刻画该设定下有效的 pushout complement,使双推重写(DPO)适配该结构。最后以带延迟和反馈的逻辑门构成的顺序电路等式理论为案例,说明图重写可为顺序电路定义操作语义。

问题
如何为具有 traced comonoid 结构(连线可分叉、输出可反馈至输入)的范畴建立弦图的超图重写与完全性理论。
方法
将超图表示推广到该结构,证明特定超图子类与范畴项在公理意义下一一对应,并刻画 DPO 重写的有效 pushout complement。
评估
以完全性等定理证明进行理论验证,并通过顺序电路等式理论与操作语义案例研究展示框架。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · arXiv · PDF(开放获取) · DBLP

BibTeX
@article{GhicaK23,
  title = {Rewriting Modulo Traced Comonoid Structure},
  author = {Dan R. Ghica and George Kaye},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 22, Issue 1},
  year = {2026},
  doi = {10.46298/lmcs-22(1:2)2026}
}