Pijul
When working with distant collaborators on the same documents, one often uses a version control system, which is a program tracking the history of files and helping importing modifications brought by others as patches. The implementation of such a system requires to handle lots of situations depending on the operations performed by users on files, and it is thus difficult to ensure that all the corner cases have been correctly addressed. Here, instead of verifying the implementation of such a system, we adopt a complementary approach: we introduce a theoretical model, which is defined abstractly by the universal property that it should satisfy, and work out a concrete description of it. We begin by defining a category of files and patches, where the operation of merging the effect of two coinitial patches is defined by pushout. Since two patches can be incompatible, such a pushout does not necessarily exist in the category, which raises the question of which is the correct category to represent and manipulate files in conflicting state. We provide an answer by investigating the free completion of the category of files under finite colimits, and give an explicit description of this category: its objects are finite sets labeled by lines equipped with a transitive relation and morphisms are partial functions respecting labeling and relations.
patch の圈$ \cal Pを操作する VMS (version management system) file 中の全ての行が一列に竝んだ (conflict を含まない) file と patch の圈$ \cal Lを構成する file$ A,B,…を對象とし、patch$ f,g,…を射とする
$ L=\lbrace a,b,…\rbraceを行の集合とする
file は行$ \in Lの有限列。自然數の部分集合である行番號から行への函數$ A:\lbrack n_{\in\N}\rbrack\to Lと見做せる 空 file$ Iも 0 行目を持つ$ I:\lbrack 0\rbrack\to L
file$ A:\lbrack m\rbrack\to Lからfile$ B:\lbrack n\rbrack\to Lへの patch$ fは、自然數の單調な部分寫像$ f:\lbrack m\rbrack\to\lbrack n\rbrackに成る。file$ Aの全ての行番號$ \forall i_{\in\lbrack m\rbrack}に就いて、若し$ \exist f(i)が定義されてゐれば$ B\circ f(i)=A(i)が成り立つ file$ A:\lbrack m\rbrack\to L,$ B:\lbrack n\rbrack\to L,$ C:\lbrack j\rbrack\to Lと patch$ f:\lbrack m\rbrack\to\lbrack n\rbrack,$ g:\lbrack n\rbrack\to\lbrack j\rbrackに就いて、patch の合成$ g\circ f:\lbrack m\rbrack\to\lbrack j\rbrackは單純な函數の合成
單位は空 file$ I:\lbrack 0\rbrack\to L
file$ A:\lbrack m\rbrack\to L,$ B:\lbrack n\rbrack\to Lに就いて$ (A\otimes B)(i):\lbrack m+n\rbrack\to Lは、
$ i<mならば$ A(i)
$ i\ge mならば$ B(i-m)
file$ Aの末尾に file$ Bを繫げた file
file$ A:\lbrack m\rbrack\to L,$ B:\lbrack n\rbrack\to L,$ C:\lbrack j\rbrack\to L,$ D:\lbrack k\rbrack\to Lに對して、patch$ f:\lbrack m\rbrack\to\lbrack j\rbrack,$ g:\lbrack n\rbrack\to\lbrack k\rbrackの tensor 積$ (f\otimes g)(i):\lbrack m+n\rbrack\to\lbrack j+k\rbrackは、 $ i<mならば$ f(i)
$ i\ge mならば$ g(i-m)
結合律$ (A\otimes B)\otimes C=A\otimes(B\otimes C) 行$ \in Lを對象に入れる
全ての行$ \forall a_{\in L}に就いて
射「插入 (insertion)」を$ \eta_a:I\to aで定義する
射「削除 (deletion)」を$ \epsilon_a:a\to Iで定義する
律$ \epsilon_a\circ\eta_a={\rm id}_Iが成り立つ
conflict を含まない merge は圈$ \cal Lでの自然な押し出しに成る。conflict を含む merge の押し出しは圈$ \cal Lに存在しない 押し出しとは、圖式$ B\xleftarrow{f}A\xrightarrow{g}Cの餘極限$ B+_AC 可換圖式$ P\xleftarrow{g/f}B\xleftarrow{f}A\xrightarrow{g}C\xrightarrow{f/g}Pを成立させる對象$ Pの圈の終對象 patch$ g/fは、patch$ gの patch$ fに依る剩餘
conflict を含まない merge とは、互ひに離れた行を編緝した patch 同士の merge
file 中の一部の行の竝びが決まってゐない (conflict を含む) file と patch の圈$ \cal Pを、圈$ \cal Lの自由で有限な保守的餘完備化に依り構成する 埋め込み函手$ y:{\cal L}\to{\cal P}は有限餘極限を保存する 有限餘完備化した任意の圈$ \cal Cに就いて、 有限餘極限を保存する同型を除いて一意な函手$ \exist F:{\cal L}\to{\cal C}と、 有限餘極限を保存する一意な函手$ \exist!F^〜:{\cal P}\to{\cal C}が存在し、 conflict を含んだ file を對象に含む
underlying graph (臺 graph)
patch を管理するのは Darcs を參考にしたから