An Effective Framework for Implementing Derivation Systems

实施推导系统的有效框架

• 批准号: 9803971
• 负责人: Dale Miller
• 金额: $ 7万
• 依托单位: Pennsylvania State Univ University Park
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1998
• 资助国家: 美国
• 起止时间: 1998-07-15 至 2001-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9803971&HistoricalAwards=false
• 关键词: Effective; Framework; Implementing; Derivation; Systems

9803971 Many reasoning and specification tasks require the analysis of logically complex syntactic objects. Such tasks arise, for instance, in using typing systems, in describing and prototyping programming languages, in effecting program transformations, in demonstrating program correctness, in realizing theorem provers, in describing the semantics of natural languages and in constructing corresponding parsers for them. A satisfactory framework for performing such tasks is obtained from using lambda- terms to represent the objects that are of interest and a constructive logic to describe their properties. This research addresses questions of implementation and use of lambda Prolog, a programming language that provides such a framework. The starting point for this work is an implementation of lambda Prolog that embodies the first serious attempt to realize many of its new features in an efficient manner. Using this system, the project conducts an extensive empirical study of the impact on efficiency of choices in the representation of lambda terms and in the compilation of unification and other operations on these terms. Refinements to the structure of lambda terms and to other language features are considered towards understanding the tradeoffs between efficiency and expressiveness. Issues relevant to constructing a flexible programming system around the language are studied. Finally, the strength of the programming system and of the methods supported by it are tested by employing them to implement a compiler for lambda Prolog.***

许多推理和规范任务需要分析逻辑上复杂的句法对象。例如，在使用类型系统、描述和原型化编程语言、实现程序转换、证明程序正确性、实现定理证明器、描述自然语言的语义以及为它们构造相应的解析器时，都会出现这样的任务。 一个令人满意的框架，执行这样的任务是从使用lambda-条款来表示感兴趣的对象和一个建设性的逻辑来描述它们的属性。这项研究解决了问题的实现和使用的lambda Prolog，编程语言，提供了这样一个框架。这项工作的起点是lambda Prolog的实现，它体现了以有效的方式实现其许多新功能的第一次认真尝试。使用这个系统，该项目进行了广泛的实证研究的影响，选择的效率表示的lambda条款，并在这些条款的统一和其他操作的编译。 对lambda术语的结构和其他语言特性的改进被认为是为了理解效率和表达能力之间的权衡。围绕语言构建灵活的编程系统的相关问题进行了研究。最后，编程系统和它所支持的方法的强度通过使用它们来实现Lambda Prolog的编译器来测试。