Declarative Compilation for Constraint Logic Programming

  • Emilio Jesús Gallego Arias
  • James LiptonEmail author
  • Julio Mariño
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8981)


We present a new declarative compilation of logic programs with constraints into variable-free relational theories which are then executed by rewriting. This translation provides an algebraic formulation of the abstract syntax of logic programs. Management of logic variables, unification, and renaming apart is completely elided in favor of algebraic manipulation of variable-free relation expressions. We prove the translation is sound, and the rewriting system complete with respect to traditional SLD semantics.


Logic programming Constraint programming Relation algebra Rewriting Semantics 


  1. 1.
    Amato, G., Lipton, J., McGrail, R.: On the algebraic structure of declarative programming languages. Theor. Comput. Sci. 410(46), 4626–4671 (2009), (abstract Interpretation and Logic Programming: In honor of professor Giorgio Levi)
  2. 2.
    Asperti, A., Martini, S.: Projections instead of variables: a category theoretic interpretation of logic programs. In: ICLP, pp. 337–352 (1989)Google Scholar
  3. 3.
    Bellia, M., Occhiuto, M.E.: C-expressions: a variable-free calculus for equational logic programming. Theor. Comput. Sci. 107(2), 209–252 (1993)CrossRefzbMATHMathSciNetGoogle Scholar
  4. 4.
    Broome, P., Lipton, J.: Combinatory logic programming: computing in relation calculi. In: ILPS’94: Proceedings of the 1994 International Symposium on Logic programming, pp. 269–285. MIT Press, Cambridge (1994)Google Scholar
  5. 5.
    Cheney, J., Urban, C.: Alpha-prolog: a logic programming language with names, binding, and alpha-equivalence (2004)Google Scholar
  6. 6.
    Clark, K.L.: Negation as failure. In: Gallaire, H., Minker, J. (eds.) Logic and Data Bases, pp. 293–322. Plenum Press (1977)Google Scholar
  7. 7.
    Comini, M., Levi, G., Meo, M.C.: A theory of observables for logic programs. Inf. Comput. 169(1), 23–80 (2001)CrossRefzbMATHMathSciNetGoogle Scholar
  8. 8.
    Finkelstein, S.E., Freyd, P.J., Lipton, J.: A new framework for declarative programming. Theor. Comput. Sci. 300(1–3), 91–160 (2003)CrossRefMathSciNetGoogle Scholar
  9. 9.
    Freyd, P., Scedrov, A.: Categories, Allegories. North Holland Publishing Company, Amsterdam (1991)Google Scholar
  10. 10.
    Gallego Arias, E.J., Lipton, J., Mariño, J., Nogueira, P.: First-order unification using variable-free relational algebra. Log. J. IGPL 19(6), 790–820 (2011). CrossRefzbMATHMathSciNetGoogle Scholar
  11. 11.
    Gallego Arias, E.J., Lipton, J.: Logic programming in tabular allegories. In: Dovier, A., Costa, V.S. (eds.) Technical Communications of the 28th International Conference on Logic Programming, ICLP 2012, September 4–8, 2012, Budapest, Hungary. LIPIcs, vol. 17, pp. 334–347. Schloss Dagstuhl—Leibniz-Zentrum fuer Informatik (2012)Google Scholar
  12. 12.
    Jaffar, J., Maher, M.J.: Constraint logic programming: a survey. J. Log. Program. 19/20, 503–581 (1994). CrossRefMathSciNetGoogle Scholar
  13. 13.
    Kinoshita, Y., Power, A.J.: A fibrational semantics for logic programs. In: Dyckhoff, R., Herre, H., Schroeder-Heister, P. (eds.) ELP. LNCS, vol. 1050, pp. 177–191. Springer, Heidelberg (1996) CrossRefGoogle Scholar
  14. 14.
    Komendantskaya, E., Power, J.: Coalgebraic derivations in logic programming. In: Bezem, M. (ed.) CSL. LIPIcs, vol. 12, pp. 352–366. Schloss Dagstuhl—Leibniz-Zentrum fuer Informatik (2011)Google Scholar
  15. 15.
    Lipton, J., Chapman, E.: Some notes on logic programming with a relational machine. In: Jaoua, A., Kempf, P., Schmidt, G. (eds.) Using Relational Methods in Computer Science, pp. 1–34. Technical report Nr. 1998-03, Fakultät für Informatik, Universität der Bundeswehr München, July 1998Google Scholar
  16. 16.
    Lloyd, J.W.: Foundations of Logic Programming. Springer, New York (1984)CrossRefzbMATHGoogle Scholar
  17. 17.
    Miller, D., Nadathur, G., Pfenning, F., Scedrov, A.: Uniform proofs as a foundation for logic programming. Ann. Pure Appl. Log. 51(1–2), 125–157 (1991)CrossRefzbMATHMathSciNetGoogle Scholar
  18. 18.
    Pfenning, F., Elliot, C.: Higher-order abstract syntax. In: PLDI’88: Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation, pp. 199–208. ACM, New York (1988)Google Scholar
  19. 19.
    Rydeheard, D.E., Burstall, R.M.: A categorical unification algorithm. In: Proceedings of a Tutorial and Workshop on Category Theory and Computer Programming, pp. 493–505. Springer, New York (1986)Google Scholar
  20. 20.
    Sterling, L., Shapiro, E.: The Art of Prolog. The MIT Press, Cambridge (1986)zbMATHGoogle Scholar
  21. 21.
    Tarski, A., Givant, S.: A Formalization of Set Theory Without Variables, Colloquium Publications, vol. 41. American Mathematical Society, Providence (1987)Google Scholar
  22. 22.
    Urban, C., Pitts, A.M., Gabbay, M.J.: Nominal unification. Theor. Comput. Sci. 323(1–3), 473–497 (2004)CrossRefzbMATHMathSciNetGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  • Emilio Jesús Gallego Arias
    • 1
  • James Lipton
    • 2
    Email author
  • Julio Mariño
    • 3
  1. 1.University of PennsylvaniaPhiladelphiaUSA
  2. 2.Wesleyan UniversityMiddletownUSA
  3. 3.Universidad Politécnica de MadridMadridSpain

Personalised recommendations