Interprétation géométrique du calcul

Étant issu de la physique, j'ai été formé pour étudier de nombreux problèmes d'un point de vue géométrique. Par exemple la géométrie différentielle des variétés dans les systèmes dynamiques, etc. Quand je lis les fondements de l'informatique, j'essaie toujours de trouver des interprétations géométriques. Comme une interprétation géométrique plausible d'ensembles récursivement énumérables (j'ai travaillé sur une partie où j'ai essayé de les relier à la géométrie algébrique en exploitant l'équivalence avec les ensembles diophantiens mais la connexion semblait forcée et je n'ai pas pu trouver une expression "naturelle" des faits dans ce formulation) ou un beau résultat géométrique pour un algorithme simple de tri des nombres. Bien que je ne sois pas un expert, j'ai lu des enquêtes sur la théorie de la complexité géométrique et c'est sûrement un programme intéressant, mais je suis plus intéressé à avoir une vue géométrique de concepts extrêmement fondamentaux comme la dynamique d'une machine de Turing, le calcul Lambda ou la structure de ( ensembles non calculables (plutôt que problèmes spécifiques). Est-ce un travail désespéré de trouver une structure géométrique dans ces objets ou peut-on s'attendre à des résultats complexes? Existe-t-il une formulation du TCS qui le traite géométriquement?

La sémantique des programmes informatiques peut être comprise géométriquement de trois manières distinctes (et apparemment incompatibles).

• L'approche la plus ancienne est via la théorie des domaines . L'intuition derrière la théorie des domaines provient de l'asymétrie derrière la terminaison et la non-terminaison.

  Lorsque vous traitez des programmes de manière étendue (c'est-à-dire en ne regardant que leur comportement d'E / S et non leur structure interne), il est toujours possible de confirmer en temps limité qu'un programme s'arrête - il suffit d'attendre qu'il s'arrête. Cependant, il n'est pas possible de confirmer qu'un programme ne s'arrête pas , car peu importe le temps que vous attendez, il existe toujours un programme d'arrêt qui s'exécutera pendant quelques étapes de plus que ce que vous avez attendu.

  En conséquence, l'arrêt et la boucle peuvent être considérés comme formant un espace topologique ( l'espace Sierpiński ). Cela soulève des notions plus riches d'observation (via la topologie de Scott), et vous pouvez ainsi interpréter les programmes comme des éléments d'espaces topologiques. Ces espaces sont généralement assez surprenants d'un point de vue traditionnel - les domaines ne sont généralement pas Hausdorff.

  La meilleure introduction topologique que je connaisse à ces idées est la topologie courte et extrêmement accessible de Steve Vickers via Logic . Cela peut être compris comme une sorte d'échauffement pour les espaces de pierre beaucoup plus formidables de Peter Johnstone .

  Si vous recherchez des notes de cours en ligne, permettez-moi de suggérer la topologie synthétique des types de données et des espaces classiques de Martin Escardo .

