Document Open Access Logo

Non-Uniform Complexity via Non-Wellfounded Proofs

Authors Gianluca Curzi, Anupam Das

PDF
Thumbnail PDF

File

LIPIcs.CSL.2023.16.pdf
  • Filesize: 0.83 MB
  • 18 pages

Document Identifiers

Author Details

Gianluca Curzi
  • University of Birmingham, UK
Anupam Das
  • University of Birmingham, UK

Funding

Both authors are supported by a UKRI Future Leaders Fellowship, Structure vs. Invariants in Proofs, project reference MR/S035540/1.

Acknowledgements

We thank the anonymous reviewers for their helpful comments and suggestions.

Cite AsGet BibTex

Gianluca Curzi and Anupam Das. Non-Uniform Complexity via Non-Wellfounded Proofs. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CSL.2023.16

Abstract

Cyclic and non-wellfounded proofs are now increasingly employed to establish metalogical results in a variety of settings, in particular for type systems with forms of (co)induction. Under the Curry-Howard correspondence, a cyclic proof can be seen as a typing derivation "with loops", closer to low-level machine models, and so comprise a highly expressive computational model that nonetheless enjoys excellent metalogical properties. In recent work, we showed how the cyclic proof setting can be further employed to model computational complexity, yielding characterisations of the polynomial time and elementary computable functions. These characterisations are "implicit", inspired by Bellantoni and Cook’s famous algebra of safe recursion, but exhibit greater expressivity thanks to the looping capacity of cyclic proofs. In this work we investigate the capacity for non-wellfounded proofs, where finite presentability is relaxed, to model non-uniformity in complexity theory. In particular, we present a characterisation of the class FP/poly of functions computed by polynomial-size circuits. While relating non-wellfoundedness to non-uniformity is a natural idea, the precise amount of irregularity, informally speaking, required to capture FP/poly is given by proof-level conditions novel to cyclic proof theory. Along the way, we formalise some (presumably) folklore techniques for characterising non-uniform classes in relativised function algebras with appropriate oracles.

Subject Classification

ACM Subject Classification
  • Theory of computation → Complexity theory and logic
  • Theory of computation → Proof theory
Keywords
  • Cyclic proofs
  • non-wellfounded proof-theory
  • non-uniform complexity
  • polynomial time
  • safe recursion
  • implicit complexity

Metrics

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

Related Versions

