Higher-Order Metalanguages for Implementing Derivation Systems

我们将研究适合于实现证明系统和程序转换系统等派生系统的元语言。这类语言的一个重要特征似乎是能够表示更高顺序的对象，并以逻辑上有意义的方式操纵它们。将研究一种提供这种能力的更高阶逻辑编程语言。这种语言提供了简单的类型化术语作为数据结构，用于表示程序和证明等对象，并结合了高阶统一和搜索原语来对这些对象进行推理。实验表明，这种语言作为一种元语言具有相当大的潜力，从而表明了对其进行健壮和高效实现的重要性。本研究将探讨在该语言中有效实现新运算的技术，即高阶合一和新的搜索原语，从而设计出一种抽象机。将根据这些结果提供一个实现，并将用于探索这种语言在实际派生系统中的应用。这些研究的反馈将用于改进对常见问题的实施行为。还将讨论基于使用更丰富的术语类别对语言的扩展。

Metalanguages that are suitable for implementing derivation systems such as proof systems and program transformation systems will be investigated. A crucial feature of such languages appears to be the ability to represent higher.order objects and to manipulate them in logically meaningful ways. A higher.order logic programming language that provides such a capability will be studied. This language provides simply typed \-terms as data structures for representing objects such as programs and proofs and incorporates higher-order unification and search primitives for reasoning about such objects. Experiments have shown that such a language has considerable potential as a metalanguage, thus pointing to the importance of a robust and efficient implementation for it. This research will examine techniques for efficiently implementing the novel operations in this language, i.e. higher-order unification and the new search primitives, resulting in the design of an abstract machine. An implementation will be provided based on these results and will be used to explore applications of this language within actual derivation systems. Feedback from these studies will be used to improve the behavior of the implementation on commonly occurring problems. Extensions to the language based on using a richer class of \-terms will also be addressed.