Linear Logic and Noncommutativity in the

By
Published by

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


Published : Thursday, May 01, 2003
Reading/s : 12
Origin : lix.polytechnique.fr
Number of pages: 276
See more See less

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 finite syntactic constructions,
andhow facts concerning infinite structures are proved by finite proofs. Another important
question of proof theoretical research is the investigation of intuitive proofs [Kre68]. More
precisely, not only the study of a given formal system is of interest, but also the analysis of
the intuitive proofs and the choice of the formal systems needs attention.
These general questions of research are not the only ones that are investigated in proof
theory, but they arethemostimportantonesfortheapplication of proof theory in computer
science in general, and in declarative programming in particular. By restricting itself to
finitary methods, proof theory studies the objects that computers (which are, per se, finite)
can deal with.
In declarative programming the intention is to describe what the user wants to achieve,
rather than how the machine is accomplishing it. By concerning itself with the relation
between intuitive proofs and formal systems, proof theory can help to design declarative
programming languages in such a way that the computation of the machine meets the
intuition of the user.
This rather high level argumentation is made explicit and put on formal grounds by the
two proof theoretical concepts of proof normalisation (or proof reduction)and proof search
(or proof construction), which provide the theoretical foundations for the two declarative
programming paradigms of functional programming and logic programming,respectively.
Proof normalisation and functional programming. The relationbetween the func-
tional programming paradigm and proof theory is established by the Curry-Howard-iso-
morphism [CF58, How80, Tai68], which identifies formal logical systems, as they are stud-
ied inprooftheory, with computational systems, as they are studied in type theory. More
12 1. Introduction
precisely, a formula corresponds to a type and a proof of that formula to a term of the corre-
sponding type. For example, natural deduction proofs of intuitionistic logic [Gen34, Pra65]
correspond to terms of the simply typed λ-calculus [Chu40]. This bijective mapping be-
tween proofs and terms is an isomorphism becauseanormalisation step of the proof in the
logical system corresponds exactly to a normalisation step of the λ-term, whichin turnis
acomputation step in functional programming. Hence, the normalisation (or reduction) of
the proof is the computation of the corresponding functional program. The isomorphism
can be summarised as follows:
formula = type ,
(correct) proof = (well-typed) program ,
proof normalisation = computation .
The correspondence does not only hold for propositional logic, but also for first order logic,
which corresponds to dependent types (without inductive types), and second order logic,
which corresponds to polymorphic types. A good introduction and historical overview for
this can be found in [Wad00]. A detailed survey is [SU99]. For the relation between classical
logic and type theory, the reader is referred to [Ste01].
The importance of the Curry-Howard-isomorphism for computer science is also corrob-
orated by the fact that proofs of termination and correctness in computer science often
reduce to known techniques in proof theory. The probably best known example for this is
the proof of strong normalisation of the polymorphic λ-calculus (also known as system F)
[Gir72], which is the basis for the type systems of functional programming languages like
ML or Haskell.
Another application of the Curry-Howard-isomorphism is the possibility of extracting
programs from proofs. For example, the Coq proof assistant (see e.g. [BC03]) can extract a
certified program from the constructive proof of its formal specification. Another example
+is the NuPrl development system [CAB 86]. The basic idea is that from a constructive
proof of
Φ ∀ x.∃y.P(x,y),
where Φ is a set of hypotheses and P abinarypredicate, itispossible to obtain a program
that computes from a given input x an output y such that P(x,y)holds. The types
corresponding to the formulae in Φ are the types of parameters for the program.
Proof search and logic programming. The relationbetween logic programming and
proof theory is more obvious because the paradigm of logic programming is already defined
in terms of logic and proofs. A logic program is a conjunction of formulae, each of which
canbeseen as an instruction. The input to the program is another formula, called the goal.
The computation is the search for a proof (also called proof construction) showing that
the goal is a logical consequence of the program. We have the following correspondence
[And01]:
formula = instruction ,
(incomplete) proof = state ,
proof search = computation .

Be the first to leave a comment!!

12/1000 maximum characters.