余代数行为度量
摘要：在一个共代数的设置中，我们研究了不同的行为度量，比如通过分支和线性时间语义产生的度量。给定一个函子 $H \colon \mathrm{Set} \to \mathrm{Set}$ 下的共代数 $\alpha \colon X \to HX$，我们定义了一个在 $X$ 上的伪度量的框架，用于衡量状态之间的行为距离。一个关键的步骤是将 $H$ 在 $\mathrm{Set}$ 上的提升为在伪度量空间范畴 $\mathrm{PMet}$ 上的函子 $\overline{H}$。我们提出了两种不同的方法，可以看作是概率度量的 Kantorovich 和 Wasserstein 伪度量的推广。我们证明了这两种方法在几个自然的示例上得到的伪度量是相同的，但一般情况下它们是不同的。如果 $H$ 有一个最终共代数，那么每一个提升 $\overline{H}$ 都以一种规范的方式产生了一个行为距离，通常是分支时间的，也就是广义的相似性。为了建模线性时间的度量（广义的迹等价关系），我们展示了提升分配律和单子论的充分条件。这些结果使我们能够使用广义幂集构造。
作者：Paolo Baldan, Filippo Bonchi, Henning Kerstan, Barbara K"onig
论文ID：1712.07511
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22