效果与改写的婚姻
摘要：计算效应的研究中，通过代数定义的效应符号通常要满足一些方程。如果我们定向这些方程，就得到了一个重写系统，这可能是转换或优化程序中效应的有效方法。为了做到这一点，我们需要建立重写系统的强归纳性或终止性。在这里，我们定义了一个框架来进行这样的证明，并扩展了Dershowitz的递归路径序来证明一些效应系统的终止性。
作者：Ezra e. k. Cooper
论文ID：2302.02462
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-02-07