paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Rewriting with Frobenius

用 Frobenius 重写
LICS Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science2018匹配度 1/10 · 论文研究对称幺半范畴中的 string diagram 与 DPO 超图重写，属于形式语义和证明工程；与用户关注的静态分析、LLM/Agent、浮点程序分析及贝叶斯程序分析均无直接关联。引用 5 inbox
Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, Fabio Zanasi
形式语义定理证明与证明工程
crossref: 2026-09-12

AI 速览

一句话：在对称幺半范畴的 string diagram 推理中，结合 Frobenius 与 DPO 超图重写，吸收结构定律并仅显式保留领域方程。

对称幺半范畴已成为以 string diagram 图形语法对复合系统进行组合式、资源敏感分析的形式环境。近期，string diagram 推理通过双推（DPO）超图重写得到具体实现：超图表示不仅便于机械化，还能完全吸收对称幺半范畴的结构定律，使重写系统中只需显式给出领域特定方程。本文标题为“用 Frobenius 重写”，在上述背景下关注将 Frobenius 结构用于这类重写推理，以在保留 DPO 超图重写机械化优势的同时处理更丰富的代数结构。摘要未提供实验评估或具体定理细节，贡献定位在范畴语义与重写系统的表示层面。

问题
如何为对称幺半范畴中的 string diagram 推理提供具体、可机械化的重写机制，并处理 Frobenius 等代数结构。
方法
在 DPO 超图重写的基础上，利用超图表示吸收对称幺半范畴的结构定律，仅将领域特定方程显式化，并结合 Frobenius 结构进行重写。
评估
摘要未报告实验或案例评估；论证主要基于超图表示对机械化与结构定律吸收的便利性。
原文摘要（Abstract）

Symmetric monoidal categories have become ubiquitous as a formal environment for the analysis of compound systems in a compositional, resource-sensitive manner using the graphical syntax of string diagrams. Recently, reasoning with string diagrams has been implemented concretely via double-pushout (DPO) hypergraph rewriting. The hypergraph representation has the twin advantages of being convenient for mechanisation and of completely absorbing the structural laws of symmetric monoidal categories, leaving just the domain-specific equations explicit in the rewriting system.

链接与引用

DOI 原文 ·

BibTeX 
@inproceedings{paperbot4320,
  title = {Rewriting with Frobenius},
  author = {Filippo Bonchi and Fabio Gadducci and Aleks Kissinger and Pawel Sobocinski and Fabio Zanasi},
  booktitle = {LICS},
  year = {2018},
  doi = {10.1145/3209108.3209137}
}