Completeness of Tree Automata Completion
Completeness of Tree Automata Completion
复制标题
树自动机完成的完整性
DOI：
10.4230/lipics.fscd.2018.16
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
T. Genet
中科院分区：
文献类型：
--
作者：
T. Genet
我们考虑用左线性项重写系统重写正则语言。我们证明了一个完备性定理方程树自动机完成说明，如果存在一个经常过近似的一组可达条款，然后方程完成可以计算它（或安全下近似）。这个定理的一个很好的推论是，如果可达项的集合是正则的，那么方程完备化也可以计算它。这对于某些保持正则性的项重写系统类是正确的，但在一般情况下仍然是一个悬而未决的问题。这个证明不是构造性的，因为它依赖于不可判定的可达项集合的正则性。为了实现这些证明，我们推广和改进了两个完备性结果：终止定理和上界定理。这些理论结果提供了一种安全地探索具有完备性的正则近似的算法方法。这已经在Timbuk实现，并用于自动有效地验证一阶和高阶函数程序的安全属性。
We consider rewriting of a regular language with a left-linear term rewriting system. We show a completeness theorem on equational tree automata completion stating that, if there exists a regular over-approximation of the set of reachable terms, then equational completion can compute it (or safely under-approximate it). A nice corollary of this theorem is that, if the set of reachable terms is regular, then equational completion can also compute it. This was known to be true for some term rewriting system classes preserving regularity, but was still an open question in the general case. The proof is not constructive because it depends on the regularity of the set of reachable terms, which is undecidable. To carry out those proofs we generalize and improve two results of completion: the Termination and the Upper-Bound theorems. Those theoretical results provide an algorithmic way to safely explore regular approximations with completion. This has been implemented in Timbuk and used to verify safety properties, automatically and efficiently, on first-order and higher-order functional programs.