单次控制运算符与协程的表达力

控制运算符，如异常和效果处理器，提供了以抽象和模块化方式表示程序中计算效果的手段。虽然大多数理论研究聚焦于多次控制运算符，但单次控制运算符——即限制所捕获的继续处理最多使用一次的控制运算符——因其在表达力和效率之间的平衡而日益受到关注。本研究旨在填补这一空白。我们提出了对单次控制运算符（包括效果处理器、受限继续以及甚至非对称协程）之间表达力进行数学严谨比较的做法。遵循前期关于多次控制运算符的研究，我们采用费莱森的宏表达力作为衡量标准。我们验证了单次效果处理器和单次受限控制运算符可被非对称协程宏表达式，但反之不行。我们解释了为何之前的非正式论证失败，以及如何修订其以实现有效的宏翻译。