A Logic Programming Language Based on Binding Algebras
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.
Unable to display preview. Download preview PDF.
- [dB72]N. de Bruijn. Lambda clculus notation with nameless dummies, a tool for automatic formula manipulation, whith application to the church-rosser theorem. Indagationes Mathematicae, 34:381–391, 1972.Google Scholar
- [FPT99]M. Fiore, G. Plotkin, and D. Turi. Abstrat syntax and variable binding. In 14th Annual Symposium on Logic in Computer Science, pages 193–202, Washington, 1999.IEEE Computer Society Press.Google Scholar
- [GP99]M.J. Gabba y and A.M. Pitts. A new approach to abstract syntax involving binders.In 14th Annual Symposium on Logic in Computer Science, pages 214–224, Washington, 1999.IEEE Computer Society Press.Google Scholar
- [Hof99]M. Hofmann.Seman tical analysis of higher-order abstract syntax.In 14th Annual Symposium on Logic in Computer Science, pages 204–213, Washington, 1999.IEEE Computer Society Press.Google Scholar
- [Mil00]D. Miller. Abstract syntax for variable binders: An overview.In John Lloyd, et.al., editor, Proceedings of Computation Logic 2000, LNAI 1861, 2000.Google Scholar
- [NM88]G. Nadathur and D. Miller. An overview of λProlog.In Fifth International Logic Programming Conference, pages 810–827.MIT Press, 1988.Google Scholar
- [Oho96]A. Ohori. A typed context calculus.In Preprint RIMS-1098.Research Institute for Mathematical Sciences, Kyoto University, 1996.Google Scholar
- [PG00]A.M. Pitts and M.J. Gabba y. A metalanguage for programming with bound names modulo renaming. In R. Backhouse and J.N. Oliveira, editors, Mathematics of Program Construction, MPC2000, Proceedings, Ponte de Lima, Portugal, July 2000, volume 1837 of Lecture Notes in Computer Science, pages 230–255.Springer-Verlag, Heidelberg, 2000.Google Scholar