Document Open Access Logo

From Normal Functors to Logarithmic Space Queries (Track B: Automata, Logic, Semantics, and Theory of Programming)

Authors Lê Thành Dũng Nguyễn , Cécilia Pradic

PDF

File

Thumbnail PDF
PDF
LIPIcs.ICALP.2019.123.pdf
  • Filesize: 0.57 MB
  • 15 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Linear logic
  • Theory of computation → Complexity theory and logic
  • Theory of computation → Finite Model Theory
Keywords
  • coherence spaces
  • elementary linear logic
  • semantic evaluation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We introduce a new approach to implicit complexity in linear logic, inspired by functional database query languages and using recent developments in effective denotational semantics of polymorphism. We give the first sub-polynomial upper bound in a type system with impredicative polymorphism; adding restrictions on quantifiers yields a characterization of logarithmic space, for which extensional completeness is established via descriptive complexity.

Cite As Get BibTex

Lê Thành Dũng Nguyễn and Cécilia Pradic. From Normal Functors to Logarithmic Space Queries (Track B: Automata, Logic, Semantics, and Theory of Programming). In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 123:1-123:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.ICALP.2019.123

Author Details

Lê Thành Dũng Nguyễn
  • LIPN, UMR 7030 CNRS, Université Paris 13, Sorbonne Paris Cité, France
Cécilia Pradic
  • ENS de Lyon, Université de Lyon, LIP, France
  • University of Warsaw, Faculty of Mathematics, Informatics and Mechanics, Poland

Funding

  • Nguyễn, Lê Thành Dũng: Partially supported by the Elica project (ANR-14-CE25-0005).
  • Pradic, Cécilia: Partially supported by the the RAPIDO project (ANR-14-CE25-0007).

Acknowledgements

L. T. D. Nguyễn wishes to thank Damiano Mazza, Thomas Seiller and Kazushige Terui for highly instructive discussions. C. Pradic thanks Alexis Ghyselen for his valuable feedback on a first draft of this paper.

