Feste Anwendungen der Kategorietheorie in TCS?

Ich habe ein paar Teile der Kategorietheorie gelernt. Es ist sicherlich eine andere Sichtweise. (Sehr grobe Zusammenfassung für diejenigen, die es nicht gesehen haben: Die Kategorietheorie bietet die Möglichkeit, alle Arten von mathematischem Verhalten ausschließlich in Bezug auf funktionale Beziehungen zwischen Objekten auszudrücken. Beispielsweise werden Dinge wie das kartesische Produkt zweier Mengen vollständig in Bezug auf definiert wie sich andere Funktionen damit verhalten, nicht hinsichtlich der Elemente, die Mitglieder der Menge sind.)

Ich habe ein vages Verständnis dafür, dass Kategorietheorie auf der Seite der Programmiersprachen / Logik ("Theorie B") nützlich ist, und frage mich, wie viel Algorithmen und Komplexität ("Theorie A") davon profitieren könnten. Es könnte mir jedoch helfen, auf den Weg zu kommen, wenn ich einige solide Anwendungen der Kategorietheorie in Theorie B kenne. (Ich gehe implizit davon aus, dass es in Theorie A bisher keine Anwendungen gibt, aber wenn Sie einige davon haben, ist das eben Besser für mich!)

Mit "fester Anwendung" meine ich:

(1) Die Anwendung hängt so stark von der Kategorietheorie ab, dass es sehr schwierig ist, sie ohne den Einsatz der Maschine zu erreichen.

(2) Die Anwendung beruft sich auf mindestens ein nicht triviales Theorem der Kategorientheorie (zB Yonedas Lemma).

Es könnte gut sein, dass (1) (2) impliziert, aber ich möchte sicherstellen, dass dies "echte" Anwendungen sind.

Ich habe zwar etwas "Theorie B" -Hintergrund, aber es ist schon eine Weile her, daher wäre jede Entjargonisierung sehr willkommen.

(Abhängig davon, welche Art von Antworten ich bekomme, könnte ich diese Frage später in Community-Wiki umwandeln. Aber ich möchte wirklich gute Anwendungen mit guten Erklärungen, daher ist es eine Schande, die Antwortenden nicht mit etwas zu belohnen.)

Ich kann mir einen Fall vorstellen, in dem die Kategorietheorie direkt "angewendet" wurde, um ein offenes Problem in Programmiersprachen zu lösen: Thorsten Altenkirch, Peter Dybjer, Martin Hofmann und Phil Scott, "Normalisierung durch Auswertung für typisierte Lambda-Rechnung mit Koprodukten" . Aus ihrer Zusammenfassung: "Wir lösen das Entscheidungsproblem für einfach getippte Lambda-Berechnungen mit starken binären Summen, ebenso das Wortproblem für freie kartesische geschlossene Kategorien mit binären Nebenprodukten. Unsere Methode basiert auf der semantischen Technik, die als 'Normalisierung durch Auswertung' bekannt ist und beinhaltet die Interpretation der Syntax in ein geeignetes Garbenmodell umzukehren und daraus geeignete eindeutige Normalformen zu extrahieren. "

Im Allgemeinen denke ich jedoch, dass die Kategorietheorie normalerweise nicht angewendet wird, um tiefe Theoreme in Programmiersprachen zu beweisen (von denen es nicht so viele gibt), sondern stattdessen einen konzeptuellen Rahmen bietet, der oft nützlich ist (zum Beispiel im obigen Beispiel) Vorstellung von (Pre) Sheaf Semantik).

Ein wichtiges historisches Beispiel ist der Vorschlag von Eugenio Moggi, dass der Begriff Monade (der in der Kategorietheorie grundlegend und allgegenwärtig ist) als Teil einer semantischen Erklärung von Nebenwirkungen in Programmiersprachen (z. B. Zustand, Nichtdeterminismus) verwendet werden könnte. Dies hat auch zu Überlegungen zur Syntax von Programmiersprachen geführt, die beispielsweise direkt zur "Monad-Typenklasse" in Haskell führten (die zur Kapselung von Effekten verwendet wird).

