# Tag Info

$\lambda$-calculus has two key roles. It is a simple mathematical foundation of sequential, functional, higher-order computational behaviour. It is a representation of proofs in constructive logic. This is also known as the Curry-Howard correspondence. Jointly, the dual view of $\lambda$-calculus as proof and as (sequential, functional, higher-order) ...
Here is one problem described in the book "A second course in formal languages and automata theory" by Shallit. Let $u$ and $v$ be two distinct words with $|u|=|v|=n$. What is the size of the smallest DFA that accepts $u$ but rejects $v$, or vice versa? Robson, in his paper "Separating strings with small automata" in 1989 proved an upper bound $O(n^{... 61 As a department chair, I can say you aren't alone. These situations come up all too often. Please do reach out to your department chair, graduate program director or grad student ombudsperson if your institution has one. We want to know when our faculty are behaving badly and often we can help. 52 Is this a common situation that a researchers notices that her idea is not going to work after considerable amount of work? Yes. But as you get more experienced, you're able to "fail fast" - learn how to test the idea quickly to see if it passes a 'smell test'. What do you do when you realized that an approach you had in mind is not going to work ... 51 SAT, CP, SMT, (much of) ASP all deal with the same set of combinatorial optimisation problems. However, they come at these problems from different angles and with different toolboxes. These differences are largely in how each approach structures information about the exploration of the search space. My working analogy is that SAT is machine code, while the ... 48 Here's a very simple decision problem about DFA's. Given a DFA M, does M accept the base-2 representation of at least one prime number? Currently, we don't even know if this problem is recursively solvable. If it is recursively solvable, and we had an algorithm for it, we could resolve the longstanding open problem about whether there are any Fermat ... 44 The Černý conjecture is still open and important. It is about DFAs that have a synchronizing word (a word with the property that two copies of the automaton started in different states always end up in the same state as each other after both processing the word), and asks whether (for$n$-state automata) the length of the shortest such word is always at most ... 44 To complete the other answers: I think that Turing Machine are a better abstraction of what computers do than finite automata. Indeed, the main difference between the two models is that with finite automata, we expect to treat data that is bigger than the state space, and Turing Machine are a model for the other way around (state space >> data) by making the ... 43 It might come as no surprise, but there is a substantial overlap between cstheory Q&A power-users and the blogosphere. We even had a dedicated blog for a while, with some great posts but it fell into disuse. However, I thought I would list some of the blogs run by our top 38 users that have had new posts since 2012: David Eppstein's 0xDE: graph-theory ... 40 I was just referred to this question by graduate students that, in my opinion, were far too influenced by the answers. So let me start with two generic advises. To the aspiring scientist: Don't assign too much weight to any answer on such matters, and don't assume that a small and highly non-random sample represents the common views among senior (or non-... 40 I strongly disagree with the "find a list of open problems" approach. Usually open problems are quite hard to make progress on, and I'm thoroughly unconvinced that good research is done by tackling some hard but uninteresting problem in a technical area. That being said, of course solving an open problem is really good for academic credentials. But that's ... 38 This is very common, and certainly frustrating. Here is my advice: Don't wait until you have a complete result to start writing. Maintain a TeX document with formal descriptions of your problem, proofs of preliminary lemmas, etc. as you go. It is easy to convince yourself that something is true and overlook simple mistakes if you are holding the argument ... 37 I did a survey on Twitter about this a while back, results here. A few of my favorites: Parametric Polymorphism through Runtime Sealing, or, Theorems for Low, Low Prices! by Jacob Matthews and Amal Ahmed, ESOP 2008 DOI:10.1007/978-3-540-78739-6_2 F-ing Modules by Andreas Rossberg, Claudio Russo, and Derek Dreyer, TLDI 2010 Cons should not cons its arguments ... 34 Software Foundations by Benjamin C. Pierce would be a good place to start. It would be a make a good precursor to his Types and Programming Languages. There is also Simon Thompson's Type Theory and Functional Programming and Girard's Proofs and Types. 32 There are two approaches when considering this question: historical that pertains to how concepts were discovered and technical which explains why certain concepts were adopted and others abandoned or even forgotten. Historically, the Turing Machine is perhaps the most intuitive model of several developed trying to answer the Entscheidungsproblem. This is ... 31 I have always seen the notion of nondeterminism in computation attributed to Michael Rabin and Dana Scott. They defined nondeterministic finite automata in their famous paper Finite Automata and Their Decision Problems, 1959. Rabin's Turing Award citation also suggests that Rabin and Scott introduced nondeterministic machines. 30 I used to like quirky titles when I started out in computer science but got bored eventually. Some authors manage to write titles that are clever, memorable and relevant but most attempts at funny titles results in unnecessarily long, uninformative and kludgy phrases that I find difficult to remember and look up. There are papers like Pnueli's The Temporal ... 30 First, "theoretical computer science" means different things to different people. I think for most users on this site, a historical caricature (which reflects some modern sociological tendencies) is that there is "Theory A" and "Theory B" (with no implied order relation between them): Theory A consists of the theory of algorithms, complexity theory, ... 29 I think$\lambda$-calculus has contributed in many ways to this field, and still contributes to it. Three examples follow, and this is not exhaustive. Since I am not a specialist in$\lambda$-calculus, I certainly miss some important points. First, I think having different models of computation that turn out to represent the exact same set of functions was ... 28 Try the 50+ page essay "Why Philosophers Should Care About Computational Complexity" https://arxiv.org/abs/1108.1791 28 You should switch advisors. Since you are independently writing papers and have a track record, it should be possible to find a fair-minded theory advisor in a different technical area who is willing to do the administrative aspects of handling a PhD thesis. Your department chair should also help in this matter. 27 There have been recent developments in dependent type theory which relate type systems to homotopy types. This is now a relatively small field, but there is a lot of exciting work being done right now, and potentially a lot of low hanging fruit, most notably in porting results from algebraic topology and homological algebra and formalizing the notion of ... 25 Algebraic geometry is used heavily in algebraic complexity theory and in particular in geometric complexity theory. Representation theory is also crucial for the latter, but it's even more useful when combined with algebraic geometry and homological algebra. 25 Yes, it happens that the work that merits the Turing award was pioneered or introduced in a single very influential paper. Sometimes, this is even explicitly the reason for the award. For example, in 1976, Rabin and Scott were given the Turing award For their joint paper "Finite Automata and Their Decision Problem," which introduced the idea of ... 24 Title: Intersection non-emptiness for two DFA's Description: Given two DFA's$D_1$and$D_2$, does there exist a string$x$such that$D_1$and$D_2$both accept$x$? Open Problem: Can we solve intersection non-emptiness for two DFA's in$o(n^2)$time? If we could solve this problem in$O(n^{\delta})$time where$\delta$< 2, then the strong ... 24 Very briefly: the simply-typed$\lambda$-calculus does not have dependent types. Dependent types were proposed by de Bruijn and Howard who wanted to extend the Curry-Howard correspondence from propositional to first-order logic. The key contribution of Martin-Löf's is a novel analysis of equality. There are two main ways of giving Curry-Howard style ... 24 In some fields (like e.g. Economics and Mathematics) single authored papers -are- a good thing to have when you go on the job market. In theoretical computer science, collaboration is much more common, and it is not unusual for even relatively senior researchers to have very few single authored papers. It is not at all suspicious if a student on the market ... 22 Apart from the foundational role of the$\lambda$-calculus, which was mentioned in all other answers, I would like to add something on What exactly did the lambda calculus do to advance the theory of CS? I believe that concurrency theory is one field of CS which has been tremendously influenced by the compositional view mentioned by Martin Berger. Of ... 22 As for question 2, there are at least two examples of$NP$-completeness proofs that involve computer-assistant. Erickson and Ruskey provided a computer-aided proof that Domino Tatami Covering is NP-complete. They gave a polynomial time reduction from planar 3-SAT to tatami domino covering. A SAT-solver (Minisat) was used to automate gadgets discovery in ... 22 You're in good company. Kurt Gödel criticized$\lambda\$-calculus (as well as his own theory of general recursive functions) as not being a satisfactory notion of computability on the grounds that it is not intuitive, or that it does not sufficiently explain what is going on. In contrast, he found Turing's analysis of computability and the ensuing notion of ...