Lectures on the Curry-Howard Isomorphism (eBook)

Morten Heine Sorensen, Pawel Urzyczyn (Autoren)

eBook Download: EPUB

2006 | 1. Auflage
456 Seiten
Elsevier Science (Verlag)
978-0-08-047892-0 (ISBN)

Infos

The Curry-Howard isomorphism states an amazing correspondence between systems of formal logic as encountered in proof theory and computational calculi as found in type theory. For instance,
minimal propositional logic corresponds to simply typed lambda-calculus, first-order logic corresponds to dependent types, second-order logic corresponds to polymorphic types, sequent calculus is related to explicit substitution, etc.

The isomorphism has many aspects, even at the syntactic level:
formulas correspond to types, proofs correspond to terms, provability corresponds to inhabitation, proof normalization corresponds to term reduction, etc.

But there is more to the isomorphism than this. For instance, it is an old idea---due to Brouwer, Kolmogorov, and Heyting---that a constructive proof of an implication is a procedure that transforms
proofs of the antecedent into proofs of the succedent, the Curry-Howard isomorphism gives syntactic representations of such procedures. The Curry-Howard isomorphism also provides theoretical foundations for many modern proof-assistant systems (e.g. Coq).

This book give an introduction to parts of proof theory and related aspects of type theory relevant for the Curry-Howard isomorphism. It can serve as an introduction to any or both of typed lambda-calculus and intuitionistic logic.

Key features
- The Curry-Howard Isomorphism treated as common theme
- Reader-friendly introduction to two complementary subjects: Lambda-calculus and constructive logics
- Thorough study of the connection between calculi and logics
- Elaborate study of classical logics and control operators
- Account of dialogue games for classical and intuitionistic logic
- Theoretical foundations of computer-assisted reasoning

? The Curry-Howard Isomorphism treated as the common theme.
? Reader-friendly introduction to two complementary subjects: lambda-calculus and constructive logics
? Thorough study of the connection between calculi and logics.
? Elaborate study of classical logics and control operators.
? Account of dialogue games for classical and intuitionistic logic.
? Theoretical foundations of computer-assisted reasoning

Inhalt

Cover 1
Title Page 4
Copyright Page 5
Table of Contents 12
Chapter 1 Type-free Lambda-calculus 16
1.1 A gentle introduction 16
1.2 Pre-terms and Lambda-terms 18
1.3 Reduction 25
1.4 The Church-Rosser theorem 27
1.5 Leftmost reductions are normalizing 29
1.6 Perpetual reductions and the conservation theorem 33
1.7 Expressibility and undeeidability 34
1.8 Notes 37
1.9 Exercises 38
Chapter 2 Intultionistic logic 42
2.1 The BHK interpretation 43
2.2 Natural deduction 47
2.3 Algebraic semantics of classical logic 49
2.4 Heyting algebras 52
2.5 Kripke semantics 58
2.6 The implicational fragment 62
2.7 Notes 63
2.8 Exercises 65
Chapter 3 Simply typed Lambda-calcuIus 70
3.1 Simply typed Lambda-ealculus a la Curry 71
3.2 Type reconstruction algorithm 75
3.3 Simply typed Lambda-calculus a la Church 78
3.4 Church versus Curry typing 80
3.5 Normalization 82
3.6 Church-Rosser property 85
3.7 Expressibility 87
3.8 Notes 88
3.9 Exercises 89
Chapter 4 The Curry-Howard isomorphism 92
4.1 Proofs and terms 92
4.2 Type inhabitation 94
4.3 Not an exact isomorphism 96
4.4 Proof normalization 98
4.5 Sums and products 101
4.6 Prover-skeptic dialogues 104
4.7 Prover-skeptic dialogues with absurdity 109
4.8 Notes 111
4.9 Exercises 115
Chapter 5 Proofs as combinators 118
5.1 Hubert style proofs 118
5.2 Combinatory logic 123
5.3 Typed combinators 125
5.4 Combinators versus lambda terms 128
5.5 Extensionality 131
5.6 Relevance and linearity 133
5.7 Notes 137
5.8 Exercises 138
Chapter 6 Classical logic and control operators 142
6.1 Classical prepositional lope 142
6.2 The Lambda meu-calculus 147
6.3 Subject reduction, confluence, strong normalization 152
6.4 Logical embedding and CPS translation 155
6.5 Classical prover-skeptic dialogues 159
6.6 The pure implicational fragment 165
6.7 Conjunction and disjunction 168
6.8 Notes 171
6.9 Exercises 172
Chapter 7 Sequent calculus 176
7.1 Gentzen's sequent calculus LK 177
7.2 Fragments of LK versus natural deduction 180
7.3 Gentzen's Hauptaatz 184
7.4 Cut elimination versus normalization 189
7.5 Lorenzen dialogues 196
7.6 Notes 204
7.7 Exercises 206
Chapter 8 First-order logic 210
8.1 Syntax of first-order logic 210
8.2 Informal semantics 212
8.3 Proof systems 215
8.4 Classical semantics 220
8.5 Algebraic semantics of intuitionistie logic 222
8.6 Kripke semantics 227
8.7 Lambda-calculus 234
8.8 Undeddability 236
8.9 Notes 239
8.10 Exercises 240
Chapter 9 First-order arithmetic 244
9.1 The language of arithmetic 244
9.2 Peano Arithmetic 247
9.3 Godel's theorems 249
9.4 Representable and provably recursive functions 252
9.5 Heyting Arithmetic 255
9.6 Kleene's realfeability interpretation 258
9.7 Notes 260
9.8 Exercises 262
Chapter 10 Godel's system T 266
10.1 From Heyting Arithmetic to system T 266
10.2 Syntax 268
10.3 Strong normalization 271
10.4 Modified realizability 275
10.5 Notes 280
10.6 Exercises 281
Chapter 11 Second-order logic and polymorphism 284
11.1 Prepositional second-order logic 285
11.2 Polymorphic lambda-calculus (system F) 291
11.3 Expressive power 295
11.4 Gurry-style polymorphism 299
11.5 Strong normalization 302
11.6 The inhabitation problem 305
11.7 Higher-order polymorphism 311
11.8 Notes 314
11.9 Exercises 315
Chapter 12 Second-order arithmetic 318
12.1 Second-order syntax 318
12.2 Classical second-order logic 320
12.3 Intuitionistic second-order logic 323
12.4 Second-order Peano Arithmetic 326
12.5 Second-order Heyting Arithmetic 329
12.6 Simplified syntax 330
12.7 Lambda-calculus 333
12.8 Notes 338
12.9 Exercises 338
Chapter 13 Dependent types 340
13.1 The language of Lambda P 341
13.2 Type assignment 343
13.3 Strong normalization 348
13.4 Dependent types a la Curry 350
13.5 Correspondence with first-order logic 352
13.6 Notes 354
13.7 Exercises 355
Chapter 14 Pure type systems and the Lambda-cube 358
14.1 System Lambda P revisited 358
14.2 Pure type systems 359
14.3 The Calculus of Constructions 361
14.4 Strong normalization 363
14.5 Beyond the cube 366
14.6 Girard's paradox 367
14.7 Notes 372
14.8 Exercises 373
Appendix A: Mathematical background 376
A.1 Set theory 376
A.2 Algebra and unification 380
A.3 Partial recursive functions 381
A.4 Decision problems 383
A.5 Hard and complete 386
Appendix B: Solutions and hints to selected exercises 388
Bibliography 417
Index 446

