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