Termination of Rewrite Systems

重写系统的终止

• 批准号: 9700070
• 负责人: Samuel Kamin
• 金额: $ 15万
• 依托单位: University of Illinois at Urbana-Champaign
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1997
• 资助国家: 美国
• 起止时间: 1997-06-01 至 2000-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9700070&HistoricalAwards=false
• 关键词: Termination; 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.

重写系统是一组等式，用于从左到右替换相等。 它们在编程语言中有重要的应用，因为它们代表了一种简单而直观的函数式语言，在自动演绎中，它们在提高方程推理效率方面发挥着重要作用。 系统的终止性意味着方程不能无限频繁地使用，除非达到一个不包含左手边实例的项。 证明终止可能很困难。 (It当然，一般情况下是不可判定的。） 在过去的支持下，设计了一些证明终止的方法，这些方法证明是有用的。 这个问题的新方面，现在正在调查的重点是语义方法的结构化（层次）系统和扩展重写处理条件等式，关联交换功能，高阶重写，和逻辑编程风格。 由于建立终止是许多自动演绎和程序验证系统的重要组成部分，因此本项目也将在实现方面投入精力。