课题基金 / 基金详情

Termination of Rewrite Systems

Termination of Rewrite Systems
重写系统的终止
批准号:
9700070
负责人:
Samuel Kamin
金额:
$15.0万
依托单位国家:
美国
项目类别:
Standard Grant
财政年份:
1997
资助国家:
美国
项目状态:
已结题
起止时间:
1997-06-01 至 2000-05-31

项目摘要

项目成果

Samuel Kamin的其他基金

相似基金

相关文献

中文摘要
翻译
重写系统是一组方程式,用于从左到右替换等号。它们在编程语言中有重要的应用,因为它们代表了一种简单直观的函数式语言,在自动演绎中,它们在提高方程推理的效率方面起着重要的作用。系统的终止意味着方程不能无限频繁地使用,除非达到一个不包含左手边实例的项。证明终止可能很困难。(当然,一般来说,这是无法确定的。)在过去的支持下,设计了一些证明终止的方法,这些方法已被证明是有用的。这一主题的新方面目前正在研究,重点是结构化(分层)系统的语义方法,以及处理条件等式、关联交换函数、高阶重写和逻辑编程风格的重写扩展。由于建立终止是许多自动推导和程序验证系统的基本组成部分,因此该项目还将在实现上投入精力。
英文摘要
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.
期刊论文(0)
专著(0)
科研奖励(0)
会议论文
Collaborative Research: BPC-A: Improving Metropolitan Participation to Accelerate Computing Throughput and Success
Collaborative Research: ITWF: Building Communities: Recruiting and Retention of Underrepresented Groups in Computer Science
Run-time Code Generation for the Masses
Technologies for Lightweight, Generative, Binary Software Components
海外基金