Semantics Club 16 02 2001
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.