Logic Programming and Logarithmic Space

  • Clément Aubert
  • Marc Bagnol
  • Paolo Pistone
  • Thomas Seiller
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8858)


We present an algebraic view on logic programming, related to proof theory and more specifically linear logic and geometry of interaction. Within this construction, a characterization of logspace (deterministic and non-deterministic) computation is given via a syntactic restriction, using an encoding of words that derives from proof theory.

We show that the acceptance of a word by an observation (the counterpart of a program in the encoding) can be decided within logarithmic space, by reducing this problem to the acyclicity of a graph. We show moreover that observations are as expressive as two-ways multihead finite automata, a kind of pointer machine that is a standard model of logarithmic space computation.


Implicit Complexity Unification Logic Programming Logarithmic Space Proof Theory Pointer Machines Geometry of Interaction Automata 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Asperti, A., Danos, V., Laneve, C., Regnier, L.: Paths in the lambda-calculus. In: LICS, pp. 426–436. IEEE Computer Society (1994)Google Scholar
  2. 2.
    Aubert, C., Bagnol, M.: Unification and logarithmic space. In: Dowek, G. (ed.) RTA-TLCA 2014. LNCS, vol. 8560, pp. 77–92. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  3. 3.
    Aubert, C., Seiller, T.: Characterizing co-nl by a group action. Arxiv preprint abs/1209.3422 (2012)Google Scholar
  4. 4.
    Baader, F., Snyder, W.: Unification theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 445–532. Elsevier and MIT Press (2001)Google Scholar
  5. 5.
    Baillot, P., Mazza, D.: Linear logic by levels and bounded time complexity. Theoret. Comput. Sci. 411(2), 470–503 (2010)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Baillot, P., Pedicini, M.: Elementary complexity and geometry of interaction. Fund. Inform. 45(1-2), 1–31 (2001)MathSciNetzbMATHGoogle Scholar
  7. 7.
    Bellia, M., Occhiuto, M.E.: N-axioms parallel unification. Fund. Inform. 55(2), 115–128 (2003)MathSciNetzbMATHGoogle Scholar
  8. 8.
    Ben-Amram, A.M.: What is a “pointer machine”? Science of Computer Programming 26, 88–95 (1995)Google Scholar
  9. 9.
    Calimeri, F., Cozza, S., Ianni, G., Leone, N.: Computable functions in ASP: Theory and implementation. In: Garcia de la Banda, M., Pontelli, E. (eds.) ICLP 2008. LNCS, vol. 5366, pp. 407–424. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  10. 10.
    Dal Lago, U., Hofmann, M.: Bounded linear logic, revisited. Log. Meth. Comput. Sci. 6(4) (2010)Google Scholar
  11. 11.
    Dantsin, E., Eiter, T., Gottlob, G., Voronkov, A.: Complexity and expressive power of logic programming. ACM Comput. Surv. 33(3), 374–425 (2001)CrossRefGoogle Scholar
  12. 12.
    Dwork, C., Kanellakis, P.C., Mitchell, J.C.: On the sequential nature of unification. J. Log. Program. 1(1), 35–50 (1984)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Dwork, C., Kanellakis, P.C., Stockmeyer, L.J.: Parallel algorithms for term matching. SIAM J. Comput. 17(4), 711–731 (1988)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Gaboardi, M., Marion, J.Y., Ronchi Della Rocca, S.: An implicit characterization of pspace. ACM Trans. Comput. Log. 13(2), 18:1–18:36 (2012)Google Scholar
  15. 15.
    Girard, J.Y.: Linear logic. Theoret. Comput. Sci. 50(1), 1–101 (1987)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Girard, J.Y.: Geometry of interaction 1: Interpretation of system F. Studies in Logic and the Foundations of Mathematics 127, 221–260 (1989)MathSciNetCrossRefGoogle Scholar
  17. 17.
    Girard, J.Y.: Towards a geometry of interaction. In: Gray, J.W., Ščedrov, A. (eds.) Proceedings of the AMS-IMS-SIAM Joint Summer Research Conference held, June 14-20. Categories in Computer Science and Logic, vol. 92, pp. 69–108. AMS (1989)Google Scholar
  18. 18.
    Girard, J.Y.: Geometry of interaction III: Accommodating the additives. In: Girard, J.Y., Lafont, Y., Regnier, L. (eds.) Advances in Linear Logic. London Math. Soc. Lecture Note Ser., vol. 222, pp. 329–389. CUP (1995)Google Scholar
  19. 19.
    Girard, J.Y.: Light linear logic. In: Leivant, D. (ed.) LCC 1994. LNCS, vol. 960, pp. 145–176. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  20. 20.
    Girard, J.Y.: Normativity in logic. In: Dybjer, P., Lindstrm, S., Palmgren, E., Sundholm, G. (eds.) Epistemology versus Ontology. Logic, Epistemology, and the Unity of Science, vol. 27, pp. 243–263. Springer (2012)Google Scholar
  21. 21.
    Girard, J.Y.: Three lightings of logic. In: Ronchi Della Rocca, S. (ed.) CSL. LIPIcs, vol. 23, pp. 11–23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2013)Google Scholar
  22. 22.
    Hillebrand, G.G., Kanellakis, P.C., Mairson, H.G., Vardi, M.Y.: Undecidable boundedness problems for datalog programs. J. Log. Program. 25(2), 163–190 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
  23. 23.
    Holzer, M., Kutrib, M., Malcher, A.: Multi-head finite automata: Characterizations, concepts and open problems. In: Neary, T., Woods, D., Seda, A.K., Murphy, N. (eds.) CSP. EPTCS, vol. 1, pp. 93–107 (2008)Google Scholar
  24. 24.
    Jones, N.D.: Space-bounded reducibility among combinatorial problems. J. Comput. Syst. Sci. 11(1), 68–85 (1975)CrossRefzbMATHGoogle Scholar
  25. 25.
    Laurent, O.: A token machine for full geometry of interaction (extended abstract). In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol. 2044, pp. 283–297. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  26. 26.
    Lierler, Y., Lifschitz, V.: One more decidable class of finitely ground programs. In: Hill, P.M., Warren, D.S. (eds.) ICLP 2009. LNCS, vol. 5649, pp. 489–493. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  27. 27.
    Ohkubo, M., Yasuura, H., Yajima, S.: On parallel computation time of unification for restricted terms. Tech. rep., Kyoto University (1987)Google Scholar
  28. 28.
    Pighizzini, G.: Two-way finite automata: Old and recent results. Fund. Inform. 126(2-3), 225–246 (2013)MathSciNetzbMATHGoogle Scholar
  29. 29.
    Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23–41 (1965)CrossRefzbMATHGoogle Scholar
  30. 30.
    Savage, J.E.: Models of computation - exploring the power of computing. Addison-Wesley (1998)Google Scholar
  31. 31.
    Schöpp, U.: Stratified bounded affine logic for logarithmic space. In: LICS, pp. 411–420. IEEE Computer Society (2007)Google Scholar
  32. 32.
    Seiller, T.: Interaction graphs: Multiplicatives. Ann. Pure Appl. Logic 163, 1808–1837 (2012)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Clément Aubert
    • 1
  • Marc Bagnol
    • 1
  • Paolo Pistone
    • 1
  • Thomas Seiller
    • 2
  1. 1.CNRS, Centrale Marseille, I2M UMR 7373Aix Marseille UniversitéMarseilleFrance
  2. 2.I.H.É.S., Le Bois-MarieBures-sur-YvetteFrance

Personalised recommendations