一句话：提出三种可靠完备变换及统一矩阵解释框架，证明循环重写及其相对终止性。
论文研究循环重写系统的终止性证明，即在首尾相连的字符串（环）上进行重写。作者提出三类将循环重写转换为普通字符串重写的变换，并证明这些变换是可靠且完备的：变换后字符串重写系统的终止性（以及非终止性）可对应原循环重写系统。此外，论文给出统一的矩阵解释框架，覆盖此前大多数自动证明循环重写终止性的方法。所有技术同时适用于终止性与相对终止性，并通过实验验证其效力。
We present techniques to prove termination of cycle rewriting, that is, string rewriting on cycles, which are strings in which the start and end are connected. Our main technique is to transform cycle rewriting into string rewriting and then apply state of the art techniques to prove termination of the string rewrite system. We present three such transformations, and prove for all of them that they are sound and complete. In this way not only termination of string rewriting of the transformed system implies termination of the original cycle rewrite system, a similar conclusion can be drawn for non-termination. Apart from this transformational approach, we present a uniform framework of matrix interpretations, covering most of the earlier approaches to automatically proving termination of cycle rewriting. All our techniques serve both for proving termination and relative termination. We present several experiments showing the power of our techniques.Comment: 38 pages, 1 figure
@article{paperbot202,
title = {Termination of Cycle Rewriting by Transformation and Matrix Interpretation},
author = {David Sabel and Hans Zantema},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 1},
year = {2017},
doi = {10.23638/lmcs-13(1:11)2017}
}