• Un autre point de vue découle de la théorie de la concurrence. Un programme simultané peut être compris comme ayant plusieurs exécutions valides (séquences d'états), selon la façon dont les races sont résolues. Ensuite, l'ensemble des exécutions peut être considéré comme un espace, chaque séquence possible d'états étant comprise comme un chemin à travers cet espace. Ensuite, des méthodes issues de la topologie algébrique et de la théorie de l'homotopie peuvent être appliquées pour dériver des invariants concernant l'exécution du programme.

  Nir Shavit et Maurice Herlihy utilisent cette idée pour prouver l'impossibilité de certains algorithmes distribués, pour lesquels ils ont remporté le prix Gödel 2004. (Voir La structure topologique du calcul asynchrone .) Eric Goubault a un document d'enquête expliquant les idées pertinentes dans Some Geometric Perspectives in Concurrency Theory .

• Plus récemment, il a été observé que la structure du type d'identité dans la théorie des types dépendants correspond très étroitement à la notion de type homotopique dans la théorie de l'homotopie - si étroitement, en fait, que la théorie des types dépendants peut en fait être considérée comme une sorte de "théorie synthétique de l'homotoptie"! (Vladimir Voevodsky a plaisanté en disant qu'il a passé plusieurs années à développer un nouveau calcul pour la théorie de l'homotopie, pour découvrir que ses collègues du département CS l'enseignaient déjà aux étudiants de premier cycle.)

  Voir le lien de cody ci-dessus vers le livre de théorie des types d'homotopie .

Fait intéressant, ces trois points de vue semblent incompatibles, ou du moins très difficiles à concilier. La théorie des types dépendants est un langage total, donc la non-terminaison (et la topologie de Scott) n'y survient pas. Il est également confluent, de sorte que la vue des calculs en tant qu'espaces ne se pose pas non plus. De même, la formulation de la concurrence en termes de théorie des domaines s'est révélée férocement difficile, et un compte complètement satisfaisant reste un problème ouvert.

Comme cela se produit, il y a eu récemment un développement dans la théorie des types dépendants , dans laquelle un type, qui représente traditionnellement un invariant statique pour un programme informatique, peut être interprété comme un espace topologique, ou plutôt une classe d'équivalence de tels des espaces ( type homotopique ).

Cela a fait l'objet d'intenses recherches au cours des dernières années, qui ont abouti à un livre .

Des travaux plus anciens ont tenté de donner une description de modèles de systèmes de calcul, comme le pur$\lambda$ -calculus , en termes de certains espaces topologiques appelés domaines . L' article de Wikipedia donne un bon aperçu.

Vous connaissez GCT, mais vous ne connaissez peut-être pas les travaux antérieurs de Mulmuley sur la démonstration d'une séparation entre un sous-ensemble de calculs PRAM et P, qui utilise des idées géométriques sur la façon dont un calcul peut être considéré comme découpant un espace.

De nombreuses limites inférieures pour les problèmes du modèle d'arbre de décision algébrique se réduisent à un raisonnement sur la topologie des espaces sous-jacents de solutions (les nombres de Betti apparaissent comme un paramètre pertinent).

Dans un sens, TOUTES les optimisations sont géométriques: les programmes linéaires impliquent de trouver le point le plus bas d'un polytope dans des dimensions élevées, les SDP sont des fonctions linéaires sur l'espace des matrices semi-finies, etc. La géométrie est largement utilisée dans la conception d'algorithmes ici.

Sur ce thème, il existe un lien long et profond entre notre capacité à optimiser certaines fonctions sur les graphiques et notre capacité à intégrer des espaces métriques dans certains espaces normés. C'est une vaste littérature maintenant.

Enfin, au cours des dernières années, il y a eu un grand intérêt pour les mécanismes dits «de levage et de projet» pour résoudre les problèmes d'optimisation, et ceux-ci font un usage intensif de la géométrie sous-jacente et des ascensions vers des espaces de dimension supérieure: les notions de la géométrie algébrique jouent un rôle important ici.

$T_1$ ). Ils sont "dirigés" dans un sens, il faudrait donc trouver une géométrie dirigée pour tenir compte du phénomène. Et il y a des tours à jouer qui symétrisent la situation (essentiellement vous vous tenez debout).

Une façon de comprendre la relation entre le traitement de l'information (également appelé "calcul") et la géométrie est que le traitement de l'information est une géométrie antérieure . Ce point de vue devrait être familier de certaines parties de la physique. Par exemple, dans la théorie de la relativité, nous étudions à la fois la structure causale de l'espace-temps (son traitement de l'information) ainsi que sa structure géométrique . Beaucoup considéreraient ce dernier comme plus fondamental que le premier.

Ces connexions ont été remarquées dans le passé et il y a plusieurs années, un effort a été fait pour relier les aspects théoriques de l'information de l'informatique à la théorie de la relativité. L'une des tâches que les gens voulaient résoudre était: à partir de la structure de causalité de l'espace-temps (qui n'est qu'un ordre partiel sur l'espace-temps), reconstruire la topologie de l'espace-temps, ou peut-être aussi la géométrie. La récupération de la topologie à partir d'un ordre partiel est le genre de chose dans laquelle la théorie des domaines est bonne, donc il y a eu un certain succès.

Les références:

• Structures de calcul pour la modélisation de l'espace, du temps et de la causalité , Dagstuhl Seminar 06341, 20–25 août 2006

• Key Martin et Prakash Panangaden: géométrie de l' espace-temps à partir de la structure causale et d'une mesure

$U$

en interprétant de manière créative votre question, certaines possibilités autres que GCT, comme vous le mentionnez, vous viennent à l'esprit. une façon consiste à rechercher des problèmes indécidables (alias l'exhaustivité de Turing) qui sont assez omniprésents.

• Carrelage apériodique Plan & Carrelage Penrose . il a été prouvé que la question de savoir s'il existe un pavage apérodique de l'avion est indécidable.

• Les automates cellulaires qui sont également de plus en plus connus pour avoir des liens profonds avec la physique, de nombreux problèmes indécidables associés, une MT éprouvée et complète, et ils sont naturellement interprétés comme (et convertis entre) des tableaux de calcul TM.

• $(x,y)$

• Indécidabilité dans les systèmes dynamiques (Hainry), là encore parfois étroitement liée à la physique. les systèmes dynamiques ont généralement une interprétation géométrique multidimensionnelle.

• Langages de programmation visuels . un programme peut être vu comme un type de graphe (dirigé?) avec différents types de sommets (par exemple conditionnel, opération arithmétique), etc.