Speaker
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. Bibliography
|