Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Asperti, A., Danos, V., Laneve, C., Regnier, L.: Paths in the lambda-calculus. In: LICS, pp. 426–436. IEEE Computer Society (1994)
Aubert, C., Bagnol, M.: Unification and logarithmic space. In: Dowek, G. (ed.) RTA-TLCA 2014. LNCS, vol. 8560, pp. 77–92. Springer, Heidelberg (2014)
Aubert, C., Seiller, T.: Characterizing co-nl by a group action. Arxiv preprint abs/1209.3422 (2012)
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)
Baillot, P., Mazza, D.: Linear logic by levels and bounded time complexity. Theoret. Comput. Sci. 411(2), 470–503 (2010)
Baillot, P., Pedicini, M.: Elementary complexity and geometry of interaction. Fund. Inform. 45(1-2), 1–31 (2001)
Bellia, M., Occhiuto, M.E.: N-axioms parallel unification. Fund. Inform. 55(2), 115–128 (2003)
Ben-Amram, A.M.: What is a “pointer machine”? Science of Computer Programming 26, 88–95 (1995)
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)
Dal Lago, U., Hofmann, M.: Bounded linear logic, revisited. Log. Meth. Comput. Sci. 6(4) (2010)
Dantsin, E., Eiter, T., Gottlob, G., Voronkov, A.: Complexity and expressive power of logic programming. ACM Comput. Surv. 33(3), 374–425 (2001)
Dwork, C., Kanellakis, P.C., Mitchell, J.C.: On the sequential nature of unification. J. Log. Program. 1(1), 35–50 (1984)
Dwork, C., Kanellakis, P.C., Stockmeyer, L.J.: Parallel algorithms for term matching. SIAM J. Comput. 17(4), 711–731 (1988)
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)
Girard, J.Y.: Linear logic. Theoret. Comput. Sci. 50(1), 1–101 (1987)
Girard, J.Y.: Geometry of interaction 1: Interpretation of system F. Studies in Logic and the Foundations of Mathematics 127, 221–260 (1989)
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)
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)
Girard, J.Y.: Light linear logic. In: Leivant, D. (ed.) LCC 1994. LNCS, vol. 960, pp. 145–176. Springer, Heidelberg (1995)
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)
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)
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)
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)
Jones, N.D.: Space-bounded reducibility among combinatorial problems. J. Comput. Syst. Sci. 11(1), 68–85 (1975)
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)
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)
Ohkubo, M., Yasuura, H., Yajima, S.: On parallel computation time of unification for restricted terms. Tech. rep., Kyoto University (1987)
Pighizzini, G.: Two-way finite automata: Old and recent results. Fund. Inform. 126(2-3), 225–246 (2013)
Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23–41 (1965)
Savage, J.E.: Models of computation - exploring the power of computing. Addison-Wesley (1998)
Schöpp, U.: Stratified bounded affine logic for logarithmic space. In: LICS, pp. 411–420. IEEE Computer Society (2007)
Seiller, T.: Interaction graphs: Multiplicatives. Ann. Pure Appl. Logic 163, 1808–1837 (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Aubert, C., Bagnol, M., Pistone, P., Seiller, T. (2014). Logic Programming and Logarithmic Space. In: Garrigue, J. (eds) Programming Languages and Systems. APLAS 2014. Lecture Notes in Computer Science, vol 8858. Springer, Cham. https://doi.org/10.1007/978-3-319-12736-1_3
Download citation
DOI: https://doi.org/10.1007/978-3-319-12736-1_3
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-12735-4
Online ISBN: 978-3-319-12736-1
eBook Packages: Computer ScienceComputer Science (R0)