Non-wellfounded parsimonious proofs and non-uniform complexity

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. We present non-wellfounded parsimonious proof systems capturing the classes $\mathbf{F}\mathbf{P}$ and $\mathbf{F}\mathbf{P}\mathrm{/}\mathsf{p}\mathsf{o}\mathsf{l}\mathsf{y}$. Soundness is established via a polynomial modulus of continuity for continuous cut-elimination. Completeness relies on an encoding of polynomial Turing machines with advice within a type assignment system based on parsimonious logic. As a byproduct of our proof methods, we establish a series of characterisation results for various finitary proof systems.