Logic Colloquium 2024


Gianluca Curzi

University of Gothenburg

Talks at this conference:

  Friday, 18:10, J330

Non-wellfounded parsimonious proofs and non-uniform complexity

Authors: Matteo Acclavio, Gianluca Curzi and Giulio Guerrieri

Cyclic and non-wellfounded proof-theory has established itself as an ideal framework for studying (co)inductive reasoning, hence to express computationally (co)recursion mechanisms under the Curry-Howard correspondence paradigm.

In [3] the second author showed how cyclic proofs can be employed in computational complexity, yielding an implicit characterisation of the polynomial time computable functions (\(\mathbf{FP}\)) inspired by Bellantoni and Cook’s algebra of safe recursion [2]. In a follow up paper [4], a characterisation of the class of functions computed by polynomial-size circuits (\(\mathbf{FP}/\mathsf{poly}\)) has been presented, where non-uniformity in complexity theory is modelled via non-wellfounded proofs.

In this paper we investigate the complexity-theoretical aspects of cyclic and non-wellfounded proofs in the context of parsimonious logic, a variant of linear logic where the exponential modality ! is interpreted as a constructor for streams over finite data (see, e.g., [1]). We present non-wellfounded parsimonious proof systems capturing the classes \(\mathbf{FP}\) and \(\mathbf{FP}/\mathsf{poly}\), essentially restating the results in [1] for parsimonious logic to a non-wellfounded proof-theoretic setting. Soundness is established via a polynomial modulus of continuity for continuous cut-elimination. Completeness relies on an encoding of polynomial Turing machines with advice.


  1. D. Mazza and K. Terui,Parsimonious Types and Non-uniform Computation,Automata, Languages, and Programming - 42nd International Colloquium,{ICALP},vol. 9135,Springer, 2015,pp. 350–361.
  2. S. Bellantoni and S. Cook,A New Recursion-Theoretic Characterization of the Polytime Functions (Extended Abstract),Proceedings of the Twenty-Fourth Annual ACM Symposium on Theory of Computing,Association for Computing Machinery, 1992,pp. 283–293.
  3. G. Curzi andA. Das,Cyclic Implicit Complexity,Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science,Association for Computing Machinery,2022,pp. 1–13.
  4. G. Curzi andA. Das,Non-Uniform Complexity via Non-Wellfounded Proofs,31st {EACSL} Annual Conference on Computer Science Logic, {CSL}vol. 252,Schloss Dagstuhl - Leibniz-Zentrum f{ü}r Informatik,2023,pp. 16:1–16:18.