Termination of Rewrite Systems

重写系统是用于从左到右将相等替换为相等的一组等式。它们在编程语言中有重要的应用，因为它们代表了一种简单而直观的函数式语言，并且在自动演绎中，它们在提高公式推理的效率方面发挥了重要作用。系统的终止意味着方程不能被无限频繁地使用，除非得到一个不包含左手边实例的项。要证明终止合同可能很困难。(当然，总的来说，这是无法决定的。)在过去的支持下，设计了一些证明终止的方法，事实证明这些方法是有用的。现在正在研究这个主题的新方面，重点是结构化(分层)系统的语义方法和重写的扩展，以处理条件等式、联想-交换函数、高阶重写和逻辑编程风格。由于建立终止性是许多自动演绎和程序验证系统的重要组成部分，该项目还将投资于实现工作。

Rewrite systems are sets of equations used to substitute equals for equals from left-to-right only. They have important applications to programming languages, since they represent a simple and intuitive functional language, and in automated deduction, where they play an important role in improving the efficiency of reasoning about equations. Termination of a system means that the equations cannot be used infinitely often, without reaching a term that does not contain an instance of a left-handed side. Proving termination can be difficult. (It is, of course, undecidable in general.) Under past support, a number of methods for proving termination were devised which have proved useful. New aspects of this subject are now being investigated with an emphasis on semantic methods for structured (hierarchical) systems and extensions of rewriting to handle conditional equalities, associative- commutative functions, higher-order rewriting, and a logic programming style. Since establishing termination is an essential component of many automated deduction and program verification systems, this project will also invest effort in implementations.