144
I have to admit (surprising as it sounds) that I don't know really the answer. I either discovered or rediscovered this reduction myself.
I discovered the discrete log algorithm first, and the factoring algorithm second, so I knew from discrete log that periodicity was useful. I knew that factoring was equivalent to finding two unequal numbers with equal ...
100
$\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) ...
63
If you really want to know what led Neil Robertson and me to tree-width, it wasn't algorithms at all. We were trying to solve Wagner's conjecture that in any infinite set of graphs, one of them is a minor of another, and we were right at the beginning. We knew it was true if we restricted to graphs with no k-vertex path; let me explain why. We knew all such ...
55
The random reduction from factorization to order-finding (mod N) was very well known to people working in number theory algorithms in the late 1970's and early 1980's. Indeed, it appears in a paper of Heather Woll, Reductions among number theoretic problems, Information and Computation 72 (1987) 167-179, and Eric Bach and I knew it before then.
I am ...
35
This paper, in Russian,
Gricenko, S. A., Karatsuba, E. A., Korolyov, M. A., Rezvyakova, I. S.,
Tolev, D. I., & Changa, M. E. (2012). Scientific contributions of A. A.
Karatsuba / Научные достижения Анатолия Алексеевича Карацубы.
Современные проблемы математики, 16(0), 7-30.
states the following (items 1—3).
Karatsuba presented his algorithm ...
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.
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
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 of the metric theory of tensor product spaces", and published it in a now famous paper in 1958, in French, in a limited circulation Brazilian journal. The paper ...
26
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 the untyped lambda calculus (or combinatory logic) and interpret $XZ$ as expressing "$Z$ satisfies the predicate $X$" and $\Xi XY$ as expressing "$X\subseteq Y$". ...
25
I've asked Dick personally out of curiosity a few years back. He said that as far as he knows Rabin-Karp was a random switch many years after the paper was first published. He also indicated that it is his understanding that Michael would say the same thing if asked, since at some point they had talked about it.
24
[Following a suggestion of Kaveh, I am putting my (somewhat extended) comment as an answer]
This "conjecture" of Kolmogorov is just a rumor. It was not published anywhere. In the former USSR, "publishing" mathematics meant something different than what it does today: give a talk at a seminar or tell your colleagues at lunch. Counting papers was not an issue....
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 ...
23
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, it was invented by Galler and Fischer2, but this seems to be incorrect, as they did not have all the components of the algorithm needed to make it run that ...
22
The footnote of my paper that you cite refers to a heuristic "argument" as well, at least, what we think was Kolmogorov's intuition -- the positive resolution of Hilbert's thirteenth problem.
http://en.wikipedia.org/wiki/Hilbert's_thirteenth_problem
In particular, it was proved by Kolmogorov and Arnold that any continuous function on $n$ variables can be ...
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 ...
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
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 can also talk about $SL_m$, but it's just a little cleaner to state the results when $m=3$.)
Went from non-constructive proof of finiteness, to computable, to ...
18
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 theory, where $X\subseteq \{ \text{simple},$ $\text{dependent},$ $\text{polymorphic},$ $\text{higher-order}\}$) based on the categorical notion of Grothendieck ...
18
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 the invention of the Prolog language.
17
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 research field, with a competition (the POPLmark challenge) some years ago. There are even jokes by people in the field about the complexity of approaches to ...
17
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 reductions to show that $SAT$ is $\mathbb{NP}$-complete, in the modern sense of the term.
As for whether Cook understood the significance of a $\mathbb{NP}$-...
17
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 answered negatively by Turing in his famous 1936 paper "On Computable Numbers, with an application to the Entscheidungsproblem". The word literally means ...
14
An $\omega$-regular language is actually quite low in the Borel hierarchy (inside $\Delta_3$), a result due to
R. McNaughton, Testing and generating infinite sequences by a finite automaton, Information and Control 9 (1966), 521-530.
For a proof and more details, you can look at Chapter 3 of the following book
D. Perrin et J.-É. Pin, Infinite words, ...
14
There are two loanable copies at The National Library of Israel.
Here is a scanned copy.
14
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". The class $\Pi_1^P$ in there is of course coNP. Stockmeyer wrote a full paper on the polynomial hierarchy (TCS 1977) which also uses the notation coNP.
13
Your questions can be approached from many sides. I'd like to leave the historical and philosophical aspects on the side and address your main question, which I take to be this:
What's the point of lambda calculus? Why go through all these functions/reductions?
What is the point of Boolean Algebra, or Relational Algebra, or First-Order Logic, or Type ...
13
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 thinking of how it would run on a Turing Machine.
However, Turing Machines are excellent for reasoning about. In Theoretical Computer Science, we're interested ...
12
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 hypothesis over finite fields coming from the Weil conjectures can be thought of as asking questions which originally had fruitful results from Grothendieck's etale ...
12
Turing argued that Mathematics can be reduced to a combination of reading/writing symbols, chosen from a finite set, and switching between a finite number of mental 'states'. He reified this in his Turing Machines, where symbols are recorded in cells on a tape and an automaton keeps track of the state.
However, Turing's machines are not a constructive proof ...
12
Nobody has yet mentioned directed algebraic topology, which was in fact developed to provide a suitable algebraic topological toolbox for the study of concurrency.
There are also several low dimensional topological approaches to topics in the theory of computation, all fairly new:
Various approaches to fault-tolerant anyonic quantum computation based on ...
Only top voted, non community-wiki answers of a minimum length are eligible