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.