Существует ли формальное определение CS для VCS и версий файлов?

Я не знаю, было ли это шуткой, но однажды я прочитал то, что упоминалось как формальное определение файла в системе управления версиями, такой как git, hg или svn. Это было что-то вроде математического объекта, такого как гомеоморфизм. Это была шутка или действительно теория информатики о системах управления версиями и математике VCS?

Вы думаете о твите Исаака Волкерсторфера (@agnoster) :

git становится легче, когда вы понимаете, что ветви - это гомеоморфные эндофункторы, отображающие подмногообразия гильбертова пространства.

К сожалению, это шутка. Как написал автор на Quora :

Он был задуман как насмешливый. Я действительно люблю мерзавца, и я думаю, что его сложность сильно раздута. В то же время, я сочувствую тому факту, что советы от мерзавцев-гуру новичкам могут в конечном итоге звучать как непостижимая тарабарщина.

Это не имеет более глубокого смысла. Попытки проанализировать его таким способом должны быть тщетными, но из-за ошибки в действительности, вы можете фактически сделать любое достаточно волнообразное заявление подходящим, если вы попытаетесь достаточно усердно.

Это обсуждалось на стековом обмене программистов и на математическом стеке .

Шутка в сторону, была работа по формализации контроля версий. Одной из попыток, которые объединяют теорию и практику, является работа Дэвида Раунди по теории патчей над Darcs . Основной целью теории является моделирование слияния и, в частности, разрешение конфликтов. В вики Darcs есть введение в теорию и несколько указателей, а также библиография (не поддерживается, так что устарела, если вы хотите получить последнее представление по этому вопросу, но в ней есть обзорная статья 2009 года Петра Баудиша ) и список выступлений ( который включает в себя более свежий материал). Там также викибук . Одним из основополагающих документов является принципиальный подход к контролю версийАндрес Лох, Вутер Свирстра и Даан Лейжен3 .

Теория патчей действительно приводит к категориальной модели, которая была недавно исследована в «Категориальной теории патчей » Самюэля Мимрама и Чинзии Ди Джусто и « Гомотопическая теория патчей » Карло Анжули, Эда Морхауса, Дэниела Р. Ликата и Роберта Харпера . В работах Мимрама и Ди Джусто модель имеет файлы как объекты и патчи как морфизмы. Я думаю, что это делает слияние ветки функтором - эндофунктором, если вы работаете в одном репозитории. «Гомеоморфный эндофунктор» для меня не имеет смысла. С учетом теории гомотопий подмногообразия гильбертова пространства не могут быть так далеко ...

Конечно, существует математический формализм для систем контроля версий. Существует математический формализм практически для каждого алгоритма в CS. Есть много формализмов для многих. Не существует связи 1-1 между формализмами и системами, которые они моделируют . Модели могут варьироваться от простых до сложных. Вот пример для VCS / SCM также от Swierstra, который еще не цитировался.

• Семантика контроля версий

SCM также имеет много общего с понятием «параллельные вселенные / временные шкалы» и путешествия во времени, которые иногда используются в научной фантастике. Он фиксирует состояние развивающейся системы в разное время или «снимки». Есть «ветви» и «слияния». Смотрите также сроки .