-
Non-wellfounded parsimonious proofs and non-uniform complexity
Authors:
Matteo Acclavio,
Gianluca Curzi,
Giulio Guerrieri
Abstract:
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{FPTIME}$ and $\mathbf{FP}/\mathsf{poly}$. Soundness is…
▽ More
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{FPTIME}$ and $\mathbf{FP}/\mathsf{poly}$. Soundness is established via a polynomial modulus of continuity for continuous cut-elimination. Completeness relies on an encoding of polynomial Turing machines with advice.
As a byproduct of our proof methods, we establish a series of characterisation results for various finitary proof systems.
△ Less
Submitted 4 April, 2024;
originally announced April 2024.
-
Infinitary cut-elimination via finite approximations (extended version)
Authors:
Matteo Acclavio,
Gianluca Curzi,
Giulio Guerrieri
Abstract:
We investigate non-wellfounded proof systems based on parsimonious logic, a weaker variant of linear logic where the exponential modality ! is interpreted as a constructor for streams over finite data. Logical consistency is maintained at a global level by adapting a standard progressing criterion. We present an infinitary version of cut-elimination based on finite approximations, and we prove tha…
▽ More
We investigate non-wellfounded proof systems based on parsimonious logic, a weaker variant of linear logic where the exponential modality ! is interpreted as a constructor for streams over finite data. Logical consistency is maintained at a global level by adapting a standard progressing criterion. We present an infinitary version of cut-elimination based on finite approximations, and we prove that, in presence of the progressing criterion, it returns well-defined non-wellfounded proofs at its limit. Furthermore, we show that cut-elimination preserves the progressive criterion and various regularity conditions internalizing degrees of proof-theoretical uniformity. Finally, we provide a denotational semantics for our systems based on the relational model.
△ Less
Submitted 27 May, 2024; v1 submitted 15 August, 2023;
originally announced August 2023.
-
Computational expressivity of (circular) proofs with fixed points
Authors:
Gianluca Curzi,
Anupam Das
Abstract:
We study the computational expressivity of proof systems with fixed point operators, within the `proofs-as-programs' paradigm. We start with a calculus $μ\mathsf{LJ}$ (due to Clairambault) that extends intuitionistic logic by least and greatest positive fixed points. Based in the sequent calculus, $μ\mathsf{LJ}$ admits a standard extension to a `circular' calculus $\mathsf{C}μ\mathsf{LJ}$.
Our m…
▽ More
We study the computational expressivity of proof systems with fixed point operators, within the `proofs-as-programs' paradigm. We start with a calculus $μ\mathsf{LJ}$ (due to Clairambault) that extends intuitionistic logic by least and greatest positive fixed points. Based in the sequent calculus, $μ\mathsf{LJ}$ admits a standard extension to a `circular' calculus $\mathsf{C}μ\mathsf{LJ}$.
Our main result is that, perhaps surprisingly, both $μ\mathsf{LJ}$ and $\mathsf{C}μ\mathsf{LJ}$ represent the same first-order functions: those provably total in $Π^1_2$-$\mathsf{CA}_0$, a subsystem of second-order arithmetic beyond the `big five' of reverse mathematics and one of the strongest theories for which we have an ordinal analysis (due to Rathjen). This solves various questions in the literature on the computational strength of (circular) proof systems with fixed points.
For the lower bound we give a realisability interpretation from an extension of Peano Arithmetic by fixed points that has been shown to be arithmetically equivalent to $Π^1_2$-$\mathsf{CA}_0$ (due to Möllerfeld). For the upper bound we construct a novel computability model in order to give a totality argument for circular proofs with fixed points. In fact we formalise this argument itself within $Π^1_2$-$\mathsf{CA}_0$ in order to obtain the tight bounds we are after.
Along the way we develop some novel reverse mathematics for the Knaster-Tarski fixed point theorem.
△ Less
Submitted 27 May, 2024; v1 submitted 28 February, 2023;
originally announced February 2023.
-
Non-uniform complexity via non-wellfounded proofs
Authors:
Gianluca Curzi,
Anupam Das
Abstract:
Cyclic and non-wellfounded proofs are now increasingly employed to establish metalogical results in a variety of settings, in particular for type systems with forms of (co)induction. Under the Curry-Howard correspondence, a cyclic proof can be seen as a typing derivation 'with loops', closer to low-level machine models, and so comprise a highly expressive computational model that nonetheless enjoy…
▽ More
Cyclic and non-wellfounded proofs are now increasingly employed to establish metalogical results in a variety of settings, in particular for type systems with forms of (co)induction. Under the Curry-Howard correspondence, a cyclic proof can be seen as a typing derivation 'with loops', closer to low-level machine models, and so comprise a highly expressive computational model that nonetheless enjoys excellent metalogical properties.
In recent work, we showed how the cyclic proof setting can be further employed to model computational complexity, yielding characterisations of the polynomial time and elementary computable functions. These characterisations are 'implicit', inspired by Bellantoni and Cook's famous algebra of safe recursion, but exhibit greater expressivity thanks to the looping capacity of cyclic proofs.
In this work we investigate the capacity for non-wellfounded proofs, where finite presentability is relaxed, to model non-uniformity in complexity theory. In particular, we present a characterisation of the class $\mathsf{FP/poly}$ of functions computed by polynomial-size circuits. While relating non-wellfoundedness to non-uniformity is a natural idea, the precise amount of irregularity, informally speaking, required to capture $\mathsf{FP/poly}$ is given by proof-level conditions novel to cyclic proof theory. Along the way, we formalise some (presumably) folklore techniques for characterising non-uniform classes in relativised function algebras with appropriate oracles.
△ Less
Submitted 29 November, 2022;
originally announced November 2022.
-
Cyclic Implicit Complexity
Authors:
Gianluca Curzi,
Anupam Das
Abstract:
Circular (or cyclic) proofs have received increasing attention in recent years, and have been proposed as an alternative setting for studying (co)inductive reasoning. In particular, now several type systems based on circular reasoning have been proposed. However, little is known about the complexity theoretic aspects of circular proofs, which exhibit sophisticated loop structures atypical of more…
▽ More
Circular (or cyclic) proofs have received increasing attention in recent years, and have been proposed as an alternative setting for studying (co)inductive reasoning. In particular, now several type systems based on circular reasoning have been proposed. However, little is known about the complexity theoretic aspects of circular proofs, which exhibit sophisticated loop structures atypical of more common `recursion schemes'. This paper attempts to bridge the gap between circular proofs and implicit computational complexity (ICC). Namely we introduce a circular proof system based on Bellantoni and Cook's famous safe-normal function algebra, and we identify proof theoretical constraints, inspired by ICC, to characterise the polynomial-time and elementary computable functions. Along the way we introduce new recursion theoretic implicit characterisations of these classes that may be of interest in their own right.
△ Less
Submitted 27 May, 2024; v1 submitted 3 October, 2021;
originally announced October 2021.
-
Linear Additives
Authors:
Gianluca Curzi
Abstract:
We introduce LAM, a subsystem of IMALL2 with restricted additive rules able to manage duplication linearly, called linear additive rules. LAM is presented as the type assignment system for a calculus endowed with copy constructors, which deal with substitution in a linear fashion. As opposed to the standard additive rules, the linear additive rules do not affect the complexity of term reduction: t…
▽ More
We introduce LAM, a subsystem of IMALL2 with restricted additive rules able to manage duplication linearly, called linear additive rules. LAM is presented as the type assignment system for a calculus endowed with copy constructors, which deal with substitution in a linear fashion. As opposed to the standard additive rules, the linear additive rules do not affect the complexity of term reduction: typable terms of LAM enjoy linear strong normalization. Moreover, a mildly weakened version of cut-elimination for this system is proven which takes a cubic number of steps. Finally, we define a sound translation from proofs of LAM into linear lambda terms of IMLL2, and we study its complexity.
△ Less
Submitted 30 December, 2021; v1 submitted 28 April, 2021;
originally announced April 2021.
-
Probabilistic Soft Type Assignment
Authors:
Gianluca Curzi,
Luca Roversi
Abstract:
We model randomized complexity classes in the style of Implicit Computational Complexity. We introduce PSTA, a probabilistic version of STA, the type-theoretical counterpart of Soft Linear Logic. PSTA is a type assignment for an extension of Simpson's Linear Lambda Calculus and its surface reduction, where Linear additives express random choice. Linear additives are weaker than the usual ones; the…
▽ More
We model randomized complexity classes in the style of Implicit Computational Complexity. We introduce PSTA, a probabilistic version of STA, the type-theoretical counterpart of Soft Linear Logic. PSTA is a type assignment for an extension of Simpson's Linear Lambda Calculus and its surface reduction, where Linear additives express random choice. Linear additives are weaker than the usual ones; they allow for duplications harmlessly affecting the computational cost of normalization. PSTA is sound and complete w.r.t. probabilistic polynomial time functions and characterizes the probabilistic complexity classes PP and BPP, the latter slightly less implicitly than PP.
△ Less
Submitted 3 July, 2020;
originally announced July 2020.
-
The Benefit of Being Non-Lazy in Probabilistic λ-calculus
Authors:
Gianluca Curzi,
Michele Pagani
Abstract:
We consider the probabilistic applicative bisimilarity (PAB), a coinductive relation comparing the applicative behaviour of probabilistic untyped lambda terms according to a specific operational semantics. This notion has been studied with respect to the two standard parameter passing policies, call-by-value (cbv) and call-by-name (cbn), using a lazy reduction strategy not reducing within the body…
▽ More
We consider the probabilistic applicative bisimilarity (PAB), a coinductive relation comparing the applicative behaviour of probabilistic untyped lambda terms according to a specific operational semantics. This notion has been studied with respect to the two standard parameter passing policies, call-by-value (cbv) and call-by-name (cbn), using a lazy reduction strategy not reducing within the body of a function. In particular, PAB has been proven to be fully abstract with respect to the contextual equivalence in cbv but not in lazy cbn. We overcome this issue of cbn by relaxing the laziness constraint: we prove that PAB is fully abstract with respect to the standard head reduction contextual equivalence. Our proof is based on the Leventis Separation Theorem, using probabilistic Nakajima trees as a tree-like representation of the contextual equivalence classes. Finally, we prove also that the inequality full abstraction fails, showing that the probabilistic applicative similarity is strictly contained in the contextual preorder.
△ Less
Submitted 27 April, 2020;
originally announced April 2020.
-
A type-assignment of linear erasure and duplication
Authors:
Gianluca Curzi,
Luca Roversi
Abstract:
We introduce $\mathsf{LEM}$, a type-assignment system for the linear $ λ$-calculus that extends second-order $\mathsf{IMLL}_2$, i.e., intuitionistic multiplicative Linear Logic, by means of logical rules that weaken and contract assumptions, but in a purely linear setting. $\mathsf{LEM}$ enjoys both a mildly weakened cut-elimination, whose computational cost is cubic, and Subject reduction. A tran…
▽ More
We introduce $\mathsf{LEM}$, a type-assignment system for the linear $ λ$-calculus that extends second-order $\mathsf{IMLL}_2$, i.e., intuitionistic multiplicative Linear Logic, by means of logical rules that weaken and contract assumptions, but in a purely linear setting. $\mathsf{LEM}$ enjoys both a mildly weakened cut-elimination, whose computational cost is cubic, and Subject reduction. A translation of $\mathsf{LEM}$ into $\mathsf{IMLL}_2$ exists such that the derivations of the former can exponentially compress the dimension of the derivations in the latter. $\mathsf{LEM}$ allows for a modular and compact representation of boolean circuits, directly encoding the fan-out nodes, by contraction, and disposing garbage, by weakening. It can also represent natural numbers with terms very close to standard Church numerals which, moreover, apply to Hereditarily Finite Permutations, i.e. a group structure that exists inside the linear $ λ$-calculus.
△ Less
Submitted 13 May, 2020; v1 submitted 30 December, 2019;
originally announced December 2019.