Textauszug

Preface

The Curry-Howard isomorphism, also widely known as the “propositions-as-types” paradigm, states an amazing correspondence between systems of formal logic and computational calculi.1 It begins with the observation that an implication A → B corresponds to a type of functions from A to B, because inferring B from A → B and A can be seen as applying the first assumption to the second one—just like a function from A to B applied to an element of A yields an element of B. Similarly, one can argue that proving the implication A → B by actually inferring B from A resembles constructing a function that maps any element of a domain A into an element of B.

In fact, it is an old idea—due to Brouwer, Kolmogorov, and Heyting—that a constructive proof of an implication from A to B is a procedure that transforms proofs of A into proofs of B. The Curry-Howard isomorphism formalizes this idea so that, for instance, proofs in the propositional intuitionistic logic are represented by simply typed λ-terms. Provable theorems are nothing else than non-empty types.

This analogy, first discovered by Haskell Brooks Curry in the 1930’s, has turned out to hold for other logical systems as well. Virtually all proof-related concepts can be interpreted in terms of computations, and virtually all syntactic features of various lambda-calculi and similar systems can be formulated in the language of proof theory. For instance, quantification in predicate logic corresponds to dependent product, second-order logic is connected to polymorphism, and proofs by contradiction in classical logic are close relatives of control operators, e.g. exceptions. Moreover, various logical formalisms (Hilbert style, natural deduction, sequent calculi) are mimicked by corresponding models of computation (combinatory logic, λ-calculus, and explicit substitution calculi).

Since the 1969 work of William Howard it has been understood that the proposition-as-types correspondence is not merely a curiosity, but a fundamental principle. Proof normalization and cut-elimination are another model of computation, equivalent to β-reduction. Proof theory and the theory of computation turn out to be two sides of the same field.

Recent years show that this field covers not only theory, but also the practice of proofs and computation. Advanced type theory is now used as a tool in the development of software systems supporting program verification and computer-assisted reasoning. The growing need for efficient formal methods presents new challenges for the foundational research in computer science.

For these reasons the propositions-as-types paradigm experiences an increasing interest both from logicians and computer scientists, and it is gradually becoming a part of the curriculum knowledge in both areas. Despite this, no satistfactorily comprehensive book introduction to the subject has been available yet. This volume is an attempt to fill this gap, at least in the most basic areas.

Our aim is to give an exposition of the logical aspects of (typed) calculi (programs viewed as proofs) and the computational aspects of logical systems (proofs viewed as programs). We treat in a single book many issues that are spread over the literature, introducing the reader to several different systems of typed λ-calculi, and to the corresponding logics. We are not trying to cover the actual software systems (e.g. Coq) based on the formulas-as-types paradigm; we are concerned with the underlying mathematical principles.

