Published by
###
profil-nechor-2012

- 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

See more
See less

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. Steﬀen H¨ olldobler

Gutachter: Prof. Dr. rer. nat. habil. Steﬀen 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 ﬁeld of proof

theory and introduced me to the calculus of structures. I beneﬁted 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 toSteﬀen 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 ﬁnancial support of the DFG-Graduierten-

kolleg 334 “Speziﬁkation 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.1Quantiﬁers. ... .... ... .... ... ... .... ... .... ... . 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 ﬁnite and inﬁnite objects. In other words, proof theory

investigates how inﬁnite mathematical objects are denoted by ﬁnite syntactic constructions,

andhow facts concerning inﬁnite structures are proved by ﬁnite 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

ﬁnitary methods, proof theory studies the objects that computers (which are, per se, ﬁnite)

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 identiﬁes 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 ﬁrst 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

certiﬁed program from the constructive proof of its formal speciﬁcation. 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 deﬁned

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 .

Share this publication