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 ...
- 18.1k
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 ...
- 18.1k
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 ...
- 726
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 ...
- 10.5k
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,...
- 23.9k
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 ...
- 27k
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 ...
- 36.1k
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 ...
- 4,511
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 ...
- 2,754
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"...
- 5,504
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^...
- 4,511
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 ...
- 6,754
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 ...
- 23.9k
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 ...
- 79
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 ...
- 18.1k
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