带禁止模式的重写终止性分析与自动综合
计算机科学中的逻辑
2010-12-30 v1
摘要
我们引入了一种著名的依赖对框架的修改版本，适用于在禁止模式限制下的重写终止性分析。通过将表示相应递归函数调用上下文的上下文附加到依赖对上，可以将禁止模式限制纳入（适配后的）依赖对链概念中，从而产生一种可靠且完备的终止性分析方法。在此上下文依赖对框架的基础上，我们引入了一个依赖对处理器，通过分析依赖对的上下文信息来简化问题。此外，我们展示了如何在终止性分析过程中，利用该处理器动态综合出适用于给定项重写系统的禁止模式。
引用
@article{arxiv.1012.5562,
title = {Termination of Rewriting with and Automated Synthesis of Forbidden Patterns},
author = {Bernhard Gramlich and Felix Schernhammer},
journal= {arXiv preprint arXiv:1012.5562},
year = {2010}
}
备注
In Proceedings IWS 2010, arXiv:1012.5337