3
$\begingroup$

I was recently listening to Sean Carroll's interview with Scott Aaronson, and the two of them briefly talked about surprises in their respective fields (theoretical and particle physics, and theoretical computer science). They both agreed that some surprises would be so abnormal that they would be immediately suspicious, while other, less earth-shattering surprises have indeed happened in both of their fields.

I guess superluminal neutrinos, respectively the collapse of the polynomial hierarchy, would be in the first category, while Madame Wu's experiment showing violation of P-symmetry, respectively the proof of IP=PSPACE, have a similar feel as representatives of the second category. I was thinking that theoretical physicists coyly ask "who ordered that" when they have evidence that requires a significant update in their priors.

I think perhaps Impagliazzo and Wigderson's results on P and BPP (and, analogously, NP and AM) have a similar vibe and gave many theoretical computer scientists pause. What other theoretical computer science results have that same feel?

$\endgroup$
2
  • 4
    $\begingroup$ Candidates: PRIMES in P, PCP theorem, Ramanujan expanders, Unique Games. $\endgroup$
    – usul
    Jan 26 at 20:34
  • $\begingroup$ Thanks! Was the derandomization of PRIMES surprising? (AKS is brilliant and rightfully deserves all the praise of course… with some analogy to LIGO’s discovery…) $\endgroup$
    – Mark S
    May 13 at 2:11

2 Answers 2

3
$\begingroup$

Taking a liberal view of TCS, I can think of the following, all of which have profound influence on theoretical and practical computing.

  • The Spectre vulnerability (which undermines speculation, a (the) core principle behind the performance of all modern CPUs).
  • Strassen's fast matrix multiplication algorithm.
  • Scott's model of the untyped $\lambda$-calculus.
  • Gödel's incompleteness theorems.

An additional surprise, but not a single result, is the usefulness of SAT/SMT solvers in practice, which has lead to the the surprising realisation that SAT is the paradigm case of a feasible complexity class. TCS has not yet caught up with this.

$\endgroup$
5
  • 1
    $\begingroup$ For Dana Scott, he told me he was developing semantics of typed languages to show people how and why types were advantageous – but his setup also turned out to give semantics to the untyped ones. So, that's definitely a surprise, but he wasn't "trying to prove the opposite" (which would be "the untyped λ-calculus does not have a semantics"). $\endgroup$ Jan 28 at 10:04
  • $\begingroup$ @AndrejBauer That's interesting. I seem to recall having read somewhere that Scott tried to prove that the impossibility of such a model from the set-theoretic fact that no interesting set $D$ and be isomorphic to its own function space (set theoretically). You have a much better connection to Dana Scott than me, so I've removed the remark about trying to prove the opposite. $\endgroup$ Jan 28 at 10:11
  • 1
    $\begingroup$ Well, he never told me that he didn't try to prove non-existence of the model, but I would be surprised. Since it had been known from Church-Rosser that the $\lambda$-calclus is consistent, it would have a model on general grounds (the Lindenbaum-Tarski algebra, more or less). I asked Dana something along the lines of "but Church-Rosses tells us $\lambda$-calculus is consistent", to which his response was "but what does it mean?" So I think it's more about findin the right kind of model than just any model. $\endgroup$ Jan 28 at 10:15
  • $\begingroup$ @AndrejBauer Maybe you can ask him? $\endgroup$ Jan 28 at 10:20
  • 1
    $\begingroup$ Sure, I can do it. $\endgroup$ Jan 28 at 10:50
2
$\begingroup$

Robin Milner's $\nu$ operation, which abstracts and axiomatises the ability to generate fresh names at will in a (quasi-)compositional way.

Naming is a long-standing problem in computer science. Most programming languages can define naming constructs, which, when called, yield a fresh name. This seemed like a completely marginal issue, and was given little attention. After all, you could implement it as a global variables. But only with Milner's axiomatisation, and use in $\pi$-calculus, were the profound structural implications of free name generations discovered, including how we approach the mechanised foundations of mathematics (e.g. nominal logic).

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.