Match-Bounded String Rewriting Systems
Match-Bounded String Rewriting Systems
复制标题
匹配限制字符串重写系统
DOI：
--
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
Johannes Waldmann
中科院分区：
文献类型：
--
作者：
Alfons Geser;D. Hofbauer;Johannes Waldmann
摘要：我们引入了一类新的自动证明方法，用于终止字符串重写系统。所有这些方法的基础是表明重写保留了常规语言。为此，字母用自然数进行注释，称为匹配高度。如果 redex 中所有位置的最小高度为 h，则归约中的每个位置都将获得高度 h+1。在匹配限制系统中，匹配高度是全局限制的。使用删除系统的最新结果，我们证明通过匹配边界系统重写可以保留常规语言。因此，可以确定给定的重写系统是否具有给定的匹配界限。我们还提供了是否存在匹配限制的标准。匹配边界是否可判定仍然悬而未决。所有字符串的匹配界限都可以用作终止的自动标准，因为匹配界限系统正在终止。可以通过仅要求一组受限字符串（即前向闭包的右侧集合）的匹配有界性来加强该标准。
Abstract.We introduce a new class of automated proof methods for the termination of rewriting systems on strings. The basis of all these methods is to show that rewriting preserves regular languages. To this end, letters are annotated with natural numbers, called match heights. If the minimal height of all positions in a redex is h then every position in the reduct will get height h+1. In a match-bounded system, match heights are globally bounded. Using recent results on deleting systems, we prove that rewriting by a match-bounded system preserves regular languages. Hence it is decidable whether a given rewriting system has a given match bound. We also provide a criterion for the absence of a match-bound. It is still open whether match-boundedness is decidable. Match-boundedness for all strings can be used as an automated criterion for termination, for match-bounded systems are terminating. This criterion can be strengthened by requiring match-boundedness only for a restricted set of strings, namely the set of right hand sides of forward closures.