Document Open Access Logo

Simple Parsimonious Types and Logarithmic Space

Author Damiano Mazza

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2015.24.pdf
  • Filesize: 0.59 MB
  • 17 pages

Document Identifiers

Subject Classification

Keywords
  • implicit computational complexity
  • linear logic
  • geometry of interaction

Metrics

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

Abstract

We present a functional characterization of deterministic logspace-computable predicates based on a variant (although not a subsystem) of propositional linear logic, which we call parsimonious logic. The resulting calculus is simply-typed and contains no primitive besides those provided by the underlying logical system, which makes it one of the simplest higher-order languages capturing logspace currently known. Completeness of the calculus uses the descriptive complexity characterization of logspace (we encode first-order logic with deterministic closure), whereas soundness is established by executing terms on a token machine (using the geometry of interaction).

Cite As Get BibTex

Damiano Mazza. Simple Parsimonious Types and Logarithmic Space. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 24-40, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CSL.2015.24

Author Details

Damiano Mazza

References

  1. Beniamino Accattoli and Ugo Dal Lago. Beta reduction is invariant, indeed. In Proceedings of CSL-LICS, page 8, 2014. Google Scholar
  2. Patrick Baillot and Damiano Mazza. Linear logic by levels and bounded time complexity. Theor. Comput. Sci., 411(2):470-503, 2010. Google Scholar
  3. Stephen Bellantoni and Stephen A. Cook. A new recursion-theoretic characterization of the polytime functions. Computational Complexity, 2:97-110, 1992. Google Scholar
  4. Guillaume Bonfante. Some programming languages for logspace and ptime. In Proceedings of AMAST, pages 66-80, 2006. Google Scholar
  5. Ugo Dal Lago. Context semantics, linear logic, and computational complexity. ACM Trans. Comput. Log., 10(4), 2009. Google Scholar
  6. Ugo Dal Lago and Ulrich Schöpp. Functional programming in sublinear space. In Proceedings of ESOP, pages 205-225, 2010. Google Scholar
  7. Ugo Dal Lago and Ulrich Schöpp. Type inference for sublinear space functional programming. In Proceedings of APLAS, pages 376-391, 2010. Google Scholar
  8. Vincent Danos and Laurent Regnier. Reversible, irreversible and optimal lambda-machines. Theor. Comput. Sci., 227(1-2):79-97, 1999. Google Scholar
  9. Marco Gaboardi, Jean-Yves Marion, and Simona Ronchi Della Rocca. An implicit characterization of PSPACE. ACM Trans. Comput. Log., 13(2):18, 2012. Google Scholar
  10. Marco Gaboardi, Luca Roversi, and Luca Vercelli. A by-level analysis of multiplicative exponential linear logic. In Proceedings of MFCS, pages 344-355, 2009. Google Scholar
  11. Jean-Yves Girard. Geometry of interaction I: Interpretation of system F. In Proccedings of Logic Colloquium 1988, pages 221-260, 1989. Google Scholar
  12. Jean-Yves Girard. Light linear logic. Inf. Comput., 143(2):175-204, 1998. Google Scholar
  13. Martin Hofmann. A mixed modal/linear lambda calculus with applications to bellantoni-cook safe recursion. In Proceedings of CSL, pages 275-294, 1997. Google Scholar
  14. Martin Hofmann. Linear types and non-size-increasing polynomial time computation. Inf. Comput., 183(1):57-85, 2003. Google Scholar
  15. Neil Immerman. Descriptive complexity. Graduate texts in computer science. Springer, 1999. Google Scholar
  16. Neil D. Jones. Logspace and ptime characterized by programming languages. Theor. Comput. Sci., 228(1-2):151-174, 1999. Google Scholar
  17. Lars Kristiansen. Neat function algebraic characterizations of logspace and linspace. Computational Complexity, 14(1):72-88, 2005. Google Scholar
  18. Daniel Leivant and Jean-Yves Marion. Lambda calculus characterizations of poly-time. Fundam. Inform., 19(1/2), 1993. Google Scholar
  19. Damiano Mazza. An infinitary affine lambda-calculus isomorphic to the full lambda-calculus. In Proceedings of LICS, pages 471-480, 2012. Google Scholar
  20. Damiano Mazza. Non-uniform polytime computation in the infinitary affine lambda-calculus. In Proceedings of ICALP, Part II, pages 305-317, 2014. Google Scholar
  21. Damiano Mazza and Kazushige Terui. Parsimonious types and non-uniform computation. In Proceedings of ICALP, Part II, pages 350-361, 2015. Google Scholar
  22. Peter Møller Neergaard. A functional language for logarithmic space. In Proceedings of APLAS, pages 311-326, 2004. Google Scholar
  23. Ramyaa Ramyaa and Daniel Leivant. Ramified corecurrence and logspace. Electr. Notes Theor. Comput. Sci., 276:247-261, 2011. Google Scholar
  24. Ulrich Schöpp. Space-efficient computation by interaction. In Proceedings of CSL, pages 606-621, 2006. Google Scholar
  25. Ulrich Schöpp. Stratified bounded affine logic for logarithmic space. In Proceedings of LICS, pages 411-420, 2007. Google Scholar
  26. Kazushige Terui. Proof nets and boolean circuits. In Proceedings of LICS, pages 182-191, 2004. Google Scholar
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