关系名义和高阶抽象规范
Relating Nominal and Higher-order Abstract Syntax Specifications
摘要：
名义抽象语法和高阶抽象语法提供了比传统技术更高层次的描述绑定结构的手段。这些方法产生了两个不同的社区，它们沿着类似的路线发展，但有微妙的差异，使它们难以联系起来。名义抽象语法社区有名称、新鲜度、带有变量捕获的名称抽象和新量词等设备，而高阶抽象语法社区则有类似于nabda-binders、nabda-conversion、raising和nabla-quantifier的设备。本文旨在统一这些社区，并提供了一个具体的对应关系，他们不同的设备。特别是，我们开发了一个语义保持的翻译从阿尔法Prolog，名义上的抽象语法为基础的逻辑程序设计语言，G-，高阶抽象语法为基础的逻辑程序设计语言。我们还讨论了高阶判断，这是一种用于具有高阶抽象语法的规范的常见且强大的工具，并且我们展示了如何将这些纳入G-中。这建立了G-作为一种具有高阶抽象语法的能力，名义规范的细粒度变量控制以及高阶判断的理想属性的语言。
英文摘要：
Nominal abstract syntax and higher-order abstract syntax provide a means for describing binding structure which is higher-level than traditional techniques. These approaches have spawned two different communities which have developed along similar lines but with subtle differences that make them difficult to relate. The nominal abstract syntax community has devices like names, freshness, name-abstractions with variable capture, and the new-quantifier, whereas the higher-order abstract syntax community has devices like lambda-binders, lambda-conversion, raising, and the nabla-quantifier. This paper aims to unify these communities and provide a concrete correspondence between their different devices. In particular, we develop a semantics-preserving translation from alpha-Prolog, a nominal abstract syntax based logic programming language, to G-, a higher-order abstract syntax based logic programming language. We also discuss higher-order judgments, a common and powerful tool for specifications with higher-order abstract syntax, and we show how these can be incorporated into G-. This establishes G- as a language with the power of higher-order abstract syntax, the fine-grained variable control of nominal specifications, and the desirable properties of higher-order judgments.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
