Linear Logic and Noncommutativity in the

Lutz Strassburger

Description

Niveau: Supérieur

• dissertation

Linear Logic and Noncommutativity in the Calculus of Structures Dissertation zur Erlangung des akademischen Grades Doktor rerum naturalium (Dr. rer. nat.) vorgelegt an der Technischen Universitat Dresden Fakultat Informatik eingereicht am 26. Mai 2003 von Diplom-Informatiker Lutz Straßburger geboren am 21. April 1975 in Dresden Betreuer: Dr. Alessio Guglielmi Betreuender Hochschullehrer: Prof. Dr. rer. nat. habil. Ste?en Holldobler Gutachter: Prof. Dr. rer. nat. habil. Ste?en Holldobler Dr. Franc¸ois Lamarche Prof. Dr. rer. nat. habil. Horst Reichel Disputation am 24. Juli 2003

• discussing tex


• dfg-graduierten- kolleg


• made many helpful


• thesis has


• zur erlangung des akademischen grades


• prozesse und

Sujets

• Dissertation
• Jurgensen
• Stewart
• Lipton
• Guglielmi
• Straßburger

Informations

• Publié par: profil-nechor-2012
• Publié le: 01 mai 2003
• Nombre de lectures: 12
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

Linear Logic and Noncommutativity
in the
Calculus of Structures
Dissertation
zur Erlangung des akademischen Grades
Doktor rerum naturalium (Dr. rer. nat.)
vorgelegt an der
Technischen Universit¨ at Dresden
Fakult¨at Informatik
eingereicht am 26. Mai 2003 von
Diplom-Informatiker Lutz Straßburger
geboren am 21. April 1975 in Dresden
Betreuer: Dr. Alessio Guglielmi
Betreuender Hochschullehrer: Prof. Dr. rer. nat. habil. Steffen H¨ olldobler
Gutachter: Prof. Dr. rer. nat. habil. Steffen H¨ olldobler
Dr. Fran¸cois Lamarche
Prof. Dr. rer. nat. habil. Horst Reichel
Disputation am 24. Juli 2003Acknowledgements
Iam particularly indebted to Alessio Guglielmi. Whithout his advice and guidance this
thesis would not have been written. He awoke my interest for thefascinating field of proof
theory and introduced me to the calculus of structures. I benefited from many fruitful and
inspiring discussions with him, and in desperate situations he encouraged me to keep going.
He also provided me with his T Xmacros for typesetting derivations.E
Iamgrateful toSteffen H¨olldobler for accepting the supervision of this thesis and
for providing ideal conditions for doing research. He also made many helpful suggestions
forimproving the readability. I am obliged to Fran¸cois Lamarche and Horst Reichel for
accepting to be referees.
Iwould like to thank Kai Brunnl¨ er, Paola Bruscoli, Charles Stewart, and Alwen Tiu
for many fruitful discussion during the last three years. In particular, I am thankful to Kai
Brunnl¨ er for struggling himself through a preliminary version and making helpful comments.
Jim Lipton and Charles Stewart made valuable suggestions for improving the introduction.
Additionally, I would like to thank Claus Jurg¨ ensen for the fun we had in discussing
T Xmacros. In particular, the (self-explanatory) macro \clap,which is used on almostE
every page, came out of such a discussion.
This thesis would not exist without the support of my wife Jana. During all the time
she has been a continuous source of love and inspiration.
This PhD thesis has been written with the financial support of the DFG-Graduierten-
kolleg 334 “Spezifikation diskreter Prozesse und Prozeßsysteme durch operationelle Modelle
und Logiken”.
iiiivTable of Contents
Acknowledgements iii
Table of Contents v
List of Figures vii
1Introduction 1
1.1Proof Theory andDeclarativeProgramming.. .... ... .... ... .. 1
1.2LinearLogic.... ... ... .... ... ... ... ... .. 5
1.3Noncommutativity ... ... ... ... .... ... .... ... .. 8
1.4The Calculus of Structures . .... ... ... ... ... .. 9
1.5 Summary of Results.. ... ... ... .... ... .... ... .. 12
1.6OverviewofContents. ... .... ... ... ... ... .. 15
2LinearLogic and the Sequent Calculus 17
2.1Formulaeand Sequents . ... .... ... ... .... ... .... ... .. 17
2.2Rules andDerivations . ... ... ... ... ... .. 18
2.3Cut Elimination. ... ... .... ... ... .... ... .... ... .. 22
2.4Discussion . .... ... ... ... ... ... ... .. 24
3LinearLogic and the Calculus of Structures 25
3.1Structuresfor Linear Logic. .... ... ... .... ... .... ... .. 25
3.2Rules andDerivations . ... ... ... ... ... .. 28
3.3Equivalence to theSequent Calculus System.. .... ... .... ... .. 36
3.4Cut Elimination. ... ... .... ... ... ... ... .. 41
3.4.1 Splitting.. ... ... ... ... .... ... .... ... .. 44
3.4.2Context Reduction .. .... ... ... ... ... .. 68
3.4.3Eliminationofthe Up Fragment. ... .... ... .... ... .. 72
3.5Discussion . .... ... ... .... ... ... ... ... .. 80
4TheMultiplicative Exponential Fragment of Linear Logic 83
4.1Sequents, Structures andRules ... ... ... .... ... .... ... .. 83
4.2Permutation of Rules. . ... .... ... ... ... ... .. 86
4.3Decomposition.. ... ... .... ... ... .... ... .... ... .. 96
4.3.1Chainsand Cycles in Derivations. ... ... ... .. 100
4.3.2SeparationofAbsorptionand Weakening ... ... .... ... .. 120
4.4Cut Elimination. ... ... .... ... ... .... ... ... .. 129
4.5Interpolation ... ... ... ... ... ... .... ... .. 139
vvi Table of Contents
4.6Discussion .. ... .... ... .... ... ... .... ... .... ... . 141
5ALocalSystemfor Linear Logic 143
5.1Localityvia Atomicity. . ... .... ... ... .... ... .... ... . 143
5.2Rules andCut Elimination.. .... ... ... .... ... .... ... . 145
5.3Decomposition.. .... ... ... ... ... ... . 151
5.3.1SeparationofAtomicContraction . ... .... ... .... ... . 152
5.3.2SeparationofAtomicInteraction .. ... ... ... . 160
5.3.3LazySeparationofThinning . ... ... .... ... .... ... . 167
5.3.4EagerSeparationofAtomicThinning .. ... ... . 173
5.4Discussion .. ... .... ... .... ... ... .... ... .... ... . 177
6MixandSwitch 179
6.1Adding theRules Mixand Nullary Mix.. ... .... ... .... ... . 179
6.2The Switch Rule . .... ... .... ... ... ... ... . 185
6.3Discussion .. ... ... ... ... .... ... .... ... . 195
7ANoncommutative Extension of MELL 197
7.1Structuresand Rules ... ... .... ... ... .... ... .... ... . 198
7.2Decomposition.. .... ... ... ... ... ... . 202
7.2.1Permutation of Rules. .... ... ... .... ... .... ... . 204
7.2.2CyclesinDerivations.. ... ... ... ... . 209
7.3Cut Elimination. .... ... .... ... ... .... ... .... ... . 215
7.3.1 Splitting.. .... ... .... ... ... .... ... .... ... . 215
7.3.2Context Reduction ... ... ... ... ... . 224
7.3.3Eliminationofthe Up Fragment.. ... .... ... .... ... . 226
7.4 The Undecidability of System NEL . . . . . . . . ... ... . 231
7.4.1Two CounterMachines .... ... ... .... ... .... ... . 232
7.4.2EncodingTwo CounterMachinesinNEL Structures . ... . 233
7.4.3Completenessofthe Encoding ... ... .... ... .... ... . 235
7.4.4SomeFacts aboutSystemBV. ... ... ... ... . 236
7.4.5Soundness of the Encoding . . . . . . . . .... ... .... ... . 241
7.5Discussion .. ... .... ... .... ... ... ... ... . 248
8OpenProblems 249
8.1Quantifiers. ... .... ... .... ... ... .... ... .... ... . 249
8.2A GeneralRecipe forDesigning Rules ... ... .... ... .... ... . 250
8.3The Relation between Decompositionand CutElimination. ... . 251
8.4 Controlling the Nondeterminism . . . . . . . . . .... ... .... ... . 252
8.5The Equivalencebetween System BV andPomsetLogic ... ... . 252
8.6 The Decidability of MELL . . . .... ... ... .... ... .... ... . 253
8.7The EquivalenceofProofsinthe Calculus of Structures ... ... . 253
Bibliography 255
Index 263List of Figures
1.1Overviewoflogicalsystems discussedinthisthesis. . ... .... ... .. 13
2.1 System LL in thesequent calculus . ... ... .... ... .... ... .. 20
3.1 Basic equations for the syntactic congruence for LS structures... ... .. 26
3.2 System SLS .... ... ... .... ... ... .... ... .... ... .. 35
3.3 System LS . ... ... ... ... ... ... .. 36
3.4 System LS .... ... ... .... ... ... .... ... .... ... .. 46
4.1 System MELL in thesequent calculus... ... .... ... .... ... .. 84
4.2 Basic equations for the syntactic congruence of ELS structures . . ... .. 85
4.3 System SELS ... ... ... .... ... ... .... ... .... ... .. 86
4.4 System ELS .... ... ... ... ... ... ... .. 86
4.5 Possible interferences of redex and contractum of two consecutive rules . . . 88
4.6Examplesfor interferences between twoconsecutive rules. . .... ... .. 89
4.7 Permuting b↑ up and b↓ down ... ... ... .... ... ... .. 99
4.8Connectionof!-links and?-links .. ... ... ... .... ... .. 102
4.9 A cycle χ with n(χ)=2 ... .... ... ... .... ... ... .. 106
4.10 A promotion cycle χ with n(χ)=3. ... ... ... .... ... .. 107
4.11 A pure cycle χ with n(χ)=2 .... ... ... .... ... ... .. 109
4.12 Example (with n(χ)= 3) forthe markinginside∆ .. ... .... ... .. 110
4.13 Cut elimination for system SELS∪{1↓} . ... .... ... ... .. 132
4.14 Proof of the interpolation theorem for system SELS.. ... .... ... .. 141
5.1 System SLLS ... ... ... .... ... ... .... ... .... ... .. 146
5.2 System LLS .... ... ... ... ... ... ... .. 152
◦6.1 Basic equations for the syntactic congruence of ELS structures . . ... .. 181
◦6.2 System SELS ... ... ... .... ... ... .... ... .... ... .. 182
◦6.3 System ELS ... ... ... ... ... ... ... .. 182
◦6.4 System SS .... ... ... .... ... ... .... ... .... ... .. 183
◦6.5 System S . ... ... ... ... ... ... .. 183
7.1 Basic equations for the syntactic congruence of NEL structures . . ... .. 198
7.2 System SNEL ... ... ... .... ... ... .... ... .... ... .. 199
7.3 System NEL.... ... ... ... ... ... ... .. 200
7.4 System SBV ... ... .... ... ... .... ... .... ... .. 201
7.5 System BV .... ... ... ... ... ... ... .. 201
viiviii List of Figures1
Introduction
1.1 Proof Theory and Declarative Programming
Proof theory is the area of mathematics which studies the concepts of mathematical proof
and mathematical provability [Bus98]. It is mainly concerned with the formal syntax of
logical formulae and the syntactic presentations of proofs, and can therefore be regarded
as “logic from the syntactic viewpoint” [Gir87b]. An important topic of research in proof
theory is the relation between finite and infinite objects. In other words, proof theory
investigates how infinite mathematical objects are denoted by fini