tag:blogger.com,1999:blog-3722233.post6400634916690563642..comments2023-03-20T21:49:52.361-05:00Comments on Computational Complexity: Where do theorems go to die?Lance Fortnowhttp://www.blogger.com/profile/06752030912874378610noreply@blogger.comBlogger9125tag:blogger.com,1999:blog-3722233.post-16474265610379372472011-10-02T16:33:52.117-05:002011-10-02T16:33:52.117-05:00I've seen it mentioned a few times on this blo...I've seen it mentioned a few times on this blog that complexity theory is moving from logical to combinatorial techniques. Would you place descriptive complexity/finite model theory (Immerman, Grohe-type work) in the set of techniques being moved away from?Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-67305399763588152452011-09-24T12:10:22.584-05:002011-09-24T12:10:22.584-05:00Some results you quote have not died. They have fo...Some results you quote have not died. They have found their true home where they have been nurtured, fed and have multiplied with joyful abandon. <br /><br />Items 2 and 3 alone constitute core material behind graduate courses, research papers and tools in various different areas. I was taught Presburger arithmetic in three courses in ETH Zurich, and then another three courses in Oxford. In contrast, I expect that students at these, and many other universities see (insert your favourite complexity theorem) at most once.<br /><br />- The decidability of Presburger arithmetic is taught in courses on automata theory, program verification, and automated deduction (yes, those are very different areas). The quest for efficient implementations and efficiently decidable sub-cases continues to this day.<br /><br />- The automata-based decidability proofs of logical theories have descendants in recent papers and tools using automata to decide theories of linear-real arithmetic and strings.<br /><br />- Rabin's theorem and various relatives are covered in courses and conferences on games, modal logics, and automata theory. The best paper award at STOC '11 went, I believe to Oliver Friedmann's work on Simplex. The bulk of his work is on fixed point logic and parity games.<br /><br />- The automata-based proof method is alive in Jerome Leroux's recent work on the reachability problem for Vector Addition Systems.<br /><br />- Omega automata *are* known. Well known. Extremely well known. More well known now than they have every been. This material is bread and butter for, not one, not two, but many, many, disjoint research areas. <br /> <br />The heritage of the automata-logic proofs, appears in programming language semantics, verification of functional programs, analysis of XML and XML schema, malware detection in Javascript, automated, high-level synthesis of hardware, program termination systems, mining of interfaces from Java APIs, modern results in language theory, papers that have appeared in the last 5 years. There are multiple tools whose core algorithms can be traced back to such proofs.<br /><br />It is true that different communities form and study increasingly narrower problems, as the field progresses. What is not true is that contemporary complexity course syllabi are representative of fundamental theoretical problems in computer science. For example, I consider the language inclusion problem for boring, old-school finite automata and its omega-variants an extremely fundamental problem at the heart of much computer science. How much airtime would this problem get in a course? Well, there is much current interest in these problems (implementation competitions, best paper awards in theory conferences, etc).Vijay D'Silvahttp://www.cs.ox.ac.uk/people/vijay.dsilva/noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-46617802683465648712011-09-23T09:01:39.160-05:002011-09-23T09:01:39.160-05:00The OLD course in complexity theorem at Maryland,
...The OLD course in complexity theorem at Maryland,<br />CMSC 650 (Recursion theory, NPC, Mahaney's theorem)<br />and the NEW course CMSC 652(GI NPC--> PH collapses,<br />USAT \in P --> NP=R, PCP stuff) overlap in ONLY<br />one place- Cook's theorem.<br /><br />Even the new course, now that I look at it, is a bit outdated. Maybe a byte outdated.GASARCHhttps://www.blogger.com/profile/06134382469361359081noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-64600068388097058132011-09-23T08:38:30.359-05:002011-09-23T08:38:30.359-05:00I haven't taught the local complexity course i...I haven't taught the local complexity course in over a decade, but if I did, several theorems from my old notes would have to "die" to make room for the PCP theorem, APX hard classes, FPTAs, Quantum, etc.<br /><br />Given the fix number of lectures, this seems like the normal thing to do.Alex Lopez-Ortiznoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-12999740221578740862011-09-22T20:40:14.535-05:002011-09-22T20:40:14.535-05:00"Part of this is that Complexity theory has c..."Part of this is that Complexity theory has changed from Logic-Based to Combinatorics-Based"<br /><br />Amazingly, this happened just as logic-based algorithms were being used more and more in industrial applications.<br /><br />-- Moshe VardiMoshe Vardihttp://www.cs.rice.edu/~vardinoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-32650990837061825442011-09-22T19:11:14.483-05:002011-09-22T19:11:14.483-05:00For what it's worth, I agree-- I think the *pr...For what it's worth, I agree-- I think the *proof* of Ladner's theorem is about as close to pedagogically vacuous as a proof can get (at least, for the general audience of a complexity course).<br /><br />As an example (sample size: 1), I recently spent a long hour attempting to explain the details of the proof to someone, only to have a final reaction with a gist of "Well... Ok. Whatever!"<br /><br />I do (strongly) believe the theorem itself is important to teach though, if for no other reason than to combat potential faulty intuition about the structure of classes.Daniel Aponnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-73580563776045066392011-09-21T18:12:20.330-05:002011-09-21T18:12:20.330-05:00For the record, I covered Ladner's theorem and...For the record, I covered Ladner's theorem and Mahaney's theorem the first time I taught a complexity course. This time around, I'm stating Ladner's thorem (but skipping the proof) and omitting Mahaney's theorem entirely.Jonathan Katzhttps://www.blogger.com/profile/07362776979218585818noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-61529575699717940932011-09-21T15:25:47.149-05:002011-09-21T15:25:47.149-05:00theorems never die, they just fade awaytheorems never die, they just fade awayAnonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-52908620652424902192011-09-21T12:13:53.714-05:002011-09-21T12:13:53.714-05:00Items 2 and 3 are the basis of a number of "f...Items 2 and 3 are the basis of a number of "formal methods" that are used by practitioners to find bugs in systems. Dexter has a history in both the complexity and formal methods areas so it is no wonder that he chose to cover them; bringing these too streams together is one of nice things about his book. (Sipser also covered 2 in his text.) <br /><br />I think that you are exaggerating the extent to which these things used to be taught. I took courses on these things in the early 1980's from Cook and others but most of the above topics were not taught. (In the computability course we did 6, and in the complexity theory we were told about Ladner's theorem but didn't do anything about the proof - though it may have been mentioned that its proof was like 6.)<br /><br />On the other hand, there can be a lot of value in knowing about "dead" theorems. Buchi (better known for his omega-automata work and hence virtually unknown in complexity circles), proved the following initially surprising property (which I liked to give as an extra-credit exercise when I used to teach automata): The language consisting of the set of possible strings that might ever appear on a PDA stack is regular. This theorem was an essential part of the development of leveraging tools that could verify finite-state systems to tools that can verify stack machines.<br /><br />Maybe your topic should be about the relative impact of textbooks versus papers in shaping a field. My sense is that our field suffered from a lack of quality textbooks precisely because the papers were out-stripping authors' ability to organize and synthesize. There was a long gap between Papadimitriou's text, which came out when the field was on the cusp of major advances, and Arora-Barak. (Sipser's text, though very readable, is much broader than a complexity text and only gave groundwork for a few aspects of complexity.)Paul Beamenoreply@blogger.com