论文标题
稀疏的平铺穿过重叠关闭以终止字符串重写
Sparse Tiling through Overlap Closures for Termination of String Rewriting
论文作者
论文摘要
我们过分陈列在字符串中，按字符串重写，该语言由可接受因素定义的语言（称为瓷砖）。一组稀疏的瓷砖仅包含在派生中可以触及的瓷砖，并且是通过完成自动机构建的。使用由稀疏的瓷砖定义的部分代数进行语义标记，我们获得了一种证明局部终止的转换方法。由于已知的正向封闭结果以及重叠封闭的新表征，我们分别获得了证明终止和相对终止的方法。我们报告了显示这些方法强度的实验。
We over-approximate reachability sets in string rewriting by languages defined by admissible factors, called tiles. A sparse set of tiles contains only those that are reachable in derivations, and is constructed by completing an automaton. Using the partial algebra defined by a sparse tiling for semantic labelling, we obtain a transformational method for proving local termination. With a known result on forward closures, and a new characterisation of overlap closures, we obtain methods for proving termination and relative termination, respectively. We report on experiments showing the strength of these methods.
