Mathe-Diskussion: Theorem über das Git-Revisionskontrollsystem?

Ich möchte einen mathematischen Vortrag über das Git Revisionskontrollsystem halten. Es ist heute weit verbreitet in der Mathematik sowie in der Informatikindustrie. Zum Beispiel wird es von der HoTT-Community (Homotopy Type Theory) verwendet und ist das Go-to-System für die gemeinsame Bearbeitung von Textdateien, unabhängig davon, ob es sich um Quellcode oder Latex-Markup handelt.

Ich weiß, dass Git den Begriff eines gerichteten azyklischen Graphen verwendet, der ein Anfang ist. In einem guten Mathematikgespräch werden jedoch Beweise und Theoreme erwähnt.

Welchen Satz könnte ich über Git beweisen, der für seine Verwendung tatsächlich relevant ist?

Ein Git-Repository kann als ein teilweise geordneter Satz von Revisionen betrachtet werden (wobei eine Revision in der Reihenfolge vor der anderen liegt, wenn es sich um einen direkten oder indirekten Nachfolger der früheren handelt). Die Teilbestellungen, die Sie von Git-Repositories erhalten, haben in der Regel eine geringe Breite (die Größe des größten Satzes von voneinander unabhängigen Revisionen), da die Breite direkt mit der Anzahl der aktiven Entwickler und der Anzahl der verschiedenen Gabeln zusammenhängt, die ein einzelner Entwickler möglicherweise bearbeitet auf.

Vor diesem Hintergrund würde ich den Satz von Dilworth vorschlagen , der besagt, dass die Breite einer Teilordnung gleich der Mindestanzahl von Ketten (vollständig geordnete Teilmengen) ist, die erforderlich sind, um alle Versionen abzudecken. Und um es für dieses Board themenbezogen zu machen, können Sie auch die Algorithmen erwähnen, die auf dem Graph Matching basieren, um die Breite zu berechnen und eine Abdeckung durch eine minimale Anzahl von Ketten in Polynomzeit zu finden.

Eine Möglichkeit, die für die tatsächliche Verwendung in Git relevant sein könnte, besteht in einem System zur Visualisierung des Versionsverlaufs eines Systems: Die meisten Git-Visualisierungssysteme, die ich bisher gesehen habe, zeichnen die Zeit auf der vertikalen Achse und unabhängige Versionen des Repositorys horizontal Damit können Sie die Visualisierung in eine kleine Anzahl unabhängiger vertikaler Spuren unterteilen.

Wenn Sie etwas ehrgeizigeres und fortschrittlicheres wollen, probieren Sie alternativ die Datenstruktur von Demaine et al. Aus , die direkt durch die Konfliktlösung in git-ähnlichen Versionskontrollsystemen motiviert ist.

Interessanterweise gibt es eine beginnende Mathematisierung von Versionskontrollsystemen, obwohl diese derzeit nur teilweise auf Git anwendbar ist. Es heißt Patch-Theorie [1, 2, 3, 4, 5] und ist im Kontext des DARCS-Versionskontrollsystems entstanden. Es kann als abstrakte Theorie der Verzweigung und Verschmelzung angesehen werden . Vor kurzem wurde die Patch-Theorie mit HoTT [6] und kategorischen [7] Behandlungen behandelt.

Die Patch-Theorie ist noch in Arbeit und deckt nicht alle Aspekte der Versionskontrolle ab, enthält jedoch eine Vielzahl von Theoremen, die Sie sich ansehen können. Es ist ein klares Beispiel für eine Theorie, die auf die "reale Welt" anwendbar ist - nicht überraschend, denn die Patch-Theorie ist eine Abstraktion / Vereinfachung von etwas sehr Konkretem. Gleichzeitig verbindet es sich mit hochmodernen Mathematiken wie HoTT.

1. J. Dagit, typkorrekte Änderungen - Ein sicherer Ansatz für die Implementierung der Versionskontrolle .
2. G. Sittampalam, Einige Eigenschaften der Darcs-Patch-Theorie .
3. I. Lynagh, Camp-Path-Theorie.
4. D. Roundy, Implementierung des Darcs-Patch-Formalismus ... und Überprüfung.
5. J. Jacobson, Eine Formalisierung der Darcs-Patch-Theorie unter Verwendung inverser Halbgruppen .
6. C. Angiuli, E. Morehouse, Dr. Licata, R. Harper, Homotopical Patch Theory .
7. S. Mimram, C. Di Giusto, Eine kategorische Theorie der Flecken .

Eine andere Alternative besteht darin, persistente (oder rein funktionale) Datenstrukturen zu betrachten. Die interne Datenstruktur von Git kann als konsequent persistenter Baum angesehen werden :

Eine persistente Datenstruktur ist eine Datenstruktur, die immer die vorherige Version von sich selbst beibehält, wenn sie geändert wird. Solche Datenstrukturen sind effektiv unveränderlich, da ihre Operationen die Struktur nicht (sichtbar) an Ort und Stelle aktualisieren, sondern stattdessen immer eine neue aktualisierte Struktur ergeben.

Eine Datenstruktur ist teilweise persistent, wenn auf alle Versionen zugegriffen werden kann, aber nur die neueste Version geändert werden kann. Die Datenstruktur ist vollständig persistent, wenn auf jede Version zugegriffen und sie geändert werden kann. Wenn es auch eine Verschmelzungs- oder Zusammenführungsoperation gibt, die eine neue Version aus zwei früheren Versionen erstellen kann, wird die Datenstruktur als konfluent persistent bezeichnet.

Diese Frage ist auch relevant.

Ja, Sie können mathematisch definieren, wie Git funktioniert. Sie könnten primitive Git-Strukturen und Git-Operationen definieren und dann Theoreme haben, die beweisen, dass die Verwendung dieser Operationen auf bestimmte Weise bestimmte übergeordnete Ziele erreicht, oder Sie könnten versuchen, Situationen zu charakterisieren oder zu quantifizieren, in denen dies nicht der Fall ist. (ZB lässt Gits Vertrauen in Hashes einen winzigen Spielraum für Fehler.)

Eine andere Idee ist, dasselbe für Subversion zu tun und dann Sätze zu produzieren, die beide vergleichen. Beispielsweise wird oft behauptet, dass Git besser mit Zusammenführungen umgehen kann. Sie können Theoreme haben, die dies qualitativ oder quantitativ belegen.

Der Nutzen würde entscheidend davon abhängen, die richtigen Abstraktionen zu machen. Das mathematische Beschreiben der Funktionsweise des Git-Quellcodes in allen Einzelheiten ist sinnlos: Der Quellcode selbst erledigt dies viel effektiver und prägnanter.