De beaux résultats dans TCS

Récemment, un de mes amis (travaillant dans TCS) a mentionné dans une conversation qu '"il voulait voir / connaître tous (ou autant que possible) les beaux résultats dans TCS au cours de sa vie". Cela m'a fait me questionner sur les beaux résultats dans ce domaine et donc sur la motivation pour la question suivante:

Quels résultats (ou idées), à votre avis, sont beaux en informatique théorique? Ce serait formidable si vous mentionniez également la raison. [Serait également très bien même si les idées proviennent des mathématiques, mais ont suscité de l'intérêt et trouvé des utilisations dans TCS]

Je commencerais par une réponse comme argument diagonal de Cantor parce que c'est un résultat simple, élégant et pourtant puissant.

L'indécidabilité du problème de l'arrêt.

Beau pour de nombreuses raisons. C'est un résultat impossible. La preuve utilise la diagonalisation. L'énoncé s'applique à un large éventail de modèles de calcul. Il peut être formulé de différentes manières, en particulier en utilisant des langages de programmation standard. Ce fut un résultat décisif dans l'histoire de l'informatique. L'extension de cette déclaration conduit au théorème de Rice, aux degrés de Turing et à de nombreux autres résultats intéressants. Etc. Etc. Etc.

À mon avis, la correspondance Curry-Howard est l'un des plus beaux résultats théoriques, et celui qui m'a poussé à faire des recherches.

L'idée que deux systèmes, programmes d'une part, et preuves d'autre part, ont exactement la même structure, est presque de nature philosophique: existe-t-il des "schémas de raisonnement" généraux?

La possibilité d'une cryptographie à clé publique, par exemple, le système d'échange de clés Diffie-Hellman.

Cela brise la très forte idée préconçue que les gens doivent rencontrer avant d'échanger des secrets sur un canal non sécurisé.

J'ai été et suis toujours surpris par l'algorithme d'Euclide. Pour moi, c'est un témoignage de la puissance de la pensée humaine - que les gens pourraient concevoir un tel algorithme si tôt (environ 300 avant JC si j'ai confiance en ma mémoire).

Avance rapide, il existe une littérature angoissante sur le sujet. Je pense que la liste de Scott Aaronson devrait être utile à cet égard - cependant, comme Aaronson lui-même dit qu'elle n'est pas complète (et pas entièrement théorique)

La technique de Yao pour utiliser le théorème de Minmax de von Neumann pour prouver les limites inférieures des algorithmes randomisés. Je le trouve comme quelque chose hors de ce monde.

Méthode probabiliste pour prouver l'existence d'objets que nous avons du mal à construire dont le lemme local de Lovasz. Ces techniques sont si simples, mais si puissantes.

Constructions de la théorie de codage de Madhu Soudan à l'aide de polynômes.

Expanseurs (cela a commencé comme des graphiques Ramanujan) et extracteurs et leurs applications en pseudo-aléatoire.

Algorithme de transformation de Fourier rapide de Cooley et Tukey pour trouver la DFT. (Bien que, comme le supposait Tukey, il s'agissait d'une redécouverte d'une technique bien connue, du moins connue de Gauss!)

Théorème de Barrington, (un résultat très surprenant en son temps)

Théorème de répétition parallèle (bien que le résultat soit agréable, la preuve n'est pas facile)

Fonction de Lovasz Theta pour estimer la capacité en shannon d'un graphe.

Algorithme ellipsoïde qui a montré que LP est en P, surprenant beaucoup à un moment où beaucoup soupçonnaient encore qu'il pourrait être NP-Complete.

étonnamment, l'une des réponses les plus évidentes n'a pas encore été ajoutée. parfois on travaille trop avec quelque chose pour le voir de façon impartiale. la théorie de la complétude du NP lancée par Cook / Levin et immédiatement amplifiée par Karp qui a donné une indication précoce de son omniprésence, encore plus prémonitoire rétrospectivement. à bien des égards, c'est la naissance du TCS moderne et de la théorie de la complexité, et sa question centrale / clé / notoire P =? NP est toujours ouverte après quatre décennies d'études / d'attaques intenses. P =? NP a un prix Claymath de 1 M $ pour sa solution.

la preuve Cook a introduit le NDTM qui n'est apparemment pas du tout une simple curiosité théorique mais une partie presque extrêmement fondamentale du TCS. lancé un millier de navires, pour ainsi dire. de plus, il résiste / défie continuellement les efforts via l'une des autres techniques TCS clés / puissantes mentionnées dans cette liste, la diagonalisation, vue par exemple dans les résultats BGS-75 Oracle / Relativization - suggérant qu'il doit y avoir quelque chose d'exotique et de différent dans tout possible solution, également suggérée / développée par le document Razborov-Rudich Natural Proofs (prix Godel 2007).

il y a beaucoup, beaucoup d'arbitres sur le sujet, mais un plus récent avec un compte de première main de l'histoire peut être trouvé dans la question P =? NP et la lettre perdue de Godel par RJ Lipton

Complexité de Kolmogorov et méthode d'incompressibilité .

La méthode de l'incompressibilité - basée sur la complexité de Kolmogorov - a fourni une nouvelle façon intuitive de formuler des preuves. Dans une preuve typique utilisant la méthode de l'incompressibilité, on choisit d'abord un objet incompressible dans la classe en discussion. L'argument dit invariablement que si une propriété souhaitée ne tient pas, alors, contrairement à l'hypothèse, l'objet peut être compressé et cela résout la contradiction requise.

Voir par exemple la preuve qu'il existe un nombre infini de nombres premiers, la preuve alternative du théorème d'incomplétude de Godel, ou les connexions entre la complexité de Kolmogorov et la complexité informatique , ...

J'ai été (et je suis toujours) étonné par le deuxième théorème de récurrence de Kleene . En surface, cela semble simple et pas très utile, mais j'ai découvert plus tard que c'était profond à la fois mathématiquement et philosophiquement.

Quand j'ai également lu la variante éprouvée sur les machines de Turing (déclarant très très informellement que les machines peuvent obtenir leurs propres descriptions ou de manière équivalente qu'il existe des machines qui produisent leur propre description, comme un programme qui s'imprime ..), j'ai senti mon cerveau se tordre si dur, mais intrigué comme jamais auparavant. Ensuite, vous voyez comment le théorème est utilisé pour fournir des preuves sur une ligne pour l'indécidabilité du problème d'arrêt et la méconnaissance des machines minimales .. etc.

Théorèmes de codage source et canal de Shannon.

Une définition mathématique qui faisait la distinction entre le transmis, le récepteur et le support et qui ignorait la sémantique du message était un grand pas. L'entropie, dans le contexte des données, est une notion extrêmement utile. Et parce que la théorie de l'information devrait être mieux connue.

Un beau résultat qui s'appuie sur le théorème du PCP indique qu'il est difficile sur le plan du calcul (NP-difficile) de satisfaire plus de 7/8 des clauses de la formule 3SAT même pour des clauses satisfaisantes.

algorithme shors pour la factorisation en BQP . à mon avis / mémoire, le calcul quantique n'était plus qu'une curiosité théorique jusqu'à ce résultat en 1994, moment où il semble que la littérature et l'intérêt pour la recherche sur l'informatique QM aient explosé. c'est sans doute l'un des algorithmes QM les plus importants connus. remporte le prix Gödel 1999. il révèle également que l'affacturage dans le calcul QM est en fait dans un sens un peu mieux compris que dans l'informatique classique où par exemple la question de savoir si l'affacturage est NP complet est toujours ouverte.

me semble que le test de primalité AKS P-time est assez beau à divers égards. une percée à l'époque, l'une des grandes mais plutôt rares percées observées dans la théorie de la complexité de notre vivant. il résout un problème remontant à l'antiquité grecque et concerne certains des premiers algorithmes inventés (tamis d'ératosthène), c'est-à-dire l'identification efficace des nombres premiers. C'est une preuve constructive que la détection de primalité est en P par opposition à de nombreuses grandes preuves qui sont malheureusement non constructives.

son interconnecté à l'algorithme de cryptographie RSA mentionné dans une autre réponse parce que cet algorithme doit trouver rapidement de grands nombres premiers, avant l'algorithme AKS, cela n'était possible que de manière probabiliste. son fondamentalement lié à la théorie des nombres et à d'autres problèmes profonds, par exemple la conjecture de Riemann qui, à bien des égards, est le domaine original de l'algorithmique.

reçoit le prix Gödel 2006 et le prix Fulkerson 2006

Je pense que le théorème des graphes mineurs de Robertson et Seymour était la plus merveilleuse des théories que j'aie jamais vues (et partiellement lues). Tout d'abord, c'est assez compliqué, mais les conjectures de base ne sont pas difficiles et tout le monde travaillant dans TCS peut les deviner. Leur effort extrême pour les prouver était merveilleux. En fait, après avoir lu certains des articles de cette série, je comprends le pouvoir de l'esprit humain.

Le théorème des graphes mineurs a également un grand impact sur différents domaines du TCS. Comme la théorie des graphes, l'algorithme d'approximation, les algorithmes paramétrés, la logique, ...

L'une de mes familles de résultats préférées est que divers problèmes de nature apparemment infinie sont décidables.

1. La théorie du premier ordre des champs fermés réels est décidable (par Tarski). La géométrie euclidienne est également un modèle des axiomes des champs réels fermés, par conséquent, par Tarski, les déclarations de premier ordre dans ce modèle sont décidables.
2. L'arithmétique du presburger est décidable.
3. La théorie du premier ordre des champs algébriquement fermés (cela inclut les nombres complexes) est décidable.
4. La logique monadique du second ordre sur des mots infinis (et finis) est décidable. La preuve est élégante et peut être enseignée aux étudiants de premier cycle.

Il y a beaucoup de beaux résultats sur les algorithmes probabilistes, qui sont d'une simplicité trompeuse et un grand pas en avant dans notre façon de penser le calcul.

astuce de von Neumann pour mettre en œuvre une pièce équitable avec une pièce biaisée. Nous sommes tellement habitués aux algorithmes probabilistes maintenant, mais d'un point de vue extérieur, c'est incroyablement cool. L'algorithme et la preuve sont accessibles à tous ceux qui connaissent les probabilités au secondaire.

Le résultat de Tim Griffin qui contrôle des opérateurs tels que ceux call/ccliés à la logique classique, étendant la correspondance Curry-Howard.

call/cc$E$$\neg\neg \tau$$\mathtt{call/cc}{(E)}$$\tau$$\neg\tau$$\tau\rightarrow\bot$$\tau$

Son article , "A Formulas-as-types notion of control", paraît dans POPL 1990.

Mon préféré est l'algorithme de temps linéaire de Rabin pour calculer la paire de points la plus proche dans le plan (ou plus précisément sa simplification). Il montre l'importance du modèle de calcul, la puissance des algorithmes randomisés et une manière élégante de penser aux algorithmes randomisés.

Cela dit, CS est encore loin d'atteindre le niveau d'élégance que l'on rencontre en mathématiques (enfin, ils avaient 5000 ans d'avance), des définitions / résultats de base en calcul, en topologie (théorèmes à point fixe), en combinatoire, en géométrie (théorème de Pythagore http : //en.wikipedia.org/wiki/File: Pythag_anim.gif ), etc.

Si vous recherchez la beauté, cherchez-la partout ...

Ce résultat est probablement un peu récent pour être qualifié de fondamental, mais je crois que l' interprétation des types-comme-homotopies est admissible. Cette vue permet d'interpréter les types de la théorie des types constructifs comme des ensembles avec certaines propriétés géométriques, dans ce cas l' homotopie .

Je trouve que ce point de vue est particulièrement beau car il rend simples certaines observations auparavant complexes sur la théorie des types, par exemple le fait que "l'axiome K" n'est pas dérivable .

Un aperçu de ce domaine en herbe par Steve Awodey peut être trouvé ici .

La preuve de la connaissance zéro est un concept très intéressant. Il permet à une entité, le prouveur, de prouver (avec une forte probabilité) à une autre entité, le vérificateur, qu'elle connaît "un secret" (une solution à un problème NP, une racine carrée modulaire d'un certain nombre, un discret journal d'un certain nombre, etc…) sans donner aucune information sur le secret (ce qui est difficile à première vue, car la première idée pour prouver que vous connaissez un secret est de dire le secret, et que toute communication qui pourrait entraîner le vérificateur croyant que vous connaissez le secret ne peut a priori qu'augmenter sa connaissance du secret).