In jüngerer Zeit (im letzten Jahrzehnt) wurde diese Erklärung von Effekten in Bezug auf Monaden unter dem Gesichtspunkt der alten Verbindung (hergestellt von Kategorietheoretikern in den 60er Jahren) zwischen Monaden und algebraischen Theorien überarbeitet: siehe Martin Hyland und John Power's , "Das kategorietheoretische Verständnis der universellen Algebra: Lawvere Theorien und Monaden" . Die Idee ist, dass die monadische Ansicht von Effekten mit der (in gewisser Weise ansprechenderen) algebraischen Ansicht von Effekten kompatibel ist, wobei Effekte (z. B. Speichern) in Form von Operationen (z. B. "Nachschlagen" und "Aktualisieren") erklärt werden können. und zugehörige Gleichungen (z. B. Idempotenz der Aktualisierung). Paul-André Melliès hat kürzlich ein Papiergebäude zu dieser Verbindung erstellt: "Segal-Bedingung trifft auf rechnerische Effekte"., das sich auch stark auf Ideen aus der "höheren Kategorietheorie" stützt (zum Beispiel den Begriff "Yoneda-Struktur" als Methode zur Organisation der Semantik vor der Gabe).

Eine weitere verwandte Klasse von Beispielen stammt aus der linearen Logik . Bald nach seiner Einführung durch Jean-Yves Girard in den 80er Jahren (mit dem Ziel eines besseren Verständnisses der konstruktiven Logik) wurden feste Verbindungen zur Kategorietheorie hergestellt. Für eine Erklärung dieser Verbindung siehe John Baez und Mike Stay, "Physik, Topologie, Logik und Berechnung: Ein Rosettastein" .

Schließlich wäre diese Antwort unvollständig, ohne auf Sigfpes aufschlussreichen Blog "Eine Nachbarschaft der Unendlichkeit" Bezug zu nehmen . Insbesondere können Sie sich "Eine Teilordnung einiger Kategorietheorien für Haskell" ansehen .

Quantenberechnung

Ein sehr interessantes Gebiet ist die Anwendung verschiedener monoidaler Kategorien auf die Quantenberechnung. Einige könnten argumentieren, dass dies auch Physik ist, aber die Arbeit wird von Leuten in Informatikabteilungen erledigt. Eine frühe Arbeit auf diesem Gebiet ist eine kategorische Semantik von Quantenprotokollen von Samson Abramsky und Bob Coecke; viele neuere Arbeiten von Abramsky und Coecke und anderen arbeiten in dieser Richtung weiter.

In diesem Werk werden die Quantenprotokolle als (bestimmte Arten von) kompakte geschlossene Kategorien axiomatisiert. Solche Kategorien haben eine schöne grafische Sprache in Form von String- (und Ribbon-) Diagrammen. Gleichungen in der Kategorie entsprechen bestimmten Bewegungen der Saiten, z. B. dem Glätten einer verwickelten, aber nicht geknoteten Saite, die wiederum etwas Sinnvollem in der Quantenmechanik entsprechen, z. B. einer Quantenteleportation.

Der kategoriale Ansatz bietet eine logische Übersicht über die typischen Berechnungen auf sehr niedriger Ebene.

Theorie der Systeme

$F$$F$

Graphtransformationen

$G_1,G_2$$P$$e_1:P\to G_1$$e_2:P\to G_2$$G_1$$G_2$$G_1$$G_2$$P$

$(L, K, R)$$L$$R$$K$$l:K\to L$$r:K\to R$$L\setminus K$$R\setminus K$$d$$K$$D$$d$$l$$G$$d$$k$

Programmiersprachen (über MathOverflow)

Es gab viele Anwendungen der Kategorietheorie im Design von Programmiersprachen und in der Programmiersprachtheorie. Ausführliche Antworten finden Sie auf MathOverflow. https://mathoverflow.net/questions/3721/programming-languages-based-on-category-theory ) https://mathoverflow.net/questions/4235/relating-category-theory-to-programming-language-theory .

Bigraphen - Prozesskalküle

Schließlich gibt es noch Milners Bigraphs , einen allgemeinen Rahmen für die Beschreibung und Argumentation von Systemen interagierender Agenten. Es kann als allgemeiner Rahmen für Überlegungen zu Prozessalgebren und ihren Struktur- und Verhaltenstheorien angesehen werden. Der Ansatz basiert auch auf Pushouts.

Ich gehe implizit davon aus, dass es in Theorie A noch keine Anwendungen gibt, aber wenn Sie einige davon haben, ist das noch besser für mich!

• Ich verstehe, dass Joyals Spezies-Theorie in der enumerativen Kombinatorik relativ häufig verwendet wird, um Funktionen zu verallgemeinern, die Ihnen zusätzlich sagen, wie man Dinge permutiert, und wie viele es gibt.

• Pippenger hat Stone Duality angewendet, um reguläre Sprachen und Sorten von Halbgruppen in Beziehung zu setzen. Jeandel hat topologische Automaten eingeführt, die diese Ideen anwenden, um einheitliche Konten (und Beweise!) Für Quanten-, Wahrscheinlichkeits- und gewöhnliche Automaten zu erstellen.

• Roland Backhouse hat mithilfe von Galois-Verbindungen zum tropischen Semiring abstrakte Charakterisierungen gieriger Algorithmen gegeben.

In einer viel spekulativeren Art erwähnte Noam Garbenmodelle. Diese charakterisieren abstrakt die syntaktische Technik der logischen Beziehungen, die wahrscheinlich eine der mächtigsten Techniken der Semantik ist. Wir verwenden sie meistens, um Unaussprechlichkeits- und Konsistenzergebnisse zu beweisen, aber es sollte für Komplexitätstheoretiker interessant sein, da es ein schönes Beispiel für eine praktische nicht-natürliche (im Sinne von Razborov / Rudich) Beweismethode ist. (Allerdings werden logische Beziehungen normalerweise sehr sorgfältig entworfen, um ihre Relativierung zu gewährleisten. Als Sprachdesigner möchten wir Programmierern versichern können, dass Funktionsaufrufe Black Boxes sind!)

EDIT: Ich werde weiterhin auf Ryans Bitte spekulieren. Nach meinem Verständnis handelt es sich bei einem natürlichen Beweis in etwa um einen Beweis, der versucht, eine induktive Invariante der Struktur eines Schaltkreises unter verschiedenen vernünftigen Bedingungen zu definieren. Ähnliche Ideen kommen (nicht überraschend) auch in Programmiersprachen häufig vor, wenn Sie versuchen, eine Invariante zu definieren, die induktiv durch einen Lambda-Kalkül-Ausdruck aufrechterhalten wird (um beispielsweise die Typensicherheit zu beweisen). 1

$A \to B$$A \to B$$A$

$A \to B$$A$$B$. Beachten Sie, dass es keine einzelne induktive Invariante gibt - wir definieren eine ganze Familie von Invarianten durch Rekursion über die Struktur der Eingabe und verwenden andere Mittel, um zu zeigen, dass alle Terme innerhalb dieser Invarianten liegen. Proof-theoretisch ist dies eine weitaus stärkere Technik, mit der Sie Konsistenzergebnisse nachweisen können.

Die Verbindung zu Garben ergibt sich aus der Tatsache, dass wir häufig über offene Begriffe (dh Begriffe mit freien Variablen) nachdenken müssen und daher unterscheiden müssen, ob wir aufgrund von Fehlern stecken bleiben oder ob wir aufgrund des Reduzierens einer Variablen stecken bleiben müssen. Garben ergeben sich aus der Betrachtung der Reduktionen des Lambda-Kalküls als Definition der Morphismen einer Kategorie, deren Terme die Objekte sind (dh die durch Reduktion induzierte Teilordnung), und der anschließenden Betrachtung der Funktoren aus dieser Kategorie in Mengen (dh Prädikate). Jean Gallier hat in den frühen 2000er Jahren einige schöne Artikel darüber geschrieben, aber ich bezweifle, dass sie lesbar sind, es sei denn, Sie haben bereits eine ganze Menge Lambda-Kalkül aufgenommen.

