paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Coinductive Streams in Monoidal Categories

幺半范畴中的余归纳流
LMCS vol.Volume 21, Issue 32025匹配度 1/10 · 论文是纯范畴论与形式语义工作,研究幺半流与反馈范畴,与用户关注的 AI×PL、静态分析、浮点程序分析及贝叶斯程序分析均无直接关联,也不涉及 LLM/Agent 或工业落地。引用 4 inbox
Elena Di Lavore, Giovanni de Felice, Mario Román
crossref: 2026-09-10

AI 速览

一句话:将因果流函数推广至任意对称幺半范畴,提出幺半流与反馈范畴,为数据流编程提供余归纳范畴语义。

论文引入幺半流(monoidal streams),将通常在笛卡尔幺半范畴中定义的因果流函数推广到任意对称幺半范畴。正如流为纯函数数据流编程提供语义,幺半流为由对称幺半范畴表示的进程理论提供数据流编程语义。作者证明幺半流构成反馈幺半范畴,并用余归纳串图(coinductive string diagrams)对其进行推理,类似余归纳流演算用于信号流图。作为实例,论文研究一种随机数据流语言的语法,并在随机幺半流中给出其语义。

问题
如何将笛卡尔幺半范畴上的因果流函数语义推广到任意对称幺半范畴,并为由进程理论表示的数据流编程与反馈提供统一范畴语义。
方法
定义幺半流及反馈幺半范畴结构,构造余归纳串图作为推理工具,并以随机数据流语言的语法与随机幺半流语义为案例分析。
评估
评估为理论构造与案例分析:证明幺半流形成反馈幺半范畴,并展示随机数据流语言可在该语义框架中解释。
原文摘要(Abstract)

We introduce monoidal streams. Monoidal streams are a generalization of causal stream functions, which can be defined in cartesian monoidal categories, to arbitrary symmetric monoidal categories. In the same way that streams provide semantics to dataflow programming with pure functions, monoidal streams provide semantics to dataflow programming with theories of processes represented by a symmetric monoidal category. Monoidal streams also form a feedback monoidal category. In the same way that we can use a coinductive stream calculus to reason about signal flow graphs, we can use coinductive string diagrams to reason about feedback monoidal categories. As an example, we study syntax for a stochastic dataflow language, with semantics in stochastic monoidal streams.arXiv admin note: substantial text overlap with arXiv:2202.02061

链接与引用

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

BibTeX
@article{LavoreFR25,
  title = {Coinductive Streams in Monoidal Categories},
  author = {Elena Di Lavore and Giovanni de Felice and Mario Román},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 21, Issue 3},
  year = {2025},
  doi = {10.46298/lmcs-21(3:18)2025}
}