Utilisations des catégories

Je ne suis pas un informaticien théorique. Je suis un théoricien stable de l'homotopie utilisant -categories. J'ai vu des applications de la théorie des catégories et de la théorie des topos à l'informatique théorique, et je me demandais s'il y avait un moyen d'utiliser -catégories (et de préférence pour moi, la théorie de l'homotopie stable) en informatique théorique. Je pense que HoTT pourrait être une telle application, mais je peux très bien me tromper parce que je ne connais pratiquement rien à HoTT. (Donc, je ne sais pas non plus comment HoTT est utilisé dans TCS.)∞$\infty$$\infty$

Appliquer des idées théoriques homotopiques plus élevées à CS est encore un domaine très naissant! Ma compréhension est que ce n'est même pas aussi ancien qu'un domaine mathématique.

Certes, HoTT est l'impulsion centrale pour de telles idées. Même là cependant, il n'y a eu que peu d'applications de la théorie des catégories de «dimension» supérieure à 2.

Une belle "science informatique" est la théorie des patchs homotopiques par Anguili et al . Ils montrent que certaines opérations et propriétés communes inhérentes gitaux systèmes de contrôle de version peuvent être mieux comprises en utilisant la théorie des types d'homotopie.

Un autre courant de pensée plutôt indépendant est un travail intéressant sur la relation entre la théorie de l'homologie (2-) et la confluence des systèmes de réécriture des termes (ou des structures plus complexes telles que les algèbres supérieures). Quelques exemples sont

Y. Guiraud Confluence de la réécriture linéaire et de l'homologie des algèbres .

Y. Lafont & A. Proute Propriété de Church-Rosser et homologie des monoïdes .

Les informaticiens théoriques font beaucoup de choses, dont la modélisation mathématique de diverses choses de compétence informatique. Par exemple, nous aimons fournir des modèles mathématiques de langages de programmation, afin que les gens puissent réellement prouver des choses sur les programmes (comme prouver que le programme fait ce qu'il est censé faire). En ce sens, il est toujours bon d'avoir un bon approvisionnement en techniques mathématiques qui nous donneront des modèles pour diverses choses que les informaticiens proposent.

$D$$D \cong D^D$

$(\infty,1)$$\infty$

Le seul lien entre la théorie de l'homotopie stable et la théorie des types que je connaisse est le travail de Matthijs Vákár sur la théorie des types dépendants linéaires . Apparemment, un de ses modèles est la théorie de l'homotopie stable, mais celle-ci n'a pas encore été publiée, seulement suggérée à la fin de l'article lié.

Un autre endroit où vous pourriez rechercher des applications de la théorie de l'homotopie (stable ou non) en informatique est la topologie informatique . Là, l'homologie persistante a récemment trouvé de nombreuses utilisations, et les gens étudient sûrement des applications théoriques de l'homotopie d'un genre similaire. L'idée de base est d'utiliser la topologie algébrique pour étudier les propriétés de grands ensembles de données.

Il existe sans aucun doute d'autres applications. Cody a mentionné l'utilisation de la théorie de l'homotopie (sous le couvert de la théorie du type d'homotopie) pour étudier les systèmes de contrôle de révision. Il existe également des applications de la théorie de l'homotopie à l'étude des calculs parallèles et cuncurrents, comme la " topologie algébrique et la concurrence ". Quelqu'un de plus compétent peut avoir la gentillesse de fournir de meilleures références. Dans tous les cas, vous remarquerez que toutes ces applications (à l'exception peut-être de la théorie des types d'homotopie) sont assez simples d'un point de vue mathématique - ce qui ne veut pas dire qu'elles ne valent rien!

cela tente d'esquisser des liens plus généraux. une partie de ce programme peut être considérée comme une extension très récente et plus élaborée de l'ancienne correspondance Curry-Howard notée entre les preuves et les programmes. il existe également un lien étroit avec la démonstration automatisée des théorèmes (aka assistants de preuve). de nombreuses techniques utilisées dans les preuves de théorèmes automatisées ne reposent pas sur des bases mathématiques entièrement solides et la théorie de l'homotopie ajoute une mise à la terre plus ferme.

cette proposition par une équipe importante capture / étudie une grande partie des connexions actuellement connues avec CS: Théorie des types d'homotopie: Fondements unifiés des mathématiques et du calcul (Proposition MURI)

Licata de cette équipe s'intéresse particulièrement aux applications informatiques de la théorie de l'homotopie. certains de ses discours, et un par Voevodsky fondateur de l' axiome hors concours Univalence :

• Applications mathématiques et informatiques de la théorie des types d'homotopie. Colloque à l'Université de l'Iowa. Novembre 2013. [ slides ]

• Preuves vérifiées par ordinateur dans la logique de la théorie de l'homotopie. Conférence invitée à la réunion nord-américaine de l'Association for Symbolic Logic. Mai 2013. [ slides ]

• Programmation et démonstration de la théorie des types d'homotopie. Colloque à Wesleyan, Princeton et Cornell. Printemps 2013. [ slides ]

• Informatique et théorie de l'homotopie , conférence vidéo de 10 m par Voevodsky / IAS