References

  1. Serge Abiteboul and Gerd Hillebrand. Space usage in functional query languages. In Gerhard Goos, Juris Hartmanis, Jan Leeuwen, Georg Gottlob, and Moshe Y. Vardi, editors, Database Theory — ICDT '95, volume 893, pages 439-454. Springer Berlin Heidelberg, Berlin, Heidelberg, 1995. URL: http://dx.doi.org/10.1007/3-540-58907-4_33.
  2. Patrick Baillot. On the expressivity of elementary linear logic: Characterizing Ptime and an exponential time hierarchy. Information and Computation, 241:3-31, April 2015. URL: http://dx.doi.org/10.1016/j.ic.2014.10.005.
  3. Patrick Baillot, Erika De Benedetti, and Simona Ronchi Della Rocca. Characterizing polynomial and exponential complexity classes in elementary lambda-calculus. Information and Computation, 261:55-77, August 2018. URL: http://dx.doi.org/10.1016/j.ic.2018.05.005.
  4. Patrick Baillot and Alexis Ghyselen. Combining Linear Logic and Size Types for Implicit Complexity. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018), pages 9:1-9:21, 2018. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2018.9.
  5. Pierre Boudes. Projecting Games on Hypercoherences. In Automata, Languages and Programming, volume 3142, pages 257-268. Springer Berlin Heidelberg, Berlin, Heidelberg, 2004. URL: http://dx.doi.org/10.1007/978-3-540-27836-8_24.
  6. Ugo Dal Lago and Martin Hofmann. Realizability models and implicit complexity. Theoretical Computer Science, 412(20):2029-2047, April 2011. URL: http://dx.doi.org/10.1016/j.tcs.2010.12.025.
  7. Ugo Dal Lago and Ulrich Schöpp. Computation by interaction for space-bounded functional programming. Information and Computation, 248:150-194, June 2016. URL: http://dx.doi.org/10.1016/j.ic.2015.04.006.
  8. Vincent Danos and Jean-Baptiste Joinet. Linear logic and elementary time. Information and Computation, 183(1):123-137, May 2003. URL: http://dx.doi.org/10.1016/S0890-5401(03)00010-5.
  9. Vincent Danos and Laurent Regnier. Reversible, irreversible and optimal λ-machines. Theoretical Computer Science, 227(1):79-97, September 1999. URL: http://dx.doi.org/10.1016/S0304-3975(99)00049-3.
  10. Thomas Ehrhard. Parallel and serial hypercoherences. Theoretical Computer Science, 247(1):39-81, September 2000. URL: http://dx.doi.org/10.1016/S0304-3975(00)00173-0.
  11. Ronald Fagin. Contributions to the model theory of finite structures. PhD thesis, University of California, Berkeley, 1973. Google Scholar
  12. Jean-Yves Girard. The system F of variable types, fifteen years later. Theoretical Computer Science, 45:159-192, January 1986. URL: http://dx.doi.org/10.1016/0304-3975(86)90044-7.
  13. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-101, January 1987. URL: http://dx.doi.org/10.1016/0304-3975(87)90045-4.
  14. Jean-Yves Girard. Geometry of Interaction 1: Interpretation of System F. In R. Ferro, C. Bonotto, S. Valentini, and A. Zanardo, editors, Studies in Logic and the Foundations of Mathematics, volume 127 of Logic Colloquium '88, pages 221-260. Elsevier, January 1989. Google Scholar
  15. Jean-Yves Girard. Linear logic: its syntax and semantics. In Jean-Yves Girard, Yves Lafont, and Laurent Regnier, editors, Advances in Linear Logic, volume 222 of London Mathematical Society Lecture Notes. Cambridge University Press, 1995. Google Scholar
  16. Jean-Yves Girard. Light Linear Logic. Information and Computation, 143(2):175-204, June 1998. URL: http://dx.doi.org/10.1006/inco.1998.2700.
  17. Yuri Gurevich. Algebras of feasible functions. In 24th Annual Symposium on Foundations of Computer Science (FOCS 1983), pages 210-214, Tucson, AZ, USA, November 1983. URL: http://dx.doi.org/10.1109/SFCS.1983.5.
  18. Gerd G. Hillebrand. Finite Model Theory in the Simply Typed Lambda Calculus. PhD thesis, Brown University, Providence, RI, USA, 1994. Google Scholar
  19. Gerd G. Hillebrand and Paris C. Kanellakis. Functional Database Query Languages As Typed Lambda Calculi of Fixed Order (Extended Abstract). In Proceedings of the Thirteenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, PODS '94, pages 222-231, New York, NY, USA, 1994. ACM. URL: http://dx.doi.org/10.1145/182591.182615.
  20. Gerd G. Hillebrand and Paris C. Kanellakis. On the Expressive Power of Simply Typed and Let-Polymorphic Lambda Calculi. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996, pages 253-263. IEEE Computer Society, 1996. URL: http://dx.doi.org/10.1109/LICS.1996.561337.
  21. Gerd G. Hillebrand, Paris C. Kanellakis, and Harry G. Mairson. Database Query Languages Embedded in the Typed Lambda Calculus. Information and Computation, 127(2):117-144, June 1996. URL: http://dx.doi.org/10.1006/inco.1996.0055.
  22. Neil Immerman. Languages that Capture Complexity Classes. SIAM Journal on Computing, 16(4):760-778, August 1987. URL: http://dx.doi.org/10.1137/0216051.
  23. Neil Immerman. Nondeterministic Space is Closed under Complementation. SIAM Journal on Computing, 17(5):935-938, October 1988. URL: http://dx.doi.org/10.1137/0217058.
  24. Donald E. Knuth. Mathematics and Computer Science: Coping with Finiteness. Science, 194(4271):1235-1242, 1976. URL: http://dx.doi.org/10.1126/science.194.4271.1235.
  25. Lars Kristiansen. Higher Types, Finite Domains and Resource-bounded Turing Machines. Journal of Logic and Computation, 22(2):281-304, April 2012. URL: http://dx.doi.org/10.1093/logcom/exq009.
  26. Daniel Leivant. Reasoning about functional programs and complexity classes associated with type disciplines. In 24th Annual Symposium on Foundations of Computer Science (FOCS 1983), pages 460-469, Tucson, AZ, USA, November 1983. URL: http://dx.doi.org/10.1109/SFCS.1983.50.
  27. Harry G. Mairson. A simple proof of a theorem of Statman. Theoretical Computer Science, 103(2):387-394, September 1992. URL: http://dx.doi.org/10.1016/0304-3975(92)90020-G.
  28. Damiano Mazza. Simple Parsimonious Types and Logarithmic Space. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015), pages 24-40, 2015. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2015.24.
  29. Damiano Mazza and Kazushige Terui. Parsimonious Types and Non-uniform Computation. In Automata, Languages, and Programming, Lecture Notes in Computer Science, pages 350-361. Springer, Berlin, Heidelberg, July 2015. URL: http://dx.doi.org/10.1007/978-3-662-47666-6_28.
  30. Paul-André Melliès. Sequential algorithms and strongly stable functions. Theoretical Computer Science, 343(1):237-281, October 2005. URL: http://dx.doi.org/10.1016/j.tcs.2005.05.015.
  31. Paul-André Melliès. On dialogue games and coherent strategies. In Simona Ronchi Della Rocca, editor, Computer Science Logic 2013 (CSL 2013), pages 540-562, 2013. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2013.540.
  32. Lê Thành Dũng Nguyễn. Around finite second-order coherence spaces. CoRR, abs/1902.00196, 2019. URL: http://arxiv.org/abs/1902.00196.
  33. A. Pavan, Raghunath Tewari, and N. V. Vinodchandran. On the power of unambiguity in log-space. computational complexity, 21(4):643-670, December 2012. URL: http://dx.doi.org/10.1007/s00037-012-0047-3.
  34. K. Reinhardt and E. Allender. Making Nondeterminism Unambiguous. SIAM Journal on Computing, 29(4):1118-1131, January 2000. URL: http://dx.doi.org/10.1137/S0097539798339041.
  35. Walter L. Ruzzo, Janos Simon, and Martin Tompa. Space-bounded hierarchies and probabilistic computations. Journal of Computer and System Sciences, 28(2):216-230, April 1984. URL: http://dx.doi.org/10.1016/0022-0000(84)90066-7.
  36. Ulrich Schöpp. Stratified Bounded Affine Logic for Logarithmic Space. In 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), pages 411-420, July 2007. URL: http://dx.doi.org/10.1109/LICS.2007.45.
  37. Richard Statman. The typed λ-calculus is not elementary recursive. Theoretical Computer Science, 9(1):73-81, July 1979. URL: http://dx.doi.org/10.1016/0304-3975(79)90007-0.
  38. Kazushige Terui. Proof Nets and Boolean Circuits. In 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings, pages 182-191, 2004. URL: http://dx.doi.org/10.1109/LICS.2004.1319612.
  39. Kazushige Terui. Semantic Evaluation, Intersection Types and Complexity of Simply Typed Lambda Calculus. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12), pages 323-338, 2012. URL: http://dx.doi.org/10.4230/LIPIcs.RTA.2012.323.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact