<p>Interestingly, there is a nascent mathematisation of version control systems, although at this point it's only partially applicable to Git. It's called <strong>patch theory</strong> [1, 2, 3, 4, 5] and  arose in the context of the DARCS version control system. It can be seen as an abstract theory of <a href="https://en.wikipedia.org/wiki/Branching_(revision_control)">branching</a> and <a href="https://en.wikipedia.org/wiki/Merge_(revision_control)">merging</a>. Recently patch theory has been given HoTT [ 6 ] and categorical [ 7 ] treatments. </p>

<p>Patch theory is work in progress, and doesn't cover all aspects of version control, but contains a lot of theorems that you could look at. It is a clear example of theory that's applicable to the 'real world' -- not surprising, for patch theory is an abstraction / simplification of something very concrete. At the same time it connects with cutting-edge maths like HoTT.</p>

<hr>

<ol>
<li>J. Dagit, <a href="https://ir.library.oregonstate.edu/xmlui/bitstream/handle/1957/11180/thesis.pdf">Type-Correct Changes - A Safe Approach to Version Control Implementation</a>.</li>
<li>G. Sittampalam, <a href="https://urchin.earth.li/darcs/ganesh/darcs-patch-theory/theory/formal.pdf">Some properties of darcs patch theory</a>.</li>
<li>I. Lynagh, Camp Path Theory.</li>
<li>D. Roundy, Implementing the darcs patch formalism ... and verifying it.</li>
<li>J. Jacobson, <a href="ftp://ftp.math.ucla.edu/pub/camreport/cam09-83.pdf">A Formalization Of Darcs Patch Theory Using Inverse Semigroups</a>.</li>
<li>C. Angiuli, E. Morehouse, D. R. Licata, R. Harper, <a href="https://www.cs.cmu.edu/~rwh/papers/htpt/paper.pdf">Homotopical Patch Theory</a>.</li>
<li>S. Mimram, C. Di Giusto, <a href="http://arxiv.org/abs/1311.3903">A Categorical Theory of Patches</a>.</li>
</ol>

CC BY-SA 3.0
2015-08-26T08:04:47.840Z
2015-08-26T14:35:10.533Z
2015-08-26T14:35:10.533Z
Martin Berger
<p>Another alternative is to look at persistent (or purely functional) data structures. Git's internal data structure can be seen as a <a href="https://en.wikipedia.org/w/index.php?title=Persistent_data_structure&amp;oldid=668365743#Trees" rel="nofollow noreferrer">confluently persistent tree</a>:</p>

<blockquote>
  <p>a persistent data structure is a data structure that always preserves the previous version of itself when it is modified. Such data structures are effectively immutable, as their operations do not (visibly) update the structure in-place, but instead always yield a new updated structure.</p>
  
  <p>A data structure is partially persistent if all versions can be accessed but only the newest version can be modified. The data structure is fully persistent if every version can be both accessed and modified. If there is also a meld or merge operation that can create a new version from two previous versions, the data structure is called confluently persistent.</p>
</blockquote>

<p>This <a href="https://cstheory.stackexchange.com/questions/1539/whats-new-in-purely-functional-data-structures-since-okasaki">question</a> is relevant too.</p>

CC BY-SA 3.0
2015-08-27T18:58:01.420Z
2015-08-27T19:03:09.500Z
2017-04-13T12:32:28.743Z
ivotron
<p>Yes, you can mathematically define how Git works. You could define primitive Git structures and Git operations on them and then have theorems that prove that using these operations in particular ways achieves particular higher-level goals, or attempt to characterize or quantify situations in which this is not the case.
(E.g. Git's reliance on hashes leaves a tiny margin for error.)</p>

<p>Another idea is to do the same thing for Subversion, then produce theorems that compare the two. For instance, it is often claimed that Git is better at dealing with merges; you can have theorems that prove this, qualitatively or quantitively.</p>

<p>Usefulness would critically depend on making the right abstractions. Mathematically describing the workings of the Git source code in all detail is pointless: the source code itself does that much more effectively and concisely.</p>

CC BY-SA 3.0
2015-08-25T21:52:42.547Z
2015-10-01T20:40:00.873Z
2015-10-01T20:40:00.873Z
reinierpost
<p>A git repository can be thought of as a partially ordered set of revisions (where one revision is earlier than another in the order if it is a direct or indirect successor of the earlier one). The partial orders that you get from git repositories tend to have low width (the size of the largest set of mutually independent revisions) because the width is directly related to the number of active developers and the number of different forks any individual developer might be working on.</p>

<p>Based on this background, I would suggest <a href="https://en.wikipedia.org/wiki/Dilworth%27s_theorem">Dilworth's theorem</a>, which states that the width of any partial order equals the minimum number of chains (totally ordered subsets) needed to cover all of the versions. And to make it on-topic for this board, you could also mention the graph matching based algorithms for computing the width and finding a cover by a minimum number of chains in polynomial time.</p>

<p>One way this could be relevant for actual use in Git is in a system for visualizing the version history of a system: most Git visualization systems that I've seen draw time on the vertical axis, and independent versions of the repository horizontally, so this would give you a way to organize the visualization into a small number of independent vertical tracks.</p>

<p>Alternatively, if you want something more ambitious and advanced, try Demaine et al.'s <a href="http://ezyang.com/papers/demaine13-blametrees.pdf">blame tree data structure</a>, which is directly motivated by conflict resolution in git-like version control systems.</p>

CC BY-SA 3.0
2015-08-25T22:13:43.053Z
2015-08-25T22:20:40.607Z
2015-08-25T22:20:40.607Z
David Eppstein
<p>I would like to give a mathematics talk on the <a href="https://no.wikipedia.org/wiki/Git">git</a> revision control system. It is now widely used in mathematics as well as in the computer science industry.  For example, the HoTT (Homotopy Type Theory) community uses it, and it is the go to system for collaborative editing of text files, whether they be source code or latex markup.</p>

<p>I know git uses the notion of a directed acyclic graph, which is a start.  However, a good mathematics talk mentions proofs and theorems.</p>

<p>What theorem might I prove about git that is actually relevant for its use?</p>

CC BY-SA 3.0
2015-08-25T20:22:26.667Z
Can you expand on your motivation? Is the goal to suggest reasons why mathematicians should use git, and throw in some theorems for fun / to grab their attention?
usul
CC BY-SA 3.0
2015-08-25T20:30:47.727Z
Primarily, my motivation is to demonstrate that mathematical concepts are applicable by using git as an example.  Secondarily, git is quite useful in the math world, as much as in the CS world, so my audience might as well learn what it does and why one might use it.
Rex Butler
CC BY-SA 3.0
2015-08-26T11:37:23.383Z
@RexButler - git is useful in math the same way a pencil is. It's a general tool that some mathematicians happen to use.
Davor
CC BY-SA 3.0
2015-08-26T14:18:02.707Z
This question reminds me of ["A Guide to GIT using spatial analogies"](https://web.archive.org/web/20150523021626/http://tartley.com/?p=1267) (link to Wayback Machine because the site appears to be down right now).
duplode
CC BY-SA 3.0
2015-08-28T15:39:06.643Z
["git gets easier once you get the basic idea that branches are homeomorphic endofunctors mapping submanifolds"](http://programmers.stackexchange.com/questions/256450/are-git-branches-in-fact-homeomorphic-endofunctors-mapping-submanifolds-of-a) TL;DR That is not actually the case.
Mitch
CC BY-SA 3.0
2015-08-29T04:48:48.913Z
similar question recently showed up on [cs.se]: [formal CS defn of VCS and file versions](http://cs.stackexchange.com/questions/12652/is-there-a-formal-cs-definition-of-vcs-and-file-versions)
vzn
<co.combinatorics><application-of-theory>
Math talk: Theorem about git revision control system?
Rex Butler
# Math talk: Theorem about git revision control system?

(Asked by: username_0 on 2015-08-25)

I would like to give a mathematics talk on the [git](https://no.wikipedia.org/wiki/Git) revision control system. It is now widely used in mathematics as well as in the computer science industry. For example, the HoTT (Homotopy Type Theory) community uses it, and it is the go to system for collaborative editing of text files, whether they be source code or latex markup.

I know git uses the notion of a directed acyclic graph, which is a start. However, a good mathematics talk mentions proofs and theorems.

What theorem might I prove about git that is actually relevant for its use?

**Tags:** co.combinatorics, application-of-theory
> **Comments:**
> **username_1**: Can you expand on your motivation? Is the goal to suggest reasons why mathematicians should use git, and throw in some theorems for fun / to grab their attention?  
> **username_0**: Primarily, my motivation is to demonstrate that mathematical concepts are applicable by using git as an example.  Secondarily, git is quite useful in the math world, as much as in the CS world, so my audience might as well learn what it does and why one might use it.  
> **username_2**: @RexButler - git is useful in math the same way a pencil is. It's a general tool that some mathematicians happen to use.  
> **username_3**: This question reminds me of ["A Guide to GIT using spatial analogies"](https://web.archive.org/web/20150523021626/http://tartley.com/?p=1267) (link to Wayback Machine because the site appears to be down right now).  
> **username_4**: ["git gets easier once you get the basic idea that branches are homeomorphic endofunctors mapping submanifolds"](http://programmers.stackexchange.com/questions/256450/are-git-branches-in-fact-homeomorphic-endofunctors-mapping-submanifolds-of-a) TL;DR That is not actually the case.  
> **username_5**: similar question recently showed up on [cs.se]: [formal CS defn of VCS and file versions](http://cs.stackexchange.com/questions/12652/is-there-a-formal-cs-definition-of-vcs-and-file-versions)  

---

## 4 answers

### Answer by username_9 on 2015-08-25. Score: 16 | Accepted answer

A git repository can be thought of as a partially ordered set of revisions (where one revision is earlier than another in the order if it is a direct or indirect successor of the earlier one). The partial orders that you get from git repositories tend to have low width (the size of the largest set of mutually independent revisions) because the width is directly related to the number of active developers and the number of different forks any individual developer might be working on.

Based on this background, I would suggest [Dilworth's theorem](https://en.wikipedia.org/wiki/Dilworth%27s_theorem), which states that the width of any partial order equals the minimum number of chains (totally ordered subsets) needed to cover all of the versions. And to make it on-topic for this board, you could also mention the graph matching based algorithms for computing the width and finding a cover by a minimum number of chains in polynomial time.

One way this could be relevant for actual use in Git is in a system for visualizing the version history of a system: most Git visualization systems that I've seen draw time on the vertical axis, and independent versions of the repository horizontally, so this would give you a way to organize the visualization into a small number of independent vertical tracks.

Alternatively, if you want something more ambitious and advanced, try Demaine et al.'s [blame tree data structure](http://ezyang.com/papers/demaine13-blametrees.pdf), which is directly motivated by conflict resolution in git-like version control systems.


---

### Answer by username_6 on 2015-08-26. Score: 17

Interestingly, there is a nascent mathematisation of version control systems, although at this point it's only partially applicable to Git. It's called **patch theory** [1, 2, 3, 4, 5] and arose in the context of the DARCS version control system. It can be seen as an abstract theory of [branching](https://en.wikipedia.org/wiki/Branching_(revision_control)) and [merging](https://en.wikipedia.org/wiki/Merge_(revision_control)). Recently patch theory has been given HoTT [ 6 ] and categorical [ 7 ] treatments.

Patch theory is work in progress, and doesn't cover all aspects of version control, but contains a lot of theorems that you could look at. It is a clear example of theory that's applicable to the 'real world' -- not surprising, for patch theory is an abstraction / simplification of something very concrete. At the same time it connects with cutting-edge maths like HoTT.

---

1. J. Dagit, [Type-Correct Changes - A Safe Approach to Version Control Implementation](https://ir.library.oregonstate.edu/xmlui/bitstream/handle/1957/11180/thesis.pdf).
2. G. Sittampalam, [Some properties of darcs patch theory](https://urchin.earth.li/darcs/ganesh/darcs-patch-theory/theory/formal.pdf).
3. I. Lynagh, Camp Path Theory.
4. D. Roundy, Implementing the darcs patch formalism ... and verifying it.
5. J. Jacobson, [A Formalization Of Darcs Patch Theory Using Inverse Semigroups](ftp://ftp.math.ucla.edu/pub/camreport/cam09-83.pdf).
6. C. Angiuli, E. Morehouse, D. R. Licata, R. Harper, [Homotopical Patch Theory](https://www.cs.cmu.edu/~rwh/papers/htpt/paper.pdf).
7. S. Mimram, C. Di Giusto, [A Categorical Theory of Patches](http://arxiv.org/abs/1311.3903).


---

### Answer by username_7 on 2015-08-27. Score: 4

Another alternative is to look at persistent (or purely functional) data structures. Git's internal data structure can be seen as a [confluently persistent tree](https://en.wikipedia.org/w/index.php?title=Persistent_data_structure&oldid=668365743#Trees):

> a persistent data structure is a data structure that always preserves the previous version of itself when it is modified. Such data structures are effectively immutable, as their operations do not (visibly) update the structure in-place, but instead always yield a new updated structure.
>
> A data structure is partially persistent if all versions can be accessed but only the newest version can be modified. The data structure is fully persistent if every version can be both accessed and modified. If there is also a meld or merge operation that can create a new version from two previous versions, the data structure is called confluently persistent.

This [question](https://cstheory.stackexchange.com/questions/1539/whats-new-in-purely-functional-data-structures-since-okasaki) is relevant too.


---

### Answer by username_8 on 2015-08-25. Score: 1

Yes, you can mathematically define how Git works. You could define primitive Git structures and Git operations on them and then have theorems that prove that using these operations in particular ways achieves particular higher-level goals, or attempt to characterize or quantify situations in which this is not the case.
(E.g. Git's reliance on hashes leaves a tiny margin for error.)

Another idea is to do the same thing for Subversion, then produce theorems that compare the two. For instance, it is often claimed that Git is better at dealing with merges; you can have theorems that prove this, qualitatively or quantitively.

Usefulness would critically depend on making the right abstractions. Mathematically describing the workings of the Git source code in all detail is pointless: the source code itself does that much more effectively and concisely.


---

