Normalisation on a geometric representation of a proof
Overview of the ProjectThe following fundamental question, which we call the `proof identity´ question, is still open:
When are two mathematical proofs the same?
This question has been first formulated by Hilbert, who considered including it in his famous list of open problems. In fact, this problem is often called `Hilbert's 24th problem´. Given the progress we made in the past five years, we expect to find a solution to the proof identity problem in the two years of this project. The tools and techniques that we have to develop will allow a significant advance of the whole field of proof theory, with several applications in computer science.
We need to be able to answer the proof identity question according to several possible criteria by which proofs can be considered the same. This means developing an adequate proof theory, i.e., a formalism in which to express proofs and techniques to manipulate them, called normalisation procedures. The formalism should allow the expression of proofs free of so-called `syntactic bureaucracy´, which arises from the seemingly unavoidable tension between the meaning of a proof and its syntactic formalisation. Proof identity is then defined through normalisation, viz., by transforming a given proof into a standard, bureaucracy-free form, suitable for comparison.
Traditional proof theory does not yield an adequate technology for proof identity, because its formalisms are intrinsically bureaucratic and because it lacks normalisation methods that respect some of the most fundamental properties of proofs, like their size. The purpose of this project is to design the first bureaucracy-free formalism, endowed with an array of novel normalisation notions and techniques, which respect the basic properties of proofs. This will give us the first non-trivial and convincing solution to the proof identity problem.
The main ideas employed in this project are:
The geometry of proofs is made accessible by a relatively new methodology in proof theory, which Guglielmi pioneered, called `deep inference´. Proofs in deep inference are composed of elementary parts whose size is bounded by a constant. This cannot be achieved in more traditional proof theory, and it is the crucial technical advance that allows us to treat proofs as geometric objects.
Value of this project: 750,448 EUR.
PeopleFinanced by Démosthène at LORIA–INRIA-Nancy Grand Est:
Main collaborators:
Related ProjectsREDO: Redesigning Logical SyntaxINRIA—Action de Recherche Collaborative. Two-year project of the teams Calligramme/Démosthène and Parsifal (INRIA) and the Computer Science Department of the University of Bath. The project gets 80,000 EUR. Principal investigators are Alessio Guglielmi, François Lamarche and Lutz Straßburger (coordinator).
INFER: Theory and Application of Deep InferenceANR—Programme Blanc 2006. Three-year project at LIX, LORIA and PPS. The project gets 230,400 EUR (out of a total cost of 1,280,598 EUR) from the Agence Nationale de la Recherche. Coordinator and principal investigator is Lutz Straßburger, other principal investigators are François Lamarche and Michel Parigot.
PapersFormalism B is the provisory name of the bureaucracy-free formalism that we propose as a solution to the proof identity problem. Formalism B is based on
The formalism is going to be checked for moral and technical compatibility with categorical structures and categorical proof theory, in collaboration with Yves Guiraud and François Lamarche.
Formalism B
Alessio Guglielmi, Tom Gundersen and Michel Parigot
Very provisory title, in preparation
On the Length of Medial-Switch-Mix Derivations
Paola Bruscoli, Alessio Guglielmi and Lutz Straßburger
Provisory title, in preparation (Tom Gundersen will probably join)
A General View of Normalisation Through Atomic Flows
Tom Gundersen
AbstractAtomic flows are a geometric invariant of classical propositional proofs in deep inference. In this thesis we use atomic flows to describe new normal forms of proofs, of which the traditional normal forms are special cases, we also give several normalisation procedures for obtaining the normal forms. We define, and use to present our results, a new deep-inference formalism called the functorial calculus, which is more flexible than the traditional calculus of structures. To our surprise we are able to 1) normalise proofs without looking at their logical connectives or logical rules; and 2) normalise proofs in less than exponential time.
Pdf12 August 2010
PhD thesis, defended on 10 November 2009
A System of Interaction and Structure IV: The Exponentials and Decomposition
Lutz Straßburger and Alessio Guglielmi
AbstractWe study a system, called NEL, which is the mixed commutative/non-commutative linear logic BV augmented with linear logic’s exponentials. Equivalently, NEL is MELL augmented with the non-commutative self-dual connective seq. In this paper, we show a basic compositionality property of NEL, which we call decomposition. This result leads to a cut-elimination theorem, which is proved in the next paper of this series. To control the induction measure for the theorem, we rely on a novel technique that extracts from NEL proofs the structure of exponentials, into what we call !-?-Flow-Graphs.
Pdf27 July 2010
To appear on ACM Transactions on Computational Logic
A Quasipolynomial Cut-Elimination Procedure in Deep Inference via Atomic Flows and Threshold Formulae
Paola Bruscoli, Alessio Guglielmi, Tom Gundersen and Michel Parigot
AbstractJeřábek showed in 2008 that cuts in propositional-logic deep-inference proofs can be eliminated in quasipolynomial time. The proof is an indirect one relying on a result of Atserias, Galesi and Pudlák about monotone sequent calculus and a correspondence between this system and cut-free deep-inference proofs. In this paper we give a direct proof of Jeřábek's result: we give a quasipolynomial-time cut-elimination procedure in propositional-logic deep inference. The main new ingredient is the use of a computational trace of deep-inference proofs called atomic flows, which are both very simple (they trace only structural rules and forget logical rules) and strong enough to faithfully represent the cut-elimination procedure.
25 June 201025 January 2010A Logical Basis for Quantum Evolution and Entanglement
Richard F. Blute, Alessio Guglielmi, Ivan T. Ivanov, Prakash Panangaden and Lutz Straßburger
AbstractThe discrete quantum casual dynamics of Blute-Ivanov-Panangaden is reconsidered and recast in terms of categorical logic. In that first paper, quantum systems are viewed as discrete structures, namely directed acyclic graphs. In such a graph, events are considered as vertices and edges depict propagation between events. Evolution is described as happening between a special family of spacelike slices, which were referred to as locative slices. Such slices are not so large as to result in acausal influences, but large enough to capture nonlocal correlations.
Edges are assigned logical formulas in a special logical system, called BV, an instance of a deep inference system. Vertices are considered as logical entailments. Evolution is described by the application of the logical cut rule to these entailments.
We demonstrate that BV, with its mix of commutative and noncommutative connectives, is precisely the right logic for such analysis. We show that the commutative tensor encodes (possible) entanglement, and the noncommutative seq encodes causal precedence. With this interpretation, the locative slices are precisely the derivable strings of formulas. Furthermore, using traditional ideas from categorical logic, one can assign a semantics using for example Hilbert spaces and the interpretation becomes the standard interpretation of dynamics in the original discrete quantum casual dynamics. A more faithful interpretation (making use of the distinct connectives of BV) can be made using Girard’s quantum coherence spaces.
19 May 2010
Submitted
Breaking Paths in Atomic Flows for Classical Logic
Alessio Guglielmi and Tom Gundersen and Lutz Straßburger
AbstractThis work belongs to a wider effort aimed at eliminating syntactic bureaucracy from proof systems. In this paper, we present a novel cut elimination procedure for classical propositional logic. It is based on the recently introduced atomic flows: they are purely graphical devices that abstract away from much of the typical bureaucracy of proofs. We make crucial use of the path breaker, an atomic-flow construction that avoids some nasty termination problems, and that can be used in any proof system with sufficient symmetry. This paper contains an original 2-dimensional-diagram exposition of atomic flows, which helps us to connect atomic flows with other known formalisms.
Pdf20 April 2010
Accepted by LICS 2010
A Proof Calculus Which Reduces Syntactic Bureaucracy
Alessio Guglielmi, Tom Gundersen and Michel Parigot
AbstractIn usual proof systems, like sequent calculus, only a very limited way of combining proofs is available through the tree structure. We present in this paper a logic-independent proof calculus, where proofs can be freely composed by connectives, and prove its basic properties. The main advantage of this proof calculus is that it allows to avoid certain types of syntactic bureaucracy inherent to all usual proof systems, in particular sequent calculus. Proofs in this system closely reflect their atomic flow, which traces the behaviour of atoms through structural rules. The general definition is illustrated by the standard deep-inference system for propositional logic, for which there are known rewriting techniques that achieve cut elimination based only on the information in atomic flows.
Pdf12 April 2010
RTA 2010, Leibniz International Proceedings in Informatics (LIPIcs) 6, pp. 135–150
Two Denotational Interpretations of Proofs in Classical Logic
François Lamarche and Novak Novakovic
AbstractIn this paper we present and compare two interpretations of classical logic proofs in a category of posets and relations, and relate their behavior to proof nets, extracting meaningful invariants of proofs. We show that at least one of these interpretation cannot have anything to do with the Curry-Howard correspondence.
Presented at the workshop Structures and Deduction 2009
On the Proof Complexity of Deep Inference
Paola Bruscoli and Alessio Guglielmi
AbstractWe obtain two results about the proof complexity of deep inference: 1) deep-inference proof systems are as powerful as Frege ones, even when both are extended with the Tseitin extension rule or with the substitution rule; 2) there are analytic deep-inference proof systems that exhibit an exponential speed-up over analytic Gentzen proof systems that they polynomially simulate.
Pdf19 April 2009
ACM Transactions on Computational Logic 10 (2:14) 2009, pp. 1–34
A System of Interaction and Structure V: The Exponentials and Splitting
Alessio Guglielmi and Lutz Straßburger
AbstractSystem NEL is the mixed commutative/non-commutative linear logic BV augmented with linear logic’s exponentials, or, equivalently, it is MELL augmented with the non-commutative self-dual connective seq. System NEL is Turing-complete, it is able to directly express process algebra sequential composition and it faithfully models causal quantum evolution. In this paper, we show cut elimination for NEL, based on a property that we call splitting. NEL is presented in the calculus of structures, which is a deep-inference formalism, because no Gentzen formalism can express it analytically. The splitting theorem shows how and to what extent we can recover a sequent-like structure in NEL proofs. Together with the decomposition theorem, proved in the previous paper of the series, this immediately leads to a cut-elimination theorem for NEL.
Pdf29 March 2009
Submitted to Mathematical Structures in Computer Science
Activity3–6.11.08AG and TG (from Bath) visit LIX, AG talks about Proof Identity, Proof Complexity and Deep Inference.
6–10.11.08TG (from Bath) visits LORIA to work on the paper Normalisation Control in Deep Inference Via Atomic Flows II.
19–21.11.08AG is invited speaker at Workshop—Structural Proof Theory, Université Paris 7 (Group PPS), and talks about Quasipolynomial Normalisation.
20–21.11.08TG (from Bath) participates in the Workshop—Structural Proof Theory, Université Paris 7 (Group PPS), and talks about Normalisation in Deep Inference.
1–6.12.08TG (from Bath) visits LORIA to work on the paper Normalisation Control in Deep Inference Via Atomic Flows II.
7–8.12.08MP visits LORIA to work on the paper Formalism B.
1.1.2009TG moves from Bath and joins us at LORIA to work at his PhD thesis and several papers.
9–14.3.09LS visits LORIA to work on the papers A System of Interaction and Structure IV: The Exponentials and Decomposition and A System of Interaction and Structure V: The Exponentials and Splitting.
24.3.09PB visits the Department of Computer Science of the University of Bath for a scientific exchange.
26.3.09AG talks at the Calligramme, Pareo, Types and Talaris teams of LORIA about Introduction to Deep Inference.
23.4.09AG talks at the Calligramme, Pareo, Types and Talaris teams of LORIA about Normalisation via Atomic Flows.
4.5.09AG talks at the Project Committee of LORIA about A Geometric Representation of Proofs for Proof Identity and Proof Complexity via Deep Inference.
26–28.5.09FL participates in the workshop REDO: Redesigning Logical Syntax at LIX and talks about proof nets.
26–29.5.09AG participates in the workshop REDO: Redesigning Logical Syntax at LIX and gives a Tutorial on Deep Inference.
26–29.5.09TG participates in the workshop REDO: Redesigning Logical Syntax at LIX and talks about atomic flows.
18–28.06.09FL visits the Department of Mathematics at McGill University and gives the invited talk A New Homotopy-Theoretic Interpretation of Martin-Löf's Identity Type at the conference Models, Logics and Higher-Dimensional Categories, A Tribute to the Work of Mihaly Makkai at the Centre de Recherches Mathématiques, Université de Montréal.
23–24.6.09MP visits LORIA to work on the paper Formalism B.
1–3.7.09Bruno Woltzenlogel Paleo visits LORIA and gives the talk Clause Sets and Projections for Cut-Elimination in Sequent-Calculi (he joins LORIA in December 2009).
6.7.09AG is invited speaker at the Tableaux 2009 workshop Gentzen Systems and Beyond, Oslo, and talks about Beyond.
13–14.7.09MP visits LORIA to work on the paper Formalism B.
20–24.7.09FL is invited speaker at the ESSLLI workshop Structures and Deduction 2009, Bordeaux, and talks about An Interesting Link Between Type Theory and Topology.
1.10–30.11.09TG is funded by Démosthène to write papers out of his thesis.
3-4.11.09AG is invited by and participates in the INRIA Colloquium in Paris.
9-12.11.09FL visits the Department of Computer Science of the University of Bath and acts as an examiner in TG's PhD thesis committee.
9-12.11.09AG and TG visit the Department of Computer Science of the University of Bath and give the talk Some News on the Proof Complexity of Deep Inference.
10.11TG successfully defends his PhD thesis A General View of Normalisation Through Atomic Flows at the University of Bath.
16–18.11.09PB, AG, YG, TG, FL, NN, MP and LS participate in the workshop REDO: Redesigning Logical Syntax at LORIA and AG gives the talk Formalism B and NN gives the talk Classical Logic and Frobenius Algebras.
1.12.09TG joins LIX—INRIA Saclay–Île-de-France as a post-doc in the project REDO: Redesigning Logical Syntax.
19.1.10AG visits the Department of Computer Science of the University of Pisa and gives the talk Ten Years of Deep Inference.
20.1.10AG visits the Department of Computer Science of the University of Bologna and gives the talk Normalisation with Atomic Flows.
21.1.10AG visits the Department of Computer Science of the University of Torino and gives the talk Normalisation with Atomic Flows.
2.2.10MP participates in the workshop Collegium Logicum: Proofs and Structure in Wien and talks about Formalisms for Deep Inference.
2.2.10AG participates in the workshop Collegium Logicum: Proofs and Structure in Wien and talks about Normalisation with Atomic Flows.
2.2.10TG participates in the workshop Collegium Logicum: Proofs and Structure in Wien and talks about A Quasipolynomial Cut-Elimination Procedure in Deep Inference via Atomic Flows and Threshold Formulae.
2.2.10LS participates in the workshop Collegium Logicum: Proofs and Structure in Wien and talks about Proof Nets as Invariants for Proofs.
AG, FL, LS, MP, NN, PB and TG participate in the workshop Geometric and Logic Approaches to Computation in Nancy, organised within this project.15–17.3.10FL participates in the workshop Journées GEOCAL–LAC in Nice and talks about Le Predicat d’Identité de Martin-Löf et l’Espace des Chemins en Homotopie.
15–17.3.10AG participates in the workshop Journées GEOCAL–LAC in Nice and talks about Geometric Normalisation with Atomic Flows.
15–17.3.10TG participates in the workshop Journées GEOCAL–LAC in Nice and talks about Breaking Paths in Atomic flows for Classical Logic.
15–17.3.10LS participates in the workshop Journées GEOCAL–LAC in Nice and talks about Extension Without Cut.
25.4–1.5.10TG participates in the conference LPAR-16 in Dakar and presents the paper A Quasipolynomial Cut-Elimination Procedure in Deep Inference via Atomic Flows and Threshold Formulae.
25.4–1.5.10MP participates in the conference LPAR-16 in Dakar with the invited talk Deep Inference: Why and How?.
27–30.5.10AG visits the Department of Computer Science of the University of Bath and the Department of Computer Science of Swansea University to discuss future projects and collaborations continuing the research of Démosthène.
20–26.6.10FL participates in the conference CT2010 in Genova with the talk Axioms and Models for Concrete Homotopy.
20–26.6.10NN participates in the conference CT2010 in Genova with the talk Classical Logic and Frobenius Algebras.
14–16.9.10PB, AG, TG, FL and LS participate in the workshop REDO: Redesigning Logical Syntax in Bath and FL gives the talk Confluence Criteria for Rewriting on Structures with Non-Trivial Automorphisms.
17–24.9.10PB and AG visit the Department of Computer Science of the University of Bath to collaborate with the locals on future projects.
The final part of NN's PhD is financed by Démosthène. The second part of his thesis deals with a geometric formalism for deep inference.
30.8.2010Alessio Guglielmiemail
