These are the notes for the reading group on proof-nets in linear logic, spanning April 8 and 15 of the logic seminar at the University of Melbourne. The aim is to:
- April 8 (handout): understand the definition of proof-nets and their cut-elimination procedure, and see the statement of the two main theorems in the theory: the Sequentialisation Theorem (which identifies those proof-nets coming from sequent calculus proofs) and the Strong Normalisation Theorem.
- April 15 (handout): work through details of the proof that in stratified linear logic, cut-elimination is achieved in polynomial time (Theorem 16 of Baillot and Mazza’s “Linear logic by levels”) as stated in my previous talk without details.
The main references are:
Here is a rough plan that makes sense to me, for the first seminar:
- General background on linear logic ([J91] Sections 0, 1, 3 and then [BM09] Section 1). Ideally we all would have skimmed this before Friday, to refresh our memories.
- Definition of proof-nets up to the definition of depth ([BM09] from p.8 to p.10).
- Some examples of proof-nets (Church numerals from [G87] Section 5.3.2 p. 86 and binary integers from p.26 of [BM09]).
- Definition of cut-elimination transformations and statement of Strong Normalisation Theorem ([BM09] p.12, p.13 and [PTF09]). This was proven in [G87] for a subsystem but only recently in [PTF09] for full linear logic.
- Sequentialisation of sequent calculus proofs to proof-nets ([BM09] p.11).
- Examples of proof-nets that are not sequentialisable, and proof-nets that are the sequentialisation of multiple sequent calculus proofs; discussion of the advantages of proof-nets vs sequent calculus ([J91] p.140, p.156, p.157).
- More complicated examples, with duplication of nested boxes.
- Definition of switchings and statement of the Sequentialisation Theorem (very brief statement in [BM09] Proposition 2, details from [G96], examples from [J91] Section 6).
- If there is any time remaining, some details of the proof of the Sequentialisation Theorem from [G96].
The canonical reference for proof-nets and the Sequentialisation Theorem is Girard [G96], but in order to have notational consistency with the second seminar on light linear logic, and to see an overview free of complicating details, I think [BM09] is a better starting point for us. This means we would view [G96], [J91], [PTF09] as augmenting references for the real details (which are completely absent from [BM09]).
A rough plan for the second seminar, which will be taken almost entirely from [BM09].
- A brief recall of the relation between stratification and complexity from my earlier talk (slides and screencast).
- A brief recall of proof-nets and their cut-elimination steps from last time.
- The definition of stratified proof-nets (mL3 in Baillot-Mazza) from Section 2.1 of [BM09].
- Then Section 3 of [BM09] in its entirety, which has three parts (A) weak normalisation for cut-elimination in untyped stratified proof-nets (Proposition 13) (B) the characterisation of elementary time by stratification (Theorem 16) © the characterisation of polynomial time by stratification (Theorem 23).