31 votes
Accepted

Who introduced nondeterministic computation?

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 ...
29 votes
Accepted

Impact of Grothendieck's program on TCS

Grothendieck's inequality, from his days in functional analysis, was initially proved to relate fundamental norms on tensor product spaces. Grothendieck called the inequality "the fundamental theorem ...
26 votes
Accepted

What was the original intent for the creation of Lambda calculus?

He wanted to create a formal system for the foundations of logic and mathematics that was simpler than Russell's type theory and Zermelo's set theory. The basic idea was to add a constant $\Xi$ to ...
24 votes
Accepted

Why was there a need for Martin-Löf to create intuitionistic type theory?

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 ...
23 votes

When have we found better bounds for known algorithms?

The Union-Find algorithm, which Tarjan1 showed had complexity $n \alpha(n)$, where $\alpha(n)$ is the inverse Ackermann function, had been analyzed previously by several people. According to Wikipedia,...
22 votes
Accepted

How exactly does lambda calculus capture the intuitive notion of computability?

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 ...
22 votes

Problems that started out with hopelessly intractable algorithms that have since been made extremely efficient

Computing a generating set of invariants (sometimes called the computational problem of "Noether's Normalization Lemma") for the action of $SL_3$ on an $n$-dimensional vector space $V$. (You ...
20 votes

Impact of Grothendieck's program on TCS

Grothendieck's impact can be felt in type theory and logic. For instance, Bart Jacobs' 700+ page volume Categorical Logic and Type Theory gives a uniform treatment of various type theories ($X$-type ...
  • 16.6k
17 votes
Accepted

Did Stephen Cook see the significance of showing that SAT is NP-Hard before actually proving it?

First of all, Cook actually showed that the problem of whether a logical expression is a tautology is $\mathbb{NP}$-complete under Cook reductions. The proof however works by replacing them with Karp ...
  • 3,741
17 votes
Accepted

Why was Schönfinkel's work on eliminating "bound variables" in logic so crucial?

TL;DR. The metamathematics of binding are subtle: they seem trivial but aren't — whether you deal with (higher-order) logics or 𝜆-calculus. They're so subtle that binding representations form an open ...
  • 2,029
17 votes
Accepted

Entscheidungsproblem vs. Unvollständigkeitssatz (soft question)

The two words do not refer to the same thing. Hilbert's Entscheidungsproblem was the question whether there is an algorithm that decides the universal truth of first-order logical sentences, which was ...
17 votes

Problems that started out with hopelessly intractable algorithms that have since been made extremely efficient

The task of unification went from an exponential solution to linear time in the timespan of about a decade. The original exponential algorithm was a corner-stone for symbolic AI approaches and enabled ...
  • 271
14 votes
Accepted

Are Turing machines still useful as model of computation?

I think the issue is that, you're misunderstanding the purpose of the Turing Machine model. Turing Machines are not meant to be programmed in. If you're writing code, you absolutely should not be ...
14 votes
Accepted

Rabin's "degree of difficulty of computing a function, and a partial ordering of recursive sets"

There are two loanable copies at The National Library of Israel. Here is a scanned copy.
  • 14.2k
14 votes
Accepted

When was co-NP introduced for the first time?

Albert R. Meyer and Larry J. Stockmeyer introduced the polynomial hierarchy in 1972 with their paper "the equivalence problem for regular expressions with squaring requires exponential space"...
13 votes

Impact of Grothendieck's program on TCS

Any applications of $p$-adic cohomology, etale cohomology in point counting formulas for algebraic varieties has roots in his work. I am guessing Mulmuley's vision of generalization of Riemann ...
  • 12.6k
12 votes

When have we found better bounds for known algorithms?

The algorithm of Paturi, Pudlák, Saks and Zane (PPSZ) for $k\text{-} \mathrm{SAT}$ had been known to have a running time of $O(1.364^n)$ for $3\text{-}\mathrm{SAT}$, with a better bound of $O(1.308^...
12 votes

Problems that started out with hopelessly intractable algorithms that have since been made extremely efficient

I can think of two additional examples to the ones mentioned above, although I'm not sure that they were ever considered intractable. Lovász Local Lemma - The Lovász local lemma (LLL) is a powerful ...
11 votes

Who introduced nondeterministic computation?

Here is what Odifreddi says on the issue: "Our model of a Turing machine is deterministic, in the sense that the instructions are required to be consistent (at most one of them is applicable ...
  • 21.3k
10 votes

Problems that started out with hopelessly intractable algorithms that have since been made extremely efficient

Interior point algorithms for LP. Although they came after Ellipsoid they are a different class of provably polynomial-time algorithms. And despite initial skepticism about their ability to outperform ...
10 votes

Problems that started out with hopelessly intractable algorithms that have since been made extremely efficient

Until Francis's QR algorithm was discovered, computing the eigenvalues was often done by first computing the characteristic polynomial, which was often an expensive and inaccurate endeavor, as has ...
  • 101
10 votes
Accepted

Are there two definitions of Cobham's thesis?

Cobham's thesis is essentially the Extended Church-Turing thesis. Historians of computer science have gone back and figured out who first proposed it, and attached his name to it. What Cobham was ...
9 votes
Accepted

System F and System T names

I posted this to TYPES, but its probably worth copying here as well: In "The system F of variable types, fifteen years later", Girard remarks that there was no particular reason for the name F: ...
9 votes
Accepted

Was counting complexity first introduced by Valiant in 1979?

Yes, the complexity class $\mathsf{\#P}$ is first introduced in Valiant's seminal paper "The complexity of computing the permanent." TCS, (1979). This is very clear. As for the terminology, strictly ...
  • 184
8 votes
Accepted

Does Rabin/Yao exist (at least in a form that can be cited)?

After more than two years, I have to assume the answer is "no". (Posting this stub answer so the question can be marked as answered.)
8 votes

When have we found better bounds for known algorithms?

The Logjam Attack mentions that analysis of the general number field sieve (as applied to computing discrete logarithms over $\mathbb{F}_p$) descent step was tightend, see top left of the 3rd page. As ...
  • 778
7 votes

Who introduced nondeterministic computation?

Rabin and Scott introduced the nondeterministic finite automata with their research paper published in IBM journal, April 1959. In the paper they mentioned: we have adopted an even simpler form of ...
7 votes

Are there any intersections between Theory A and Theory B?

One cool example of work that straddles things that are typically considered theory A and things typically considered theory B are the lower bounds on the running time of the simplex algorithm with ...
7 votes

Why is lambda calculus so "function" oriented?

The idea of how to 'mechanize mathematical proof' was a hot topic at the time; more specifically, Hilbert posed the Entscheidungsproblem - could we have a machine in some factory somewhere that takes ...
  • 2,305
6 votes

How exactly does lambda calculus capture the intuitive notion of computability?

You program in it! Take a look at church encodings. You can see how pretty much all arithmetic can be performed which should probably convince you that it is extremely powerful. I like to look at ...
  • 1,131

Only top scored, non community-wiki answers of a minimum length are eligible