paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Stream processors and comodels

流处理器与余模型
LMCS vol.Volume 19, Issue 12023匹配度 1/10 · 论文属于纯范畴论/余代数形式语义,研究流处理器的内涵与外延等价,与画像关注的静态分析、LLM/Agent、浮点程序分析及贝叶斯程序分析均无直接关联。引用 0 inbox
Richard Garner
crossref: 2026-09-10

AI 速览

一句话:用代数效应的余模型统一刻画外延与内涵流处理器,并类比双模拟与迹等价。

该文关注流处理器 A^N→B^N 的余代数刻画。Hancock、Pattinson 与 Ghani 在 2009 年借助 Brouwer 构造主义思想给出了内涵式流处理器的 coalgebraic 刻画;本文则给出外延式流处理器,即连续函数 A^N→B^N 的对应余代数刻画。作者将本文结果与前述工作都置于 Power-Shkaravska 提出的代数效应余模型(comodels for algebraic effects)框架中。在这一框架下,流处理器的内涵等价与外延等价之别,正类似于带标签迁移系统及概率生成系统中双模拟与迹等价之别。

问题
如何为外延式流处理器(连续函数 A^N→B^N)给出与内涵式流处理器相对应的余代数刻画,并统一理解二者差异。
方法
在代数效应的余模型(comodels)框架中构建流处理器的余代数语义,并与 Hancock 等人的内涵式刻画进行对照。
评估
属于理论工作,通过范畴论/余代数构造与既有结果的形式对照来论证刻画的一致性与区分;摘要未报告实现或实证评估。
原文摘要(Abstract)

In 2009, Hancock, Pattinson and Ghani gave a coalgebraic characterisation of stream processors $A^\mathbb{N} \to B^\mathbb{N}$ drawing on ideas of Brouwerian constructivism. Their stream processors have an intensional character; in this paper, we give a corresponding coalgebraic characterisation of extensional stream processors, i.e., the set of continuous functions $A^\mathbb{N} \to B^\mathbb{N}$. Our account sites both our result and that of op. cit. within the apparatus of comodels for algebraic effects originating with Power-Shkaravska. Within this apparatus, the distinction between intensional and extensional equivalence for stream processors arises in the same way as the the distinction between bisimulation and trace equivalence for labelled transition systems and probabilistic generative systems.

链接与引用

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

BibTeX
@article{paperbot2248,
  title = {Stream processors and comodels},
  author = {Richard Garner},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 19, Issue 1},
  year = {2023},
  doi = {10.46298/lmcs-19(1:2)2023}
}