An Effective Framework for Implementing Derivation Systems

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

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.***