论文标题
从方程式到区分：有效计算的两个解释
From Equations to Distinctions: Two Interpretations of Effectful Computations
论文作者
论文摘要
有几种方法可以为具有代数效应的功能程序定义程序等效性。我们考虑两种补充方法来指定行为等效性。一种方法是指定一组公理方程，并允许证明方法表明两个程序是等效的。另一种方法是指定Eilenberg-Moore代数，该代数生成可以区分程序的测试。据说这两种方法可以相互补充，如果可以证明任何两个程序是等效的，并且仅当没有测试以区分它们时。 在本文中，我们研究了一种通用方法，可以从一组公理方程中制定一个eilenberg-moore代数，该代数对其进行了补充。我们将查看必须满足的其他条件。然后，我们将此方法应用于少数效果示例，包括概率和全球商店，并表明它们与文献的通常代数相吻合。我们还将研究是否有可能指定一组一组一组布尔方式，这些模态可以用作区别的测试，以补充方程理论。
There are several ways to define program equivalence for functional programs with algebraic effects. We consider two complementing ways to specify behavioural equivalence. One way is to specify a set of axiomatic equations, and allow proof methods to show that two programs are equivalent. Another way is to specify an Eilenberg-Moore algebra, which generate tests that could distinguish programs. These two methods are said to complement each other if any two programs can be shown to be equivalent if and only if there is no test to distinguish them. In this paper, we study a generic method to formulate from a set of axiomatic equations an Eilenberg-Moore algebra which complements it. We will look at an additional condition which must be satisfied for this to work. We then apply this method to a handful of examples of effects, including probability and global store, and show they coincide with the usual algebras from the literature. We will moreover study whether or not it is possible to specify a set of unary Boolean modalities which could function as distinction-tests complementing the equational theory.
