通过变换与矩阵解释证明循环重写的终止性

我们提出了证明循环重写（即环上的字符串重写，环是首尾相连的字符串）终止性的技术。我们的主要技术是将循环重写变换为字符串重写，然后应用最先进的技术来证明该字符串重写系统的终止性。我们提出了三种这样的变换，并证明了它们都是可靠的且完备的。通过这种方式，不仅变换后系统的字符串重写终止性蕴含原始循环重写系统的终止性，对于非终止性也可以得出类似的结论。除了这种变换方法外，我们提出了一个统一的矩阵解释框架，涵盖了先前大多数自动证明循环重写终止性的方法。我们所有的技术均可用于证明终止性和相对终止性。我们给出了若干实验，展示了我们技术的威力。