Semantics Club 16 02 2001

A logic programming language based on binding algebra

Makoto Hamana

(joint work with Gordon Plotkin)


We give a logic programming language based on Fiore, Plotkin and Turi's binding algebra presented in LICS'99. In this language, we can use not only first-order terms but terms having variable binding. The aim of this language is similar to Miller's \lambda-Prolog, which can also deal with binding structure by introducing \lambda-terms in higher-order logic. But the notion of binding used here is finer in a sense than the usual \lambda-binding. For instance, we explicitly manage names used for binding and treat \alpha-conversion with respect to them. Also an important difference is the form of application related to \beta-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 actually comes from the semantics of binding by 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.

We will also give comparisons with related work similar to our aim: Miller's logic programming language L_\lambda, Pitts and Gabbay's functional language FreshML and Nipkow et al.'s higher-order rewrite systems.

Notes on this work is here. Any comments are very welcome.