A Logic Programming Language Based on Binding Algebras
A Logic Programming Language Based on Binding Algebras
复制标题
基于绑定代数的逻辑编程语言
DOI：
10.1007/3-540-45500-0_12
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
M. Hamana
中科院分区：
文献类型：
--
作者：
M. Hamana
本文给出了一种基于Fiore、Plotkin和图里的结合代数的逻辑程序设计语言。在这种语言中，我们不仅可以使用一阶项，还可以使用涉及变量绑定的项。这种语言的目的类似于Nadathur和米勒的λ Prolog，它也可以通过在高阶逻辑中引入λ-项来处理绑定结构。但这里使用的绑定概念在某种意义上比通常的λ-绑定更精细。我们显式地管理用于绑定的名称，并处理与它们相关的α转换。还有一个重要的区别是与β转换相关的应用形式，即我们只允许形式（M x），其中x是（对象）变量，而不是通常的应用（M N）。这个绑定的概念来自于预层范畴的绑定语义。我们首先给出了反映这种范畴语义的类型理论。然后，我们沿着一阶逻辑程序设计语言的思路，即通过约束项的SLD-归结和统一算法，给出了该语言的一种逻辑、一种操作语义。
We give a logic programming language based on Fiore, Plotkin and Turi’s binding algebras. In this language, we can use not only first-order terms but also terms involving variable binding. The aim of this language is similar to Nadathur and Miller’s λProlog, which can also deal with binding structure by introducing λ-terms in higher-order logic. But the notion of binding used here is finer in a sense than the usual λ-binding. We explicitly manage names used for binding and treat α-conversion with respect to them.Also an important difference is the form of application related to β-conversion, i.e. we only allow the form (M x), where x is a (object) variable, instead of usual application (M N). This notion of binding comes from the semantics of binding by the category of presheaves. We firstly give a type theory which reflects this categorical semantics. Then we proceed along the line of first-order logic programming language, namely, we give a logic of this language, an operational semantics by SLD-resolution and unification algorithm for binding terms.