# Non-wellfounded parsimonious proofs and non-uniform complexity

## Gianluca Curzi

**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.

## Bibliography

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