基于模态的代数效应行为等价

本文研究在扩展了（代数）效应触发操作签名的值调用函数式语言中程序间的行为等价。若两个程序享有相同的行为性质，则被视为行为等价。为此，我们定义了一种以公式指称行为性质的逻辑。一个关键要素是表达行为中效应特定方面的模态集合。我们给出此类模态的一般理论。若模态满足开放性与可分解性两个条件，则逻辑所指定的行为等价与由模态定义的适用互模拟（applicative bisimilarity）概念一致，且可通过 Howe 方法的推广证明其为一同余。我们展示了开放性与可分解性条件对若干代数效应实例成立：非确定性、概率选择、全局存储与输入/输出。