CompilerForCAP – Building and compiling categorical towers in algorithmic category theory

Abstract

In this thesis we develop CompilerForCAP, a compiler for optimizing and verifying categorical towers in algorithmic category theory. To see the need for a compiler, we start with some setup: First, we show how algorithmic category theory can be interpreted as a high-level programming language, and introduce the software framework CAP: Categories, Algorithms, and Programming. Moreover, we introduce programming conventions which allow us to prove that categorical algorithms written in CAP are faithful to the mathematics done on paper. Next, we introduce the concept of categorical towers, which has been used before to make constructions in categories algorithmic. We will see that computations in categorical towers naturally come with a sizeable performance overhead. This shows the need for a compiler like CompilerForCAP. Afterwards, we present various applications of categorical towers exhibiting the advantages of the approach. The two main applications are the computation of lifts in categories of finitely presented modules over certain rings and algorithms for the closed monoidal structure of the category of ZX-diagrams, a category appearing in quantum computing. As an application, we use the category of ZX-diagrams to model a foundational functional programming language for quantum computers. Afterwards, we see in detail how CompilerForCAP can optimize the categorical towers in the presented applications and provide benchmarks showing the performance gains in concrete computations. As we will see, CompilerForCAP can make the difference between "finishes in seconds" and "will never finish". The central mechanism that makes these optimizations possible are reinterpretations of categorical towers, which allow to simplify the data structures of categorical towers. Finally, we show that CompilerForCAP can also be used as a proof assistant for verifying categorical implementations. In summary, CompilerForCAP can generate efficient and verified implementations, allowing us to make full use of the advantages of building categorical towers on a computer.

In dieser Arbeit entwickeln wir CompilerForCAP, einen Compiler zur Optimierung und Verifikation von kategoriellen Türmen in der algorithmischen Kategorientheorie. Um die Notwendigkeit eines Compilers zu erkennen, benötigen wir einige Vorbereitungen: Zuerst zeigen wir, wie algorithmische Kategorientheorie als höhere Programmiersprache aufgefasst werden kann, und stellen das Software-Framework CAP vor: Categories, Algorithms and Programming. Außerdem führen wir Konventionen ein, mit deren Hilfe wir beweisen können, dass kategorielle Algorithmen in CAP der Mathematik auf dem Papier treu sind. Als Nächstes führen wir das Konzept der kategoriellen Türme ein, das bereits früher verwendet wurde, um Konstruktionen in Kategorien zugänglich für Algorithmen zu machen. Wir werden sehen, dass Berechnungen in kategoriellen Türmen natürlicherweise mit einem beträchtlichen Performance-Overhead verbunden sind. Dies zeigt die Notwendigkeit eines Compilers wie CompilerForCAP. Anschließend stellen wir verschiedene Anwendungen von kategoriellen Türmen vor, die die Vorteile des Ansatzes zeigen. Die zwei Hauptanwendungen sind zum einen die Berechnung von Lifts in Kategorien endlich präsentierter Moduln über bestimmten Ringen, und zum anderen Algorithmen für die geschlossene monoidale Struktur der Kategorie der ZX-Diagramme, einer Kategorie aus dem Bereich des Quantencomputing. Als Anwendung verwenden wir die Kategorie der ZX-Diagramme, um eine elementare funktionale Programmiersprache für Quantencomputer zu modellieren. Anschließend sehen wir im Detail, wie CompilerForCAP die kategoriellen Türme in den vorgestellten Anwendungen optimieren kann, und führen Benchmarks durch, die die Performancezuwächse bei konkreten Berechnungen zeigen. Wie wir sehen werden, kann CompilerForCAP den Unterschied zwischen "terminiert in Sekunden" und "wird nie terminieren" ausmachen. Der zentrale Mechanismus, der diese Optimierungen ermöglicht, sind Reinterpretationen von kategoriellen Türmen, die es erlauben, die Datenstrukturen von kategoriellen Türmen zu vereinfachen. Zum Schluss zeigen wir, dass CompilerForCAP auch als Beweisassistent zur Verifikation kategorieller Implementierungen verwendet werden kann. Zusammenfassend sehen wir, dass CompilerForCAP effiziente und verifizierte Implementierungen erzeugen kann, was es uns ermöglicht, die Vorteile kategorieller Türme auf dem Computer voll auszuschöpfen.