| 1. |
- Curzi, Gianluca, 1991, et al.
(författare)
-
A type-assignment of linear erasure and duplication
- 2020
-
Ingår i: Theoretical Computer Science. - 0304-3975.
-
Tidskriftsartikel (refereegranskat)abstract
- We introduce ???, a type-assignment system for the linear λ-calculus that extends second-order ????2, i.e., intuitionistic multiplicative Linear Logic, by means of logical rules that weaken and contract assumptions, but in a purely linear setting. ??? enjoys both a mildly weakened cut-elimination, whose computational cost is cubic, and Subject reduction. A translation of ??? into ????2 exists such that the derivations of the former can exponentially compress the dimension of the derivations in the latter. ??? 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.
|
|
| 2. |
- Curzi, Gianluca, 1991, et al.
(författare)
-
Computational expressivity of (circular) proofs with fixed points
- 2023
-
Ingår i: LICS.
-
Konferensbidrag (refereegranskat)abstract
- We study the computational expressivity of proof systems with fixed point operators, within the ‘proofs-as-programs’ paradigm. We start with a calculus μLJ (due to Clairambault) that extends intuitionistic logic by least and greatest positive fixed points. Based in the sequent calculus, μLJ admits a standard extension to a ‘circular’ calculus CμLJ.Our main result is that, perhaps surprisingly, both μLJ and CμLJ represent the same first-order functions: those provably total in Π12−CA0, 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 Π12−CA0 (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 Π12−CA0 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.
|
|
| 3. |
- Curzi, Gianluca, 1991, et al.
(författare)
-
Cyclic Implicit Complexity
- 2022
-
Ingår i: LICS.
-
Konferensbidrag (refereegranskat)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 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.
|
|
| 4. |
- Curzi, Gianluca, 1991
(författare)
-
Linear Additives
- 2021
-
Ingår i: Electronic Proceedings in Theoretical Computer Science (EPTCS). - 2075-2180.
-
Tidskriftsartikel (refereegranskat)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: 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 LAM’s proofs into IMLL2’s linear lambda terms, and we study its complexity.
|
|
| 5. |
- Curzi, Gianluca, 1991, et al.
(författare)
-
Non-Uniform Complexity via Non-Wellfounded Proofs
- 2023
-
Ingår i: CSL.
-
Konferensbidrag (refereegranskat)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 enjoys excellent metalogical properties. In recent work, we showed how the cyclic proof setting can be further employed to model com- putational 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 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 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.
|
|
| 6. |
- Curzi, Gianluca, 1991, et al.
(författare)
-
The Benefit of Being Non-Lazy in Probabilistic λ-calculus: Applicative Bisimulation is Fully Abstract for Non-Lazy Probabilistic Call-by-Name
- 2020
-
Ingår i: LICS.
-
Konferensbidrag (refereegranskat)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 by Dal Lago et al. 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 context 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 context equivalence. Our proof is based on Leventis Separation Theorem, using probabilistic Nakajima trees as a tree-like representation of the context equivalence classes. Finally, we prove also that the inequality full abstraction fails, showing that the probabilistic applicative similarity is strictly contained in the context preorder.
|
|
| 7. |
- Curzi, Gianluca, 1991, et al.
(författare)
-
Trust Evidence Logic
- 2021
-
Ingår i: ECSQARU.
-
Konferensbidrag (refereegranskat)abstract
- We investigate the application of a modal language à la Hennessy-Milner to the specific domain of evidence-based trust estimations. In particular, we refer to a context-aware notion of computational trust joining in a quantitative setting both assessment of subjective opinions and third-party recommendations. Moreover, for a comprehensive analysis of the proposed logics, we offer an axiomatization and provide soundness and completeness results.
|
|