References

  1. Sanjeev Arora and Boaz Barak. Computational Complexity - A Modern Approach. Cambridge University Press, 2009. URL: http://www.cambridge.org/catalogue/catalogue.asp?isbn=9780521424264.
  2. David Baelde, Amina Doumane, and Alexis Saurin. Infinitary proof theory: the multiplicative additive case. In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France, volume 62 of LIPIcs, pages 42:1-42:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.CSL.2016.42.
  3. Stephen Bellantoni. Predicative recursion and the polytime hierarchy. In Peter Clote and Jeffrey B. Remmel, editors, Feasible Mathematics II, pages 15-29, Boston, MA, 1995. Birkhäuser Boston. Google Scholar
  4. Stephen Bellantoni and Stephen Cook. A new recursion-theoretic characterization of the polytime functions (extended abstract). In Proceedings of the Twenty-Fourth Annual ACM Symposium on Theory of Computing, STOC '92, pages 283-293, New York, NY, USA, 1992. Association for Computing Machinery. URL: https://doi.org/10.1145/129712.129740.
  5. Stefano Berardi and Makoto Tatsuta. Equivalence of inductive definitions and cyclic proofs under arithmetic. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005114.
  6. Stefano Berardi and Makoto Tatsuta. Classical system of Martin-Lof’s inductive definitions is not equivalent to cyclic proofs. Log. Methods Comput. Sci., 15(3), 2019. URL: https://doi.org/10.23638/LMCS-15(3:10)2019.
  7. James Brotherston. Sequent calculus proof systems for inductive definitions. PhD thesis, University of Edinburgh, 2006. PhD thesis. Google Scholar
  8. James Brotherston and Alex Simpson. Sequent calculi for induction and infinite descent. Journal of Logic and Computation, 21(6):1177-1216, 2011. Google Scholar
  9. Samuel R. Buss. Chapter i - an introduction to proof theory. In Samuel R. Buss, editor, Handbook of Proof Theory, volume 137 of Studies in Logic and the Foundations of Mathematics, pages 1-78. Elsevier, 1998. URL: https://doi.org/10.1016/S0049-237X(98)80016-5.
  10. Gianluca Curzi and Anupam Das. Cyclic implicit complexity. CoRR, abs/2110.01114, 2021. To appear in proceedings of LICS 2022. URL: http://arxiv.org/abs/2110.01114.
  11. Anupam Das. A circular version of Gödel’s T and its abstraction complexity. CoRR, abs/2012.14421, 2020. URL: http://arxiv.org/abs/2012.14421.
  12. Anupam Das. On the logical complexity of cyclic arithmetic. Log. Methods Comput. Sci., 16(1), 2020. URL: https://doi.org/10.23638/LMCS-16(1:1)2020.
  13. Anupam Das. On the logical strength of confluence and normalisation for cyclic proofs. In Naoki Kobayashi, editor, 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference), volume 195 of LIPIcs, pages 29:1-29:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.FSCD.2021.29.
  14. Anupam Das and Damien Pous. A cut-free cyclic proof system for Kleene algebra. In International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, pages 261-277. Springer, 2017. Google Scholar
  15. Anupam Das and Damien Pous. Non-Wellfounded Proof Theory For (Kleene+Action) (Algebras+Lattices). In Dan Ghica and Achim Jung, editors, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018), volume 119 of Leibniz International Proceedings in Informatics (LIPIcs), pages 19:1-19:18, Dagstuhl, Germany, 2018. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2018.19.
  16. Christian Dax, Martin Hofmann, and Martin Lange. A proof system for the linear time μ-calculus. In International Conference on Foundations of Software Technology and Theoretical Computer Science, pages 273-284. Springer, 2006. Google Scholar
  17. Abhishek De and Alexis Saurin. Infinets: The parallel syntax for non-wellfounded proof-theory. In Serenella Cerrito and Andrei Popescu, editors, Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019, London, UK, September 3-5, 2019, Proceedings, volume 11714 of Lecture Notes in Computer Science, pages 297-316. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-29026-9_17.
  18. Jérôme Fortier and Luigi Santocanale. Cuts for circular proofs: semantics and cut-elimination. In Computer Science Logic 2013 (CSL 2013). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013. Google Scholar
  19. Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1-102, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  20. Emmanuel Hainry, Damiano Mazza, and Romain Péchoux. Polynomial time over the reals with parsimony. In Keisuke Nakano and Konstantinos Sagonas, editors, Functional and Logic Programming - 15th International Symposium, FLOPS 2020, Akita, Japan, September 14-16, 2020, Proceedings, volume 12073 of Lecture Notes in Computer Science, pages 50-65. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-59025-3_4.
  21. Martin Hofmann. A mixed modal/linear lambda calculus with applications to Bellantoni-Cook safe recursion. In Mogens Nielsen and Wolfgang Thomas, editors, Computer Science Logic, 11th International Workshop, CSL '97, Annual Conference of the EACSL, Aarhus, Denmark, August 23-29, 1997, Selected Papers, volume 1414 of Lecture Notes in Computer Science, pages 275-294. Springer, 1997. URL: https://doi.org/10.1007/BFb0028020.
  22. Stephen Cole Kleene. Introduction to Metamathematics. Bubliotheca Mathematica. Wolters-Noordhoff Publishing, 7 edition, 1971. Google Scholar
  23. Ker-I Ko. Complexity Theory of Real Functions. Birkhauser Boston Inc., USA, 1991. Google Scholar
  24. Denis Kuperberg, Laureline Pinault, and Damien Pous. Cyclic proofs, system T, and the power of contraction. Proc. ACM Program. Lang., 5(POPL):1-28, 2021. URL: https://doi.org/10.1145/3434282.
  25. Ugo Dal Lago and Paolo Parisen Toldin. A higher-order characterization of probabilistic polynomial time. Inf. Comput., 241:114-141, 2015. URL: https://doi.org/10.1016/j.ic.2014.10.009.
  26. Daniel Leivant. A foundational delineation of computational feasiblity. In Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS '91), Amsterdam, The Netherlands, July 15-18, 1991, pages 2-11. IEEE Computer Society, 1991. URL: https://doi.org/10.1109/LICS.1991.151625.
  27. Damiano Mazza. Non-uniform polytime computation in the infinitary affine lambda-calculus. In Javier Esparza, Pierre Fraigniaud, Thore Husfeldt, and Elias Koutsoupias, editors, Automata, Languages, and Programming - 41st International Colloquium, ICALP 2014, Copenhagen, Denmark, July 8-11, 2014, Proceedings, Part II, volume 8573 of Lecture Notes in Computer Science, pages 305-317. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-43951-7_26.
  28. Damiano Mazza. Simple parsimonious types and logarithmic space. In Stephan Kreutzer, editor, 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany, volume 41 of LIPIcs, pages 24-40. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.CSL.2015.24.
  29. Damiano Mazza and Kazushige Terui. Parsimonious types and non-uniform computation. In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann, editors, Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II, volume 9135 of Lecture Notes in Computer Science, pages 350-361. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-47666-6_28.
  30. Grigori E Mints. Finite investigations of transfinite derivations. Journal of Soviet Mathematics, 10(4):548-596, 1978. Google Scholar
  31. Damian Niwiński and Igor Walukiewicz. Games for the μ-calculus. Theoretical Computer Science, 163(1-2):99-116, 1996. Google Scholar
  32. Alex Simpson. Cyclic arithmetic is equivalent to peano arithmetic. In Javier Esparza and Andrzej S. Murawski, editors, Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10203 of Lecture Notes in Computer Science, pages 283-300, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_17.
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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact