Verwendung von

Ich bin kein theoretischer Informatiker. Ich bin ein stabiler Homotopietheoretiker mit Kategorien. Ich habe Anwendungen der Kategorietheorie und der Topos-Theorie in der theoretischen Informatik gesehen und mich gefragt, ob man in der theoretischen Informatik ∞- Kategorien (und für mich bevorzugt die stabile Homotopietheorie) verwenden kann. Ich denke, HoTT könnte eine solche Anwendung sein, aber ich kann mich sehr gut irren, weil ich so gut wie nichts über HoTT weiß. (Also weiß ich auch nicht, wie HoTT in TCS verwendet wird.)$\infty$$\infty$

Das Anwenden höherer homotopietheoretischer Ideen auf CS ist immer noch ein sehr junges Gebiet! Ich verstehe, dass es nicht einmal so alt ist wie ein mathematisches Feld.

Sicherlich ist HoTT der zentrale Anstoß für solche Ideen. Selbst dort gab es nur wenige Anwendungen der Kategorietheorie mit einer "Dimension" von mehr als 2.

Eine schöne "Informatik-y" ist Homotopical Patch Theory von Anguili et al . Sie zeigen, dass einige gebräuchliche Operationen und Eigenschaften gitwie Versionskontrollsysteme am besten mit der Homotopietypentheorie verstanden werden können.

Ein anderer, eher nicht verwandter Gedankengang ist eine interessante Arbeit über die Beziehung zwischen (2-) Homologietheorie und Zusammenfluss von Termumschreibungssystemen (oder komplexeren Strukturen wie höheren Algebren). Einige Beispiele sind

Y. Guiraud Zusammenfluss von linearer Umschreibung und Homologie von Algebren .

Y. Lafont & amp; A. Proute Church-Rosser-Eigenschaft und Homologie von Monoiden .

Theoretische Informatiker machen viele Dinge, eine davon ist die mathematische Modellierung verschiedener computerwissenschaftlicher Dinge. Zum Beispiel möchten wir mathematische Modelle von Programmiersprachen bereitstellen, damit die Leute tatsächlich Dinge über Programme beweisen können (zum Beispiel, dass das Programm das tut, was es soll). In diesem Sinne ist es immer gut, über ein gutes Angebot an mathematischen Techniken zu verfügen, die uns Modelle für verschiedene Dinge liefern, die sich Informatiker einfallen lassen.

$D$$D \cong D^D$ .

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

Die einzige Verbindung zwischen stabiler Homotopietheorie und Typentheorie, die mir bekannt ist, ist die Arbeit von Matthijs Vákár über linearen abhängigen Typentheorie . Anscheinend ist ein Modell davon eine stabile Homotopietheorie, aber dies wurde noch nicht veröffentlicht, nur angedeutet am Ende des verlinkten Artikels.

Ein weiterer Ort, an dem Sie nach (stabilen oder nicht stabilen) Anwendungen der Homotopietheorie in der Informatik suchen könnten, ist die Computertopologie . Dort hat die persistente Homologie in letzter Zeit viele Verwendungen gefunden, und die Leute suchen sicherlich nach homotopietheoretischen Anwendungen ähnlicher Art. Die Grundidee besteht darin, mithilfe der algebraischen Topologie die Eigenschaften großer Datensätze zu untersuchen.

Ohne Zweifel gibt es andere Anwendungen. Cody erwähnte die Verwendung der Homotopietheorie (in Form der Homotopietheorie) zur Untersuchung von Revisionskontrollsystemen. Es gibt auch Anwendungen der Homotopietheorie für das Studium paralleler und gleichzeitiger Berechnungen, wie " Algebraische Topologie und Nebenläufigkeit ". Jemand, der mehr darüber weiß, ist möglicherweise so freundlich, bessere Referenzen zu liefern. In jedem Fall werden Sie feststellen, dass alle diese Anwendungen (mit der möglichen Ausnahme der Homotopietheorie) aus mathematischer Sicht ziemlich einfach sind - was nicht bedeutet, dass sie wertlos sind!

Damit wird versucht, allgemeinere Zusammenhänge zu skizzieren. Ein Teil dieses Programms kann als eine sehr neue und aufwändigere Erweiterung der alten Curry-Howard-Korrespondenz angesehen werden , die zwischen Proofs und Programmen vermerkt ist. Es gibt auch eine enge Verbindung mit dem automatisierten Beweis von Theoremen (auch bekannt als Beweisassistenten). Viele Techniken, die für Beweise mit automatisierten Theoremen verwendet werden, basieren nicht auf soliden mathematischen Grundlagen, und die Homotopietheorie fügt eine festere Grundlage hinzu.

Dieser Vorschlag eines beträchtlichen Teams erfasst einen Großteil der derzeit bekannten Zusammenhänge mit CS: Homotopy Type Theory: Einheitliche Grundlagen von Mathematik und Berechnung (MURI-Vorschlag).

Die Lizenznehmer dieses Teams interessieren sich besonders für computerwissenschaftliche Anwendungen der Homotopietheorie. einige seiner Vorträge und eines von Voevodsky, dem Begründer des herausragenden Axioms der Univalenz :

• Mathematische und rechnergestützte Anwendungen der Homotopietypentheorie. Kolloquium an der Universität von Iowa. November 2013. [ Folien ]

• Computergeprüfte Beweise in der Logik der Homotopietheorie. Eingeladener Vortrag beim Treffen der Association for Symbolic Logic North American. Mai 2013. [ Folien ]

• Programmieren und Beweisen in der Homotopietypentheorie. Kolloquium in Wesleyan, Princeton und Cornell. Frühling 2013. [ Folien ]

• Informatik und Homotopietheorie , 10-m-Videovortrag von Voevodsky / IAS