Czy istnieje formalna definicja CS VCS i wersji plików?

Nie wiem, czy to był żart, ale kiedy przeczytałem coś, co nazywano formalną definicją pliku w systemie kontroli wersji, takim jak git, hg lub svn. To było coś w rodzaju przedmiotu matematycznego, takiego jak homeomorfizm. Czy to był żart, czy naprawdę istnieje teoria informatyki na temat systemów wersjonowania i matematyki VCS?

Myślisz o tweecie autorstwa Izaaka Wolkerstorfera (@agnoster) :

git staje się łatwiejszy, gdy zrozumiesz, że gałęzie są homeomorficznymi endofunkorami mapującymi podfoldery przestrzeni Hilberta.

Niestety to żart. Jak pisał autor na Quora :

Miało być mocno przymocowane do języka. Naprawdę uwielbiam Gita i myślę, że jego złożoność jest mocno przesadzona. Jednocześnie popieram fakt, że porady od git guru dla nowicjuszy mogą brzmieć jak nieprzenikniony bełkot.

Nie ma mieć głębszego znaczenia. Próby analizy tego w ten sposób powinny być daremne, ale z powodu błędu w rzeczywistości możesz właściwie dopasować dowolne oświadczenie, jeśli spróbujesz wystarczająco mocno.

Zostało to omówione na temat wymiany stosów programistów i wymiany stosów matematycznych .

Żart na bok, formalizowano kontrolę wersji. Jednym wysiłkiem, który sprzymierzyła teoria i praktyka, jest praca nad teorią łatek autorstwa Davida Roundy'ego na temat Darcsa . Głównym celem teorii jest modelowanie łączenia, a w szczególności rozwiązywania konfliktów. Darcs wiki ma wprowadzenie do teorii i kilka wskazówek, a także bibliografię (brakuje opiekuna tak nieaktualne, jeśli chcesz niedawno pogląd na ten temat, ale ma w wykazie A, papier 2009 Badanie przeprowadzone przez Petr BAUDIS ) oraz wykaz rozmów ( który zawiera nowsze materiały). Istnieje również wikibook . Jednym z najważniejszych artykułów jest zasadnicze podejście do kontroli wersjiautorzy: Andres Löh, Wouter Swierstra i Daan Leijen3 .

Teoria łatek prowadzi do modelu kategorycznego, który został ostatnio zbadany w A Categorical Theory of Patches autorstwa Samuela Mimrama i Cinzii Di Giusto oraz Homotopical Patch Theory autorstwa Carlo Angiuli, Eda Morehouse'a, Daniela R. Licaty i Roberta Harpera . W pracy Mimram i Di Giusto model ma pliki jako obiekty, a łatki jako morfizmy. Myślę, że to sprawia, że ​​scalanie gałęzi jest funktorem - endofunkorem, jeśli pracujesz w jednym repozytorium. „Homeomorficzny endofunkor” nie ma dla mnie sensu. W przypadku teorii homotopii podfoldery przestrzeni Hilberta mogą nie być tak daleko ...

Oczywiście istnieje formalizm matematyczny dla systemów kontroli wersji. Istnieje formalizm matematyczny dla praktycznie każdego algorytmu w CS. Dla wielu istnieje wiele formalności. Nie ma związku 1-1 między formalizmami a modelowanymi przez nie systemami . Modele mogą mieć zakres od prostych do złożonych. Oto przykład VCS / SCM również autorstwa Świerstry, jeszcze nie cytowany.

• Semantyka kontroli wersji

SCM ma również wiele podobieństw do koncepcji „równoległych wszechświatów / linii czasu” i podróży w czasie, czasami wykorzystywanych w science fiction. Przechwytuje stan ewoluującego systemu w różnych momentach lub „migawkach”. Istnieją „oddziały” i „scalenia”. Zobacz także osie czasu .