Logic, Automata, and Computational Complexity - the Works of Stephen A. Cook

Professor Stephen A. Cook is a pioneer of the theory of computational complexity. His work on NP-completeness and the P vs. NP problem remains a central focus of this field. Cook won the 1982 Turing Award for "his advancement of our understanding of the complexity of computation in a significant and profound way." This volume includes a selection of seminal papers embodying the work that led to this award, exemplifying Cook's synthesis of ideas and techniques from logic and the theory of computation including NP-completeness, proof complexity, bounded arithmetic, and parallel and space-bounded computation. These papers are accompanied by contributed articles by leading researchers in these areas, which convey to a general reader the importance of Cook's ideas and their enduring impact on the research community. The book also contains biographical material, Cook's Turing Award lecture, and an interview. Together these provide a portrait of Cook as a recognized leader and innovator in mathematics and computer science, as well as a gentle mentor and colleague. Logic, Automata, and Computational Complexity 12 Contents 16 Introduction 22 Note on formatting and typesetting 26 Acknowledgments 27 I BIOGRAPHICAL BACKGROUND 28 1 Stephen Cook: Complexity's Humble Hero 30 1.1 Growing Up: Buffalo and Cows 31 1.2 The Lure of Mathematics 32 1.3 From Smooth Sailing to Rough Waters 36 1.4 Growing Roots, Making Waves 41 1.5 The Quiet Influencer 47 1.6 Profound and Complex 53 2 ACM Interview of Stephen A. Cook by Bruce M. Kapron 56 II THE TURING AWARD LECTURE 72 3 The 1982 ACM Turing Award Lecture 74 Abstract 75 1 Early Papers 75 2 Early Issues and Concepts 76 3 Upper Bounds on Time 78 4 Lower Bounds 80 4.1 Natural Decidable Problems Proved Infeasible 81 4.2 Structured Lower Bounds 82 4.3 Time–Space Product Lower Bounds 83 4.4 NP-Completeness 83 4.5 #P-Completeness 84 5 Probabilistic Algorithms 85 6 Synchronous Parallel Computation 86 7 The Future 89 Acknowledgments 89 References 90 III PERSPECTIVES ON COOK'S WORK 98 4 Cook's NP-completeness Paper and the Dawn of the New Theory 100 4.1 History 100 4.2 Cook's Other 1971 Paper 103 4.3 The Paper at the 3rd STOC 104 4.4 The Mystery of Section 4.3 105 4.5 Aftermath 106 5 The Cook–Reckhow Definition 110 5.1 Definition of Proof Systems 112 5.2 Simulations among Proof Systems 115 5.3 Hard Tautologies and the PHPn Formula 118 Acknowledgments 121 6 Polynomially Verifiable Arithmetic 122 6.1 Introduction 122 6.2 The Equational Theory PV for Polynomial Time Computability 123 6.3 Extended Resolution and PV 126 6.4 Subsequent Developments 129 Acknowledgments 132 7 Towards a Complexity Theory of Parallel Computation 134 7.1 First Words 134 7.2 The Early Years 134 7.3 The Beginnings of a Theory 136 7.4 Development and Issues with the Theory 138 7.5 Steve's Class and Nick's Class 140 7.6 Cook's Surveys of Parallel Computation 148 7.7 Last Words 152 8 Computation with Limited Space 154 8.1 Time and Space Bounds 154 8.2 Pebbling 157 8.3 Circuits 163 8.4 Branching Programs 165 IV SELECTED PAPERS 168 9 The Complexity of Theorem-Proving Procedures 170 Summary 170 1 Tautologies and Polynomial Re-Reducibility 170 2 Discussion 175 3 The Predicate Calculus 176 4 More Discussion 178 References 179 10 Characterizations of Pushdown Machines in Terms of Time-Bounded Computers 180 Abstract 180 Key words and phrases 180 CR Categories 181 1 Introduction 181 2 Time-Bounded Computers 181 3 Other Machine Models 182 4 The Main Theorem 184 4.1 Algorithm for M2 189 5 Applications of the Main Theorem 190 6 Conclusion and Open Questions 198 Acknowledgment 198 References 198 11 The Relative Efficiency of Propositional Proof Systems 200 1 Introduction 200 2 Frege Systems 204 3 Natural Deduction Systems 206 4 Extended Frege Systems 209 5 The Substitution Rule 216 References 217 12 Feasibly Constructive Proofs and the Propositional Calculus (Preliminary Version) 220 1 Introduction 220 2 The System PV 223 Rules of PV 225 3 The System PV1 229 4 The Gödel Incompleteness Theorem for PV 232 5 Propositional Calculus and the Main Theorem 235 6 Propositional Formulas Assigned to Equations of PV 239 6.1 Semantic Correctness of propm 240 7 PV as a Propositional Proof System 242 8 Conclusions and Future Research 243 Acknowledgments 244 References 244 13 Towards a Complexity Theory of Synchronous Parallel Computation 246 Abstract 246 1 Introduction 246 2 Circuits and Alternating Turing Machines 249 3 Log Depth vs Log Space 255 4 Conglomerates and Aggregates 257 5 Hardware Modification Machines 261 6 Other Modifiable Models 262 7 Simultaneous Resource Bounds 264 8 Open Questions 266 Acknowledgement 267 References 267 14 A Time-Space Tradeoff for Sorting on a General Sequential Model of Computation 272 Abstract 272 Key words 272 1 Introduction 272 2 The Formal Model and an Outline of the Proof 274 3 The Proof of the Main Lemma 277 4 Proof of the Main Theorem 283 5 Conclusion 284 Acknowledgment 286 References 286 15 Pebbles and Branching Programs for Tree Evaluation 288 1 Introduction 289 1.1 Summary of Contributions 294 1.2 Relation to Previous Work 295 1.3 Organization 296 2 Preliminaries 296 2.1 Branching Programs 297 2.2 One Function Is Enough 299 2.3 Pebbling 301 3 Connecting TMS, BPS, and Pebbling 303 4 Pebbling Bounds 306 4.1 Previous Results 306 4.2 Results for Fractional Pebbling 310 4.3 White Sliding Moves 322 5 Branching Program Bounds 323 5.1 The Nec̆iporuk Method 325 5.2 The State Sequence Method 329 5.3 Thrifty Lower Bounds 334 6 Conclusion 341 Acknowledgments 343 References 343 V THE BERKELEY NOTES 346 16 Cook's Berkeley Notes 348 17 A Survey of Classes of Primitive Recursive Functions 352 1 Basic Notions 352 Relations vs. functions 352 Cofinal Classes 352 Explicit Transformation 353 Substitution 353 Boolean Operations 353 Bounded (i.e. limited) quantification 353 Bounded (i.e. limited) recursion 353 m-adic notation 353 Bounded (i.e. limited) recursion on notation 353 Subpart quantification 354 2 The Grzegorczyk Hierarchy 354 Notation 354 3 Computation Time and Limited Recursion on Notation 355 Extended Positive Rudimentary Functions, L+. 356 4 The Ritchie Hierarchy 356 5 Other Classes 357 Notation 357 The Strictly m-rudimentary relations 357 The positive m-rudimentary relations 358 The Strongly m-rudimentary relations 358 The m-rudimentary relations 358 The constructive arithmetic relations 358 The extended positive m-rudimentary relations 358 A context-sensitive language 358 Spectra 358 6 Summary of Facts and Open Questions 359 Closure under operations of relation classes 361 Functions 361 References 361 18 Further Reading 364 Bibliography 366 Bibliography of the Works of Stephen A. Cook 366 1965 366 1966 366 1968 366 1969 366 1970 367 1971 367 1972 367 1973 367 1974 368 1975 368 1976 369 1978 369 1979 369 1980 369 1981 370 1982 370 1983 370 1984 371 1985 371 1986 371 1987 371 1988 372 1989 372 1990 372 1991 373 1992 373 1993 373 1995 374 1996 374 1997 374 1998 374 1999 374 2000 375 2001 375 2002 375 2003 375 2004 376 2005 376 2006 377 2007 377 2009 377 2010 378 2011 378 2012 378 2013 379 2014 380 2016 380 2017 380 References 381 Contributors' Biographies 410 Index 414 Publisher:,Association,for,Computing,Machinery