Document Open Access Logo

Free-Cut Elimination in Linear Logic and an Application to a Feasible Arithmetic

Authors Patrick Baillot, Anupam Das

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2016.40.pdf
  • Filesize: 0.57 MB
  • 18 pages

Document Identifiers

Subject Classification

Keywords
  • proof theory
  • linear logic
  • bounded arithmetic
  • polynomial time computation
  • implicit computational complexity

Metrics

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

Abstract

We prove a general form of 'free-cut elimination' for first-order theories in linear logic, yielding normal forms of proofs where cuts are anchored to nonlogical steps. To demonstrate the usefulness of this result, we consider a version of arithmetic in linear logic, based on a previous axiomatisation by Bellantoni and Hofmann. We prove a witnessing theorem for a fragment of this arithmetic via the `witness function method', showing that the provably convergent functions are precisely the polynomial-time functions. The programs extracted are implemented in the framework of 'safe' recursive functions, due to Bellantoni and Cook, where the ! modality of linear logic corresponds to normal inputs of a safe recursive program.

Cite As Get BibTex

Patrick Baillot and Anupam Das. Free-Cut Elimination in Linear Logic and an Application to a Feasible Arithmetic. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 40:1-40:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.CSL.2016.40

Author Details

Patrick Baillot
Anupam Das

References

  1. Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. J. Log. Comput., 2(3):297-347, 1992. URL: http://dx.doi.org/10.1093/logcom/2.3.297.
  2. Arnon Avron. The semantics and proof theory of linear logic. Theor. Comput. Sci., 57:161-184, 1988. Google Scholar
  3. David Baelde. Least and greatest fixed points in linear logic. ACM Trans. Comput. Log., 13(1):2, 2012. Google Scholar
  4. Patrick Baillot and Anupam Das. Free-cut elimination in linear logic and an application to a feasible arithmetic. Preprint, 2016. URL: https://hal.archives-ouvertes.fr/hal-01316754.
  5. Arnold Beckmann and Samuel R. Buss. Corrected upper bounds for free-cut elimination. Theor. Comput. Sci., 412(39):5433-5445, 2011. Google Scholar
  6. Stephen Bellantoni and Stephen A. Cook. A new recursion-theoretic characterization of the polytime functions. Computational Complexity, 2:97-110, 1992. Google Scholar
  7. Stephen Bellantoni and Martin Hofmann. A new "feasible" arithmetic. J. Symb. Log., 67(1):104-116, 2002. Google Scholar
  8. Stephen J. Bellantoni. Predicative Recursion and Computational Complexity. PhD thesis, University of Toronto, 1992. Google Scholar
  9. Samuel R Buss. Bounded arithmetic, volume 86. Bibliopolis, 1986. Google Scholar
  10. Samuel R Buss. An introduction to proof theory. Handbook of proof theory, 137:1-78, 1998. Google Scholar
  11. Andrea Cantini. Polytime, combinatory logic and positive safe induction. Arch. Math. Log., 41(2):169-189, 2002. Google Scholar
  12. Nachum Dershowitz and Zohar Manna. Proving termination with multiset orderings. Commun. ACM, 22(8):465-476, August 1979. URL: http://dx.doi.org/10.1145/359138.359142.
  13. Harvey Friedman and Robert K. Meyer. Whither relevant arithmetic? J. Symb. Log., 57(3):824-831, 1992. URL: http://dx.doi.org/10.2307/2275433.
  14. Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1-102, 1987. URL: http://dx.doi.org/10.1016/0304-3975(87)90045-4.
  15. Jean-Yves Girard. Light linear logic. In Logical and Computational Complexity. Selected Papers. LCC'94., pages 145-176, 1994. URL: http://dx.doi.org/10.1007/3-540-60178-3_83.
  16. Jean-Yves Girard. Light linear logic. Inf. Comput., 143(2):175-204, 1998. Google Scholar
  17. Jean-Yves Girard, Andre Scedrov, and Philip J. Scott. Bounded linear logic: A modular approach to polynomial-time computability. Theor. Comput. Sci., 97(1):1-66, 1992. Google Scholar
  18. Yves Lafont. Soft linear logic and polynomial time. Theor. Comput. Sci., 318(1-2):163-180, 2004. Google Scholar
  19. Marc Lasson. Controlling program extraction in light logics. In Typed Lambda Calculi and Applications - 10th International Conference, TLCA 2011, Novi Sad, Serbia, June 1-3, 2011. Proceedings, volume 6690 of Lecture Notes in Computer Science, pages 123-137. Springer, 2011. Google Scholar
  20. Daniel Leivant. A foundational delineation of poly-time. Inf. Comput., 110(2):391-420, 1994. Google Scholar
  21. Daniel Leivant. Intrinsic theories and computational complexity. In Logical and Computational Complexity. Selected Papers. Logic and Computational Complexity, International Workshop LCC'94, Indianapolis, Indiana, USA, 13-16 October 1994, volume 960 of Lecture Notes in Computer Science, pages 177-194. Springer, 1995. Google Scholar
  22. Patrick Lincoln, John C. Mitchell, Andre Scedrov, and Natarajan Shankar. Decision problems for propositional linear logic. Ann. Pure Appl. Logic, 56(1-3):239-311, 1992. Google Scholar
  23. Jean-Yves Marion. Actual arithmetic and feasibility. In Proceedings of Computer Science Logic (CSL 2001), volume 2142 of Lecture Notes in Computer Science, pages 115-129. Springer, 2001. Google Scholar
  24. Dale Miller. Overview of linear logic programming. In Thomas Ehrhard, editor, Linear Logic in Computer Science, pages 316-119. Cambridge University Press, 2004. Google Scholar
  25. Andrzej S. Murawski and C.-H. Luke Ong. On an interpretation of safe recursion in light affine logic. Theor. Comput. Sci., 318(1-2):197-223, 2004. Google Scholar
  26. G. Takeuti. Proof Theory. North-Holland, Amsterdam, 1987. and ed. Google Scholar
  27. Kazushige Terui. Light affine set theory: A naive set theory of polynomial time. Studia Logica, 77(1):9-40, 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