论 CSP 与效应的代数理论

我们从效应的代数理论角度考虑 CSP，该理论将操作分类为效应构造子或效应解构子；它还为函数式编程提供了联系，是对 Moggi 开创性的单子观点的精炼。存在一个自然的构造子代数理论，其自由代数函子是 Moggi 的单子；我们通过用两个版本的 CSP 稳定失败模型（一个比另一个更一般）来刻画自由代数和初始代数来说明这一点。解构子被处理为到（可能非自由）代数的同态。可以将 CSP 的动作和选择算子视为构造子，而其余算子（如隐藏和并发）视为解构子。执行这一方案的结果是将确定性外部选择作为构造子，而不是一般外部选择。然而，二元解构子（如 CSP 并发算子）带来了未解决的困难。最后，我们提出了 CSP 与 Moggi 的计算 λ 演算的结合，其中算子（包括并发）是多态的。虽然本文主要关注 CSP，但应该有可能将类似的思想推广到其他进程演算。