Towards Practical Higher-Order Metalanguages

将对高阶元语言的实现和使用进行调查，该语言在原型派生系统中有几个应用。这种元语言基于逻辑编程范例，但它通过结合多态类型化方案、提供Lambda演算的术语作为数据结构、使用高阶统一来探测这些数据结构以及包括用于实现假设推理和用于在搜索期间创建新常量的两个新的搜索原语来丰富传统的此类语言。研究了这些特性带来的实现问题，并为底层逻辑语言设计了一个初步的抽象机。现在将致力于基于这些想法的方案编制系统的实际实现。将考虑语言和界面设计方面的问题，以加强基于逻辑语言的元语言的可用性。将对抽象机器进行扩展，以涵盖其他语文功能，并将实施整个系统。将使用该实现进行实验，以获得关于抽象机器的具体设计决策的反馈。将尝试根据正在变得独立感兴趣的子语言来调整实施。还将审查影响执行的质量和正确性的理论问题。特别感兴趣的将是研究lambda项的符号及其与归约中的最佳性的相关性。

Investigations will be conducted on the implementation and use of a higher-order metalanguage that has several applications in prototyping derivation systems. This metalanguage is based on the logic programming paradigm but it enriches conventional such languages by incorporating a polymorphic typing regimen, providing the terms of a lambda calculus as data structures, using higher- order unification for probing these data structures and including two new search primitives for realizing hypothetical reasoning and for creating new constants during search. The implementation problems that are raised by each of these features have been studied and a preliminary abstract machine has been designed for the underlying logical language. Efforts will now be devoted to a practical realization of a programming system based on these ideas. Language and interface design aspects will be considered to enhance the usability of the metalanguage based on the logical language. The abstract machine will be extended to cover the additional language features and an implementation of the overall system will be undertaken. Experiments will be conducted with the implementation to obtain feedback on specific design decisions pertaining to the abstract machine. Attempts will be made to tailor the implementation to sublanguages that are becoming of independent interest. Theoretical issues affecting the quality and correctness of the implementation will also be examined. A particular interest will be the study of notations for lambda terms and their relevance to optimality in reduction.