Speaker
Gianluca Curzi
University of Gothenburg
Talks at this conference:
Friday, 18:10, J330 
Nonwellfounded parsimonious proofs and nonuniform complexity 
Authors: Matteo Acclavio, Gianluca Curzi and Giulio Guerrieri Cyclic and nonwellfounded prooftheory has established itself as an ideal framework for studying (co)inductive reasoning, hence to express computationally (co)recursion mechanisms under the CurryHoward 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 polynomialsize circuits (\(\mathbf{FP}/\mathsf{poly}\)) has been presented, where nonuniformity in complexity theory is modelled via nonwellfounded proofs. In this paper we investigate the complexitytheoretical aspects of cyclic and nonwellfounded 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 nonwellfounded parsimonious proof systems capturing the classes \(\mathbf{FP}\) and \(\mathbf{FP}/\mathsf{poly}\), essentially restating the results in [1] for parsimonious logic to a nonwellfounded prooftheoretic setting. Soundness is established via a polynomial modulus of continuity for continuous cutelimination. Completeness relies on an encoding of polynomial Turing machines with advice. Bibliography