Although a great deal of our attention is paid to constructive logics, we would like to stress that we are entirely happy with non-constructive meta-proofs and we do not restrict our results to those acceptable to constructive mathematics.

An idea due to Paul Lorenzen, closely related to the Curry-Howard isomorphism, is that provability can be expressed as a dialogue game. Via the Curry-Howard isomorphism, terms can be seen as strategies for playing such games. While for us proofs and programs are more or less the same objects, we would hesitate to claim the same thing about dialogue games or strategies for such games. Nevertheless, there is an emerging picture that the Curry-Howard isomorphism is perhaps about three worlds, not two, or that all three worlds are one. We also go some way to convey this paradigm.

An important subject, the linear logic of J.-Y. Girard, is not treated here, although it is very close to the subject. In fact, linear logic (and related areas—geometry of interaction, ludics) opens an entire new world of connections between proofs and computations, adding new breathtaking perspectives to the Curry-Howard isomorphism. It deserves a broader and deeper presentation that would have to extend the book beyond reasonable size. After some hesitation, we decided with regret not to treat it at all, rather than to remain with a brief and highly incomplete overview.

As we have said above, our principal aim is to explore the relationship between logics and typed lambda-calculi. But in addition to studying aspects of these systems relevant for the Curry-Howard isomorphism, we also attempt to consider them from other angles when these provide interesting insight or useful background. For instance, we begin with a chapter on the type-free λ-calculus to provide the necessary context for typed calculi.

The book is intended as an advanced textbook, perhaps close to the border between a textbook and a monograph, but still on the side of a textbook. Thus we do not attempt to describe all current relevant research, or provide a complete bibliography. Sometimes we choose to cite newer or more comprehensible references rather than original works. We do not include all proofs, though most are provided. In general we attempt to provide proofs which are short, elegant, and contain interesting ideas. Though most proofs are based on solutions known from the literature, we try, whenever possible, to add a new twist to provide something interesting for the reader. Some new results are included too.

The book may serve as a textbook for a course on either typed λ-calculus or intuitionistic logic. Preferably on both subjects taught together. We think that a good way to explain typed λ-calculus is via logic and a good way to explain logic is via λ-calculus.

The expected audience consists mainly of graduate and PhD students, but also of researchers in the areas of computer science and mathematical logic. Parts of the text can also be of interest for scientists working in philosophy or linguistics.

We expect that the background of the readers of this book may be quite non-uniform: a typical reader will either know about intuitionistic logic or about λ-calculus (and functional programming), but will not necessarily be familiar with both. We also anticipate readers who are not familiar with any of the two subjects.

Therefore we provide an introduction to both subjects starting at a relatively elementary level. We assume basic knowledge about discrete mathematics, computability, set theory and classical logic within the bounds of standard university curricula. Appendix A provides some preliminaries that summarize this knowledge. Thus the book is largely self-contained, although a greater appreciation of some parts can probably be obtained by readers familiar with mathematical logic, recursion theory and complexity.

We hope that the bibliographical information is reasonably up to date. Each chapter ends with a Notes section that provides historical information and also suggests further reading. We try to include appropriate references, but sometimes we may simply not know the origin of a “folklore” idea, and we are sorry for any inaccuracies.

Each chapter is provided with a number of exercises. We recommend that the reader try as many of these as possible. Hints or solutions are given for some of the more difficult ones, hopefully making the book well-suited for self-study too. Some exercises are used as an excuse for including something interesting which is not in the mainstream of the book. The reader is also expected by default to do all omitted parts of proofs by herself.

Earlier versions of this text (beginning with the DIKU lecture notes [450]) have been used for several one-semester graduate/Ph.D. courses at the Department of Computer Science at the University of Copenhagen (DIKU), and at the Faculty of Mathematics, Informatics and Mechanics of Warsaw University. Summer school courses have also been held based on it.

Acknowledgments

Just like many other milestone ideas, the Curry-Howard isomorphism was discovered to various extents by different people at different times. And many others contributed to its development and understanding. The Brouwer – Heyting – Kolmogorov – Schönfinkel – Curry – Meredith – Kleene – Feys – Gödel – Läuchli – Kreisel – Tait – Lawvere – Howard – de Bruijn – Scott – Martin-Löf – Girard – Reynolds – Stenlund – Constable – Coquand – Huet –…–...

Produkt-Details

• Erscheint lt. Verlag: 4.7.2006
• Sprache: englisch
• Themenwelt: Sachbuch/Ratgeber
• Themenwelt: Mathematik / Informatik ► Informatik ► Theorie / Studium
• Themenwelt: Mathematik / Informatik ► Mathematik ► Logik / Mengenlehre
• Themenwelt: Naturwissenschaften
• Themenwelt: Technik
• ISBN-10: 0-08-047892-1 / 0080478921
• ISBN-13: 978-0-08-047892-0 / 9780080478920