-
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.
-
On Propositional Dynamic Logic and Concurrency
Authors:
Matteo Acclavio,
Fabrizio Montesi,
Marco Peressotti
Abstract:
Dynamic logic in the setting of concurrency has proved problematic because of the challenge of capturing interleaving. This challenge stems from the fact that the operational semantics for programs considered in these logics is tailored on trace reasoning for sequential programs. In this work, we generalise propositional dynamic logic (PDL) to a logic framework we call operational propositional dy…
▽ More
Dynamic logic in the setting of concurrency has proved problematic because of the challenge of capturing interleaving. This challenge stems from the fact that the operational semantics for programs considered in these logics is tailored on trace reasoning for sequential programs. In this work, we generalise propositional dynamic logic (PDL) to a logic framework we call operational propositional dynamic logic (OPDL) in which we are able to reason on sets of programs provided with arbitrary operational semantics. We prove cut-elimination and adequacy of a sequent calculus for PDL and we extend these results to OPDL. We conclude by discussing OPDL for Milner's CCS and Choreographic Programming.
△ Less
Submitted 27 March, 2024;
originally announced March 2024.
-
Logic Programming with Multiplicative Structures
Authors:
Matteo Acclavio,
Roberto Maieli
Abstract:
In the logic programming paradigm, a program is defined by a set of methods, each of which can be executed when specific conditions are met during the current state of an execution. The semantics of these programs can be elegantly represented using sequent calculi, in which each method is linked to an inference rule. In this context, proof search mirrors the program's execution. Previous works int…
▽ More
In the logic programming paradigm, a program is defined by a set of methods, each of which can be executed when specific conditions are met during the current state of an execution. The semantics of these programs can be elegantly represented using sequent calculi, in which each method is linked to an inference rule. In this context, proof search mirrors the program's execution. Previous works introduced a framework in which the process of constructing proof nets is employed to model executions, as opposed to the traditional approach of proof search in sequent calculus.
This paper further extends this investigation by focussing on the pure multiplicative fragment of this framework. We demonstrate, providing practical examples, the capability to define logic programming methods with context-sensitive behaviors solely through specific resource-preserving and context-free operations, corresponding to certain generalized multiplicative connectives explored in existing literature. We show how some of these methods, although still multiplicative, escape the purely multiplicative fragment of Linear Logic (MLL).
△ Less
Submitted 5 March, 2024;
originally announced March 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.
-
Graphical Proof Theory I: Sequent Systems on Undirected Graphs
Authors:
Matteo Acclavio
Abstract:
In this paper we explore the design of sequent calculi operating on graphs. For this purpose, we introduce a set of logical connectives allowing us to extend the correspondence between cographs and classical propositional formulas to any graph. We then provide sequent calculi operating on these formulas, we prove cut-elimination and that formula encoding the same graph are logically equivalent. We…
▽ More
In this paper we explore the design of sequent calculi operating on graphs. For this purpose, we introduce a set of logical connectives allowing us to extend the correspondence between cographs and classical propositional formulas to any graph. We then provide sequent calculi operating on these formulas, we prove cut-elimination and that formula encoding the same graph are logically equivalent. We show that these systems provide conservative extensions of multiplicative linear logic (with and without mix) and classical propositional logic. We conclude by showing that one of these systems is equivalent to the graphical logic GS defined via a system of context-free graph rewiring rules, therefore providing an alternative proof of analyticity for this logic over graphs.
△ Less
Submitted 12 February, 2024; v1 submitted 22 May, 2023;
originally announced May 2023.
-
Canonicity of Proofs in Constructive Modal Logic
Authors:
Matteo Acclavio,
Davide Catta,
Federico Olimpieri
Abstract:
In this paper we investigate the Curry-Howard correspondence for constructive modal logic in light of the gap between the proof equivalences enforced by the lambda calculi from the literature and by the recently defined winning strategies for this logic. We define a new lambda-calculus for a minimal constructive modal logic by enriching the calculus from the literature with additional reduction ru…
▽ More
In this paper we investigate the Curry-Howard correspondence for constructive modal logic in light of the gap between the proof equivalences enforced by the lambda calculi from the literature and by the recently defined winning strategies for this logic. We define a new lambda-calculus for a minimal constructive modal logic by enriching the calculus from the literature with additional reduction rules and we prove normalization and confluence for our calculus. We then provide a ty** system in the style of focused proof systems allowing us to provide a unique proof for each term in normal form, and we use this result to show a one-to-one correspondence between terms in normal form and winning innocent strategies.
△ Less
Submitted 30 July, 2023; v1 submitted 11 April, 2023;
originally announced April 2023.
-
A Deep Inference System for Differential Linear Logic
Authors:
Matteo Acclavio,
Giulio Guerrieri
Abstract:
Differential linear logic (DiLL) provides a fine analysis of resource consumption in cut-elimination. We investigate the subsystem of DiLL without promotion in a deep inference formalism, where cuts are at an atomic level. In our system every provable formula admits a derivation in normal form, via a normalization procedure that commutes with the translation from sequent calculus to deep inferenc…
▽ More
Differential linear logic (DiLL) provides a fine analysis of resource consumption in cut-elimination. We investigate the subsystem of DiLL without promotion in a deep inference formalism, where cuts are at an atomic level. In our system every provable formula admits a derivation in normal form, via a normalization procedure that commutes with the translation from sequent calculus to deep inference.
△ Less
Submitted 30 December, 2021;
originally announced December 2021.
-
Exponentially Handsome Proof Nets and Their Normalization
Authors:
Matteo Acclavio
Abstract:
Handsome proof nets were introduced by Retoré as a syntax for multiplicative linear logic. These proof nets are defined by means of cographs (graphs representing formulas) equipped with a vertices partition satisfying simple topological conditions. In this paper we extend this syntax to multiplicative linear logic with units and exponentials. For this purpose we develop a new sound and complete…
▽ More
Handsome proof nets were introduced by Retoré as a syntax for multiplicative linear logic. These proof nets are defined by means of cographs (graphs representing formulas) equipped with a vertices partition satisfying simple topological conditions. In this paper we extend this syntax to multiplicative linear logic with units and exponentials. For this purpose we develop a new sound and complete sequent system for the logic, enforcing a stronger notion of proof equivalence with respect to the one usually considered in the literature. We then define combinatorial proofs, a graphical proof system able to capture syntactically the proof equivalence, for the cut-free fragment of the calculus. We conclude the paper by defining the exponentially handsome proof nets as combinatorial proofs with cuts and defining an internal normalization procedure for this syntax.
△ Less
Submitted 30 December, 2021;
originally announced December 2021.
-
Towards a Denotational Semantics for Proofs in Constructive Modal Logic
Authors:
Matteo Acclavio,
Davide Catta,
Lutz Straßburger
Abstract:
In this paper we provide two new semantics for proofs in the constructive modal logics CK and CD. The first semantics is given by extending the syntax of combinatorial proofs for propositional intuitionistic logic, in which proofs are factorised in a linear fragment (arena net) and a parallel weakening-contraction fragment (skew fibration). In particular we provide an encoding of modal formulas by…
▽ More
In this paper we provide two new semantics for proofs in the constructive modal logics CK and CD. The first semantics is given by extending the syntax of combinatorial proofs for propositional intuitionistic logic, in which proofs are factorised in a linear fragment (arena net) and a parallel weakening-contraction fragment (skew fibration). In particular we provide an encoding of modal formulas by means of directed graphs (modal arenas), and an encoding of linear proofs as modal arenas equipped with vertex partitions satisfying topological criteria. The second semantics is given by means of winning innocent strategies of a two-player game over modal arenas. This is given by extending the Heijltjes-Hughes-Straßburger correspondence between intuitionistic combinatorial proofs and winning innocent strategies in a Hyland-Ong arena. Using our first result, we provide a characterisation of winning strategies for games on a modal arena corresponding to proofs with modalities.
△ Less
Submitted 19 April, 2021;
originally announced April 2021.
-
An Analytic Propositional Proof System on Graphs
Authors:
Matteo Acclavio,
Ross Horne,
Lutz Straßburger
Abstract:
In this paper we present a proof system that operates on graphs instead of formulas. Starting from the well-known relationship between formulas and cographs, we drop the cograph-conditions and look at arbitrary undirected) graphs. This means that we lose the tree structure of the formulas corresponding to the cographs, and we can no longer use standard proof theoretical methods that depend on that…
▽ More
In this paper we present a proof system that operates on graphs instead of formulas. Starting from the well-known relationship between formulas and cographs, we drop the cograph-conditions and look at arbitrary undirected) graphs. This means that we lose the tree structure of the formulas corresponding to the cographs, and we can no longer use standard proof theoretical methods that depend on that tree structure. In order to overcome this difficulty, we use a modular decomposition of graphs and some techniques from deep inference where inference rules do not rely on the main connective of a formula. For our proof system we show the admissibility of cut and a generalisation of the splitting property. Finally, we show that our system is a conservative extension of multiplicative linear logic with mix, and we argue that our graphs form a notion of generalised connective.
△ Less
Submitted 20 October, 2022; v1 submitted 2 December, 2020;
originally announced December 2020.
-
Proof Diagrams for Multiplicative Linear Logic: Syntax and Semantics
Authors:
Matteo Acclavio
Abstract:
Proof nets are a syntax for linear logic proofs which gives a coarser notion of proof equivalence with respect to syntactic equality together with an intuitive geometrical representation of proofs.
In this paper we give an alternative $2$-dimensional syntax for multiplicative linear logic derivations. The syntax of string diagrams authorizes the definition of a framework where the sequentializab…
▽ More
Proof nets are a syntax for linear logic proofs which gives a coarser notion of proof equivalence with respect to syntactic equality together with an intuitive geometrical representation of proofs.
In this paper we give an alternative $2$-dimensional syntax for multiplicative linear logic derivations. The syntax of string diagrams authorizes the definition of a framework where the sequentializability of a term, i.e. deciding whether the term corresponds to a correct derivation, can be verified in linear time.
Furthermore, we can use this syntax to define a denotational semantics for multiplicative linear logic with units by means of equivalence classes of proof diagrams modulo a terminating rewriting.
△ Less
Submitted 1 February, 2017;
originally announced February 2017.
-
Proof Diagrams for Multiplicative Linear Logic
Authors:
Matteo Acclavio
Abstract:
The original idea of proof nets can be formulated by means of interaction nets syntax. Additional machinery as switching, jumps and graph connectivity is needed in order to ensure correspondence between a proof structure and a correct proof in sequent calculus.
In this paper we give an interpretation of proof nets in the syntax of string diagrams. Even though we lose standard proof equivalence,…
▽ More
The original idea of proof nets can be formulated by means of interaction nets syntax. Additional machinery as switching, jumps and graph connectivity is needed in order to ensure correspondence between a proof structure and a correct proof in sequent calculus.
In this paper we give an interpretation of proof nets in the syntax of string diagrams. Even though we lose standard proof equivalence, our construction allows to define a framework where soundness and well-typeness of a diagram can be verified in linear time.
△ Less
Submitted 17 January, 2017; v1 submitted 29 June, 2016;
originally announced June 2016.
