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