A Logic Programming Language Based on Binding Algebras

  • Makoto Hamana
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2215)


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.

Unable to display preview. Download preview PDF.


  1. [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
  2. [DFH95]
    J. Despeyroux, A. Felty, and A. Hirschowitz. Higher-order abstract syntax in Coq. In M. Dezani and G. Plotkin, editors, Typed Lambda Clculi and Apllications, LNCS 902, pages 124–138, 1995.CrossRefGoogle Scholar
  3. [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
  4. [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
  5. [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
  6. [Mil91]
    D. Miller. A logic programming language with lambda-abstraction, function variables, and simple unification,. Journal of Logic and Computation, 1(4):497–536, 1991.zbMATHCrossRefMathSciNetGoogle Scholar
  7. [Mil00]
    D. Miller. Abstract syntax for variable binders: An overview.In John Lloyd,, editor, Proceedings of Computation Logic 2000, LNAI 1861, 2000.Google Scholar
  8. [MM82]
    A. Martelli and U. Montanari. An efficient unification algorithm. ACM Transactions of Programming Languages, 4(2):258–282, 1982.zbMATHCrossRefGoogle Scholar
  9. [NM88]
    G. Nadathur and D. Miller. An overview of λProlog.In Fifth International Logic Programming Conference, pages 810–827.MIT Press, 1988.Google Scholar
  10. [Oho96]
    A. Ohori. A typed context calculus.In Preprint RIMS-1098.Research Institute for Mathematical Sciences, Kyoto University, 1996.Google Scholar
  11. [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
  12. [SSK01]
    M. Sato, T. Sakurai, and Y. Kameyama. A simply typed context calculu with first-class environments.In 5th International Symposium on Functional and Logic Programming, volume LNCS 2024, pages 359–374, 2001.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Makoto Hamana

There are no affiliations available

Personalised recommendations