Es gibt viele Beispiele, die erste in den Sinn kommt , ist Alex Simpson ‚s Verwendung der Kategorie Theorie Eigenschaften von Programmiersprachen zu beweisen, siehe zB‚ Computational Adequacy für rekursive Typen in Modelle aus Intuitionistische Set Theory ‘, Annals of Pure and Applied Logic , 130: 207-275, 2004. Auch wenn der Titel Mengenlehre erwähnt, ist die Technik kategorietheoretisch. Weitere Beispiele finden Sie auf der Homepage von Alex.

Ich denke, Sie stellen zwei Fragen zur Anwendbarkeit, Typ A und Typ B, getrennt.

Wie Sie bemerken, gibt es viele inhaltliche Anwendungen der Kategorietheorie auf Themen des Typs B: Semantik von Programmiersprachen (Monaden, geschlossene kartesische Kategorien), Logik und Beweisbarkeit (Topoi, Varietäten der linearen Logik).

Es scheint jedoch nur wenige inhaltliche Anwendungen für Theorie A zu geben (Algorithmen oder Komplexität).

In elementaren Objekten gibt es einige Verwendungsmöglichkeiten, z. B. die Beschreibung von Kategorien von Automaten oder kombinatorischen Objekten (Graphen, Sequenzen, Permutationen usw.). Diese scheinen jedoch nicht für ein tieferes Verständnis der Sprachtheorie oder der Algorithmen verantwortlich zu sein.

Spekulativ könnte es sich um ein Missverhältnis zwischen den aktuellen Strategien der Kategorietheorie und den Fächern der Theorie A handeln:

• Die zentrale Strategie der Kategorietheorie ist die Auseinandersetzung mit Gleichheit (wenn Dinge gleich und verschieden sind und wie sie sich gegenseitig abbilden).

• Für die Komplexitätstheorie ist die primäre Strategie das Reduzieren und Setzen von Grenzen (man könnte annehmen, dass eine Reduzierung wie ein Pfeil ist, aber ich denke, dass nichts über diese oberflächliche Ähnlichkeit hinaus untersucht wurde).

• Für Algorithmen gibt es keine übergeordnete Strategie, außer ad-hoc kluges kombinatorisches Denken. Für bestimmte Gebiete würde ich erwarten, dass es fruchtbare Erforschung geben könnte (Algorithmen für Algebren?), Aber ich habe es noch nicht gesehen.

"TCS-A" -Anwendungen, die mir in den Sinn kommen, sind Joyals kombinatorische Spezies (Verallgemeinerungen von Potenzreihen zu Funktoren, um kombinatorische Objekte wie Bäume, Mengen, Multisätze usw. zu beschreiben) und die Formalisierung von kryptografischem "Game-Hopping" unter Verwendung relationaler, probabilistische Hoare-Logik (Easycrypt, Certicrypt, Andreas Lochbihlers Arbeit). Während Kategorien in letzteren nicht direkt vorkommen, waren sie maßgeblich an der Entwicklung der zugrunde liegenden Logik (z. B. Monaden) beteiligt.

PS: Da mein Name in der ersten Antwort erwähnt wurde: Die Verwendung von Gruppoidenfibrationen, um die Nichtteilbarkeit eines bestimmten Axioms in Martin-Löfs Typentheorie von Thomas Streicher und mir zu zeigen, kann auch als "solide" Verwendung der Kategorietheorie angesehen werden (wenn auch in Logik oder "TCS-B").

Das neuere Buch Seven Sketches in Compositionality listet verschiedene Anwendungen der Kategorietheorie in der Informatik und den Ingenieurwissenschaften auf. Hervorzuheben ist das Kapitel über Datenbanken, in dem die Autoren das Abfragen, Kombinieren, Migrieren und Entwickeln von Datenbanken anhand eines kategorialen Modells beschreiben. Die Autoren haben dies weiterentwickelt und die CQL ( Categorical Query Language ) und eine integrierte Entwicklungsumgebung (IDE) basierend auf ihrem kategorialen Datenbankmodell entwickelt.