Document

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

## File

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

## Cite As

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

## 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.
##### Keywords
• proof theory
• linear logic
• bounded arithmetic
• polynomial time computation
• implicit computational complexity

## Metrics

• Access Statistics
• Total Accesses (updated on a weekly basis)
0

## 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.
3. David Baelde. Least and greatest fixed points in linear logic. ACM Trans. Comput. Log., 13(1):2, 2012.
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.
6. Stephen Bellantoni and Stephen A. Cook. A new recursion-theoretic characterization of the polytime functions. Computational Complexity, 2:97-110, 1992.
7. Stephen Bellantoni and Martin Hofmann. A new "feasible" arithmetic. J. Symb. Log., 67(1):104-116, 2002.
8. Stephen J. Bellantoni. Predicative Recursion and Computational Complexity. PhD thesis, University of Toronto, 1992.
9. Samuel R Buss. Bounded arithmetic, volume 86. Bibliopolis, 1986.
10. Samuel R Buss. An introduction to proof theory. Handbook of proof theory, 137:1-78, 1998.
11. Andrea Cantini. Polytime, combinatory logic and positive safe induction. Arch. Math. Log., 41(2):169-189, 2002.
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.
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.
18. Yves Lafont. Soft linear logic and polynomial time. Theor. Comput. Sci., 318(1-2):163-180, 2004.
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.
20. Daniel Leivant. A foundational delineation of poly-time. Inf. Comput., 110(2):391-420, 1994.
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.
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.
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.
24. Dale Miller. Overview of linear logic programming. In Thomas Ehrhard, editor, Linear Logic in Computer Science, pages 316-119. Cambridge University Press, 2004.
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.
26. G. Takeuti. Proof Theory. North-Holland, Amsterdam, 1987. and ed.
27. Kazushige Terui. Light affine set theory: A naive set theory of polynomial time. Studia Logica, 77(1):9-40, 2004.
X

Feedback for Dagstuhl Publishing