Dyskusja matematyczna: Twierdzenie o systemie kontroli wersji git?

Chciałbym wygłosić wykład matematyczny na temat systemu kontroli wersji git . Obecnie jest szeroko stosowany w matematyce, a także w branży informatycznej. Na przykład społeczność HoTT (Homotopy Type Theory) korzysta z niego i jest to system do wspólnej edycji plików tekstowych, niezależnie od tego, czy są to kody źródłowe, czy znaczniki lateksowe.

Wiem, że git używa pojęcia ukierunkowanego wykresu acyklicznego, który jest początkiem. Jednak dobra rozmowa matematyczna wymienia dowody i twierdzenia.

Jakie twierdzenie o git może mieć znaczenie dla jego użycia?

Repozytorium git można traktować jako częściowo uporządkowany zestaw rewizji (gdzie jedna rewizja jest wcześniejsza niż druga w kolejności, jeśli jest bezpośrednim lub pośrednim następcą poprzedniej). Częściowe zamówienia otrzymywane z repozytoriów git mają zwykle małą szerokość (rozmiar największego zestawu wzajemnie niezależnych rewizji), ponieważ szerokość jest bezpośrednio związana z liczbą aktywnych programistów i liczbą różnych rozwidleń, które może pracować każdy indywidualny programista na.

Opierając się na tym tle, zasugerowałbym twierdzenie Dilwortha , które stwierdza, że ​​szerokość dowolnego zamówienia częściowego jest równa minimalnej liczbie łańcuchów (całkowicie uporządkowanych podzbiorów) potrzebnej do pokrycia wszystkich wersji. Aby uczynić go tematycznym dla tej płyty, możesz również wspomnieć o algorytmach opartych na dopasowywaniu grafów do obliczania szerokości i znajdowania pokrycia przez minimalną liczbę łańcuchów w czasie wielomianowym.

Jednym ze sposobów, które mogą być istotne dla faktycznego użycia w Git, jest system wizualizacji historii wersji systemu: większość systemów wizualizacji Git, które widziałem rysują czas na osi pionowej, oraz niezależne wersje repozytorium w poziomie, więc to dałby ci sposób zorganizowania wizualizacji w małą liczbę niezależnych ścieżek pionowych.

Ewentualnie, jeśli chcesz czegoś bardziej ambitnego i zaawansowanego, wypróbuj strukturę danych drzewa winy Demaine i wsp. , Która jest bezpośrednio motywowana rozwiązywaniem konfliktów w podobnych do git systemach kontroli wersji.

Co ciekawe, rodzi się matematyzacja systemów kontroli wersji, chociaż w tym momencie ma ona tylko częściowe zastosowanie do Git. Nazywa się to teorią łatek [1, 2, 3, 4, 5] i powstało w kontekście systemu kontroli wersji DARCS. Można to postrzegać jako abstrakcyjną teorię rozgałęziania i łączenia . Ostatnio na temat teorii płatków zastosowano leczenie HoTT [6] i kategoryczne [7].

Teoria łatek jest w toku i nie obejmuje wszystkich aspektów kontroli wersji, ale zawiera wiele twierdzeń, na które można spojrzeć. Jest to wyraźny przykład teorii, która ma zastosowanie w „prawdziwym świecie” - nic dziwnego, ponieważ teoria łatek jest abstrakcją / uproszczeniem czegoś bardzo konkretnego. Jednocześnie łączy się z najnowocześniejszymi matematykami, takimi jak HoTT.

1. J. Dagit, Zmiany poprawne dla typu - Bezpieczne podejście do implementacji kontroli wersji .
2. G. Sittampalam, Niektóre właściwości teorii łatek .
3. I. Lynagh, Teoria obozów.
4. D. Roundy, Wdrażanie formalizmu łat Darcs ... i weryfikowanie go.
5. J. Jacobson, Formalizacja teorii łatek Darcsa przy użyciu odwrotnych półgrup .
6. C. Angiuli, E. Morehouse, DR Licata, R. Harper, Homotopical Theory Patch .
7. S. Mimram, C. Di Giusto, Kategoryczna teoria łat .

Inną alternatywą jest spojrzenie na trwałe (lub czysto funkcjonalne) struktury danych. Wewnętrzna struktura danych Gita może być postrzegana jako spójne drzewo :

trwała struktura danych to struktura danych, która zawsze zachowuje swoją poprzednią wersję po modyfikacji. Takie struktury danych są niezmienne, ponieważ ich operacje nie (widocznie) aktualizują struktury w miejscu, ale zawsze dają nową zaktualizowaną strukturę.

Struktura danych jest częściowo trwała, jeśli można uzyskać dostęp do wszystkich wersji, ale modyfikować można tylko najnowszą wersję. Struktura danych jest w pełni trwała, jeśli można uzyskać dostęp do każdej wersji i ją zmodyfikować. Jeśli istnieje również operacja łączenia lub scalania, która może utworzyć nową wersję z dwóch poprzednich wersji, struktura danych jest nazywana konfluentnie trwałą.

To pytanie jest również istotne.

Tak, możesz matematycznie zdefiniować działanie Git. Możesz zdefiniować prymitywne struktury Git i operacje Git na nich, a następnie mieć twierdzenia, które dowodzą, że użycie tych operacji w określony sposób osiąga określone cele wyższego poziomu, lub próbować scharakteryzować lub kwantyfikować sytuacje, w których tak nie jest. (Np. Zależność Gita od skrótów pozostawia niewielki margines błędu).

Innym pomysłem jest zrobienie tego samego dla Subversion, a następnie wygenerowanie twierdzeń porównujących oba. Na przykład często twierdzi się, że Git lepiej radzi sobie z fuzjami; możesz mieć twierdzenia, które to potwierdzają, jakościowo lub ilościowo.

Przydatność krytycznie zależy od robienia właściwych abstrakcji. Matematyczny opis działania kodu źródłowego Git ze wszystkimi szczegółami jest bezcelowy: sam kod źródłowy robi to o wiele bardziej skutecznie i zwięźle.