斑块范畴论：文件版本管理理论的抽象模型

可在www.sciencedirect.com在线获取理论计算机科学电子笔记298（2013）283-307www.elsevier.com/locate/entcs斑块的范畴理论Samuel Mimram和Cinzia Di GiustoCEA，列表摘要当与远程协作者在同一文档上工作时，通常使用版本控制系统，这是一个跟踪文件历史并帮助导入其他人带来的修改作为补丁的程序。这种系统的实施需要根据用户对文件执行的操作来处理许多情况，因此很难确保所有的角落情况都得到正确解决。在这里，我们采用一种补充方法，而不是验证这样一个系统的实现：我们引入一个理论模型，该模型由它应该满足的普适性质抽象地定义，并对其进行具体描述。文件和补丁，其中合并两个共同初始补丁的结果的操作由pushout定义。由于两个补丁可能是不兼容的，这样的推出不一定存在于类别中，这就提出了一个问题，即哪个类别是表示和操作处于冲突状态的文件的正确类别。我们通过研究有限余极限下的文件范畴的自由完备化给出了答案，并给出了这个范畴的明确描述：它的对象是由配备有传递关系的线标记的有限集合，态射是关于标记和关系的部分函数保留字：范畴论，斑块，共初始斑块1介绍如今，当与远程合作者在同一个文件上工作时（例如，多个作者一起写一篇文章），使用一个程序来跟踪文件的历史并处理导入其他参与者的修改的操作是很常见的。这些被称为版本控制系统（简称VcS）的软件，如git或Darcs，实现了两个主要操作。当用户对文件中的更改感到满意时，它可以将这些更改记录在补丁中（将当前版本和最后记录的版本之间的差异编码的文件），并将其提交给称为存储库的服务器。用户还可以通过将其他用户添加的新补丁导入存储库并对文件应用相应的修改来更新其当前版本的文件。这里要解决的主要困难之一是没有全局的“时间”概念例如，考虑一个具有一个文件A的存储库，1这项工作得到了法国项目ANR-11-INSE-0007 REVER的部分支持1571-0661 © 2013 Elsevier B. V.在CC BY-NC-ND许可下开放访问。http://dx.doi.org/10.1016/j.entcs.2013.09.018284S. 米姆拉姆角Di Giusto/Electronic Notes in Theoretical Computer Science 298（2013）283两个用户U1和U2。 假设u1通过提交补丁f将文件A修改为B，然后由u2导入补丁f，然后u1和u2并发地将文件B修改为C（分别为D）通过提交补丁g（resp. h）的情况。文件的演变在左边描述，补丁的部分排序在中间：H/G E，g，/hC，，GD、Hg，h，C，，D、B，，ff一gBhf，，一现在，假设u2导入补丁g，或者u1导入补丁h。显然，两个补丁合并后的文件在两种情况下应该是相同的，称之为E。 计算这个文件的一种方法是说应该有一个补丁h/g，g之后h的残差，它将C转换为E，并且一旦应用g，就具有因此，在每个用户从另一个用户导入更改后，文件的演变如上图所示。在这篇文章中，我们引入了一个范畴L，其对象是文件和态射是补丁。由于残差应该以最一般的方式计算，我们将其正式定义为推出上锥的箭头，即。右边的正方形应该是外推。然而，正如预期的那样，并不是每对共初始态射在范畴L中都有推出：这反映了两个补丁可以是冲突的事实（例如，如果两个用户修改文件的同一行以一种连贯的方式表示和处理这些冲突是实现一个Vc S的最困难的部分之一（例如，对Darcs的各种建议：合并，constrictor，graphictor等。[10]）。为了能够有一个所有冲突文件的表示，我们研究了范畴L在所有推出下的自由完备化，这个范畴被记为P，这对应于以尽可能一般的方式将所有冲突文件添加到范畴这个范畴可以很容易地被证明存在一般抽象的原因，这项工作的主要贡献之一是提供了一个明确的描述，通过应用理论的预层。这种方法铺平了道路，实现了一个VC S，其正确性是从普遍范畴属性推导出来的。相关工作。Darcs社区已经研究了基于交换性质的补丁的形式化[10]。操作变换通过公理化残差补丁的概念来解决基本相同的问题[9]。在这两种情况下，残数应该形成推出上锥的事实从未被明确地陈述，除了在非正式的句子中说 我们还应该提到[4]中使用逆半群的另一种有趣的方法。最后，休斯顿提出了一个类似于我们的具有推出的范畴，以模拟冲突文件[3]，见第6节。纸的计划 我们首先在第二节中定义文件和补丁的L类，S. 米姆拉姆角Di Giusto/Electronic Notes in Theoretical Computer Science 298（2013）283285第二种情况。然后，在第3节中，我们抽象地定义了由自由有限余补得到的冲突文件的范畴P。第4节提供了一个具体的描述，在更简单的情况下，补丁只能插入线的建设。我们在第5节中给出了一些具体的例子，并在第6节中调整框架以适应一般情况。我们在第7节结束。2文件和补丁在本节中，我们研究一个简化的VcS模型：它只处理一个文件，唯一允许的操作是插入和删除行（行的修改可以通过删除和插入来编码）。我们假设一个集合L ={a，b，... . }行（通常是字符字母表上的单词）。文件A是一个有限的行序列，它将被看作是一个函数A：[n] →L，其中n∈N，其中集合[n] ={0，1，...，n-1}索引的行文件。例如，一个有三条线的文件A，使得A（0）=a，A（1）=b和A（2）=c模拟文件abc。给定a∈L，我们有时简单地将a写为文件A：[1]→L，使得A（0）=a。两个文件A：[m]→L和B：[n]→L之间的态射是一个单射增偏函数f：[m]→[n]，使得当f（i）被定义时，B∈[m]，B ∈f（i）=A（i）这样的态射称为补丁.定义2.1范畴L有作为对象的files和作为态射的patch。注意，范畴L是严格幺半群，[m]<$[n] = [m+n]，并且对于每个文件A：[m]→L和B：[n]→L，如果im，则（A<$B）（i）=A（i），否则（A<$B）（i）=B（i-m），单位是空文件I：[0]→L，并且张量以明显的方式定义在态射上。下面的命题表明，补丁是由插入和删除一行的操作生成的：命题2.2范畴L是包含L作为对象的自由幺半群范畴，并且对于每个线a ∈ L，包含态射ηa：I → a（插入线a）和εa：a→I（删除线a），使得εa <$ηa= id I（删除插入线等于什么都不做）。例2.3通过删除行c并插入标记为d和e的行，将文件abc转换为dadeb所对应的补丁由部分函数f：[3]→[5]建模，使得f（0）= 1，f（1）= 4，f（2）未定义。从图形上看，aDb一cDeb删除的线是f没有定义的线，插入的线是不在f的像中的线。换句话说，f跟踪不变的线。286S. 米姆拉姆角Di Giusto/Electronic Notes in Theoretical Computer Science 298（2013）283我1212我为了增加可读性，我们将考虑L被简化为单个元素的特殊情况。在这种未标记的情况下，L的对象可以用整数来标识（标记函数是平凡的），命题2.2可以被修改以实现对范畴的以下描述，也参见[6]。命题2.4若L约化为单例，则范畴L是自由范畴其对象是整数，态射由sn：n→n+1生成，n：n+1→n，对于每个n∈N和i∈ [n+1]（分别对应于在第i个位置插入和删除一行），服从关系sn+1sn=sn +1sndnsn= idndndn+1=dndn+1（一）ijj+1i i iijj一期+1当0 ≤ i ≤ j<时，我们也将考虑L的子范畴L+，具有相同的对象，和全内射增函数作为态射。命题2.2可以被修改以表明L+是包含态射ηa：I→a的自由monoidal范畴，并且在未标记的情况下，命题2.4可以类似地被修改以表明它是由态射sn：n→n+ 1生成的自由范畴，满足sn+1sn=sn+1sn，其中我0≤i≤jn。i j j+1i3走向一种冲突文件假设A是由两个用户分别应用补丁编辑的文件f1：A→A1和f2：A→A2到文件。 比如说，a、c、bF←−abF−→abcd（2）现在，两个用户中的每一个都从另一个用户导入修改导入后的结果文件应该是包含原始文件的两个修改的最小文件：accbcd。因此，很自然地说，它应该是图（2）的推出。现在，可以注意到，不是L中的每个图都有推出。例如，图a、c、bF←−abF−→adb（3）不允许在L中推出。在这种情况下，两个补丁f1和f2被称为是冲突的。为了表示应用两个冲突补丁后的文件状态，本文研究了范畴P的定义，它是通过在所有推出下完备范畴L而得到的。因为，这个完备化也应该包含一个初始对象（即空文件），我们实际上是把范畴P定义为L在有限余限下的自由完备化：回想一下，一个范畴是有限余完备的（具有所有有限余限）当且仅当它有一个初始对象，并且在DS. 米姆拉姆角Di Giusto/Electronic Notes in Theoretical Computer Science 298（2013）283287pushouts [6].直观地说，这个类别是通过添加行不是线性排序的文件而获得的，而只是部分排序的文件，例如在一cszdzZBZS一<<<<<<<头C=======D>5c55.B（四）这将直观地模拟图（3）的推出（如果它存在的话），指示用户必须在C和D之间选择第二行。 通知 与右边git中相应的文本符号的相似之处。范畴L的名称反映了这样一个事实，即它的对象是线是线性有序的文件，而P的对象可以被认为是线只是部分有序的文件。更正式地说，该类别的定义如下。定义3.1范畴P是L的自由有限保守余完备化：它（直到范畴等价）是唯一的有限余完备范畴，并且有一个嵌入函子y：L→P保持有限余极限，使得对于每个有限余完备范畴C和函子F：L → C保持有限余极限，在唯一同构之前，存在唯一函子F有限极限且满足Fy=F：LFC，JC：P → C保持PF在上面，术语保守指的是我们保持L中已经存在的上极限（我们在这里只考虑这样的完备化）。刻画范畴P的定理3.2范畴L的保守余完备化等价于L的完全子范畴，其对象是一个满足有限极限的集合，即Lop中的极限（或等价于L中的上极限）的像是Set中的极限(and限制锥体被传送到限制锥体）。有限保守的余完备P可以通过进一步限制为表示的有限余极限的预层来获得。例3.3有限集合和函数的范畴FinSet是终结范畴1的保守余完备化。我们还记得，p_resh的范畴L_n是函子L_op→Set和它们之间的自然变换的范畴。Yoneda函子y：L →L通过yn=L（−，n）定义在对象n∈L上，并通过后复合定义在态射上，提供了L到相应的预层范畴中的完全和忠实的嵌入，并且可以被证明为余限制到函子y：L→P[1]。对于某个n∈L，形式为yn的预层称为可表示的。y288S. 米姆拉姆角Di Giusto/Electronic Notes in Theoretical Computer Science 298（2013）2831101从上述命题中提取范畴P的具体描述是一项具有挑战性的任务，因为我们首先需要先验地刻画所有在L中允许上极限的图，其次需要刻画所有在L中存在这些图的预切。本文介绍了一个一般的方法来建立这样一个类别。特别是，也许有点令人惊讶的是，我们必须4文件的共同完成和行的插入为了使我们的表述更清楚，我们将在一个更简单的情况下开始研究范畴P，这将在第6节中推广：我们在标签集是单例的情况下计算范畴L+的自由有限余补（补丁只能插入行）。为了进一步简化符号，在本节中，我们简单地将这个类别写为L。我们有时把L中的对象刻画为L的一个子范畴G中对象的有限余极限。这个范畴G是对象为1和2的L的满子范畴：它是图1上的自由范畴2、将两个字符串分别插入到s1和s1之间。G上的预层的范畴G∈P是G上的预层的范畴：以P（1）为顶点，P（2）为边的图，函数P（s）和P（s）使1 0映射到一个顶点的源和目标，态射对应于图的通常态射。我们用x→y表示这样的图中从顶点x到顶点y的路径。包含函子I：G → L通过预复合导出函子I <$：L<$→G<$。L_n中的一个预层在这个函子下的象称为它的底层图。利用有关预层范畴的已知结果，该函子允许一个RightadjointI：G→L：givenagphG∈G，它在Rightadjoint下的象是G∈L，满足对任意n∈N，G（n+1）是图G中长为n的路的集合，具有期望的源映射，G（0）被约化为一个元素.回想一下，每个函子F：C → D都诱导出一个神经函子NF：D→ C，它在对象A∈ C上定义为NF（A）=D（F−，A）[7]。这里，我们将考虑神经NI：L→G与包含函子I：G→L相关联。 简单的计算表明，n ∈L的象NI（n）是一个有n个顶点的图，使得它的对象同构于[n]，并且对每个i，j∈[n]都有一个箭头i → j，使得1，对象n+ 1是图的L中的余极限S1 2，s，1s 1 2，s1，“2，s，1s，12，s，1（六）1011 10...01 01 1对象1出现n+ 1次，对象2出现n次。因此，对于每个n∈N，P（n+ 1）同构于基础图中长度为n的路的集合。此外，由于图表S1 2，s1，s1 2，s1，s1“2，s1，s12，s1，（七）1 0 11 10 1 0 1 0...111z2，s1S11SS. 米姆拉姆角Di Giusto/Electronic Notes in Theoretical Computer Science 298（2013）283291当对象1出现n + 1次时，对象n + 1也为上极限，则在任意两个顶点x和y之间有P（n+1）n=P（n+1）×P（2），即. 对于每个非空路径x→y，恰好存在一条边x→y。此外，由于292S. 米姆拉姆角Di Giusto/Electronic Notes in Theoretical Computer Science 298（2013）28311 vzss12，，0S10S11L01对象0是L中的初始值，它是空图的上极限。因此，集合P（0）应该是终端集合，即减少到一个元素。最后，由于I是稠密的，P应该是可表示的NI（1）和NI（2）的有限余限，集合P（1）必然是有限的，集合P（2）也必然是有限的，因为两个顶点之间至多有一条边。Q相反，我们希望证明上述命题中所提到的条件恰好符合L中的预变形中P中的预变形。为了证明这一点，通过定理3.2，我们必须证明满足这些条件的预层P在L中保持有限极限，即： 对于每个有限图D：J → L，有一个P（colimD）= lim（P<$Dop）。这似乎很难理解，图承认在L中的余极限，然而下面的引理表明，它足以检查由一个允许有上极限的图“生成”的图引理4.4一个prefP∈Lpr efRe fEl（G）πG I（八）−→ G−→ L对于Set中的极限，当G∈G∈ G ∈G是有限群，使得上图有一个上极限。L中的这样一个图被称为由图G生成。为了证明一个预层P∈L是一个有限极限，我们必须检查它是否把L中允许一个上极限的有限图的上极限发送给Set中的极限，因此我们必须刻画L中允许一个上极限的图.假设给定一个图K：J→ L。因为I是稠密的，所以每个线性对象都是只包含对象1和2的图的余限（见定义4.2）。 我们可以因此，假设这是图K中的情况。最后，可以证明图K与只包含s1和s1的图具有相同的余极限0 1箭头（这些是唯一的非平凡箭头， 其源和目标为1或2），其中每个对象2恰好是一个箭头S1和一个箭头S2的目标。例如，左边下面的L中的图承认与中间的图相同的余极限。2s2s1321s12s1s12s1s12s1，，21，s，0s0S11，0，1，0，1，0，¸¸¸01111 1 1 110 1 2 3sz2，ts0任何这样的图K都是通过粘合有限个以下形式的图来获得的：s1s 1π I112，200，1沿着ob<$1，因此，对于某些情况，nd具有El（G）−→G−→L的形式有限图G∈G<$：G的ob是K中的ob1，G的边是K中的对象2，并分别给出通过相应的箭头S1和S1的源允许其作为目标。为1 0例如，上面中间的图表是由右边的图表生成的每个图都是由一个预层生成的（是一个离散纤维化），这一事实也S. 米姆拉姆角Di Giusto/Electronic Notes in Theoretical Computer Science 298（2013）283293从Cat[8，11]上的综合因式分解系统的构造中得出更抽象和一般的结论。Q在由图生成的图中，可以使用以下命题来表征那些允许共极限的图：引理4.5给定一个群G∈G∈ L，类合diagram（8）在L中有一个极限当且仅当存在n∈ L和L中的一个态射f：G→NIn，使得L中的每个态射g：G→NIm，其中hm∈L，通过NIn唯一分解：GfNnNm我 是$IG证明从[8]的意义下存在NI的部分定义的左伴随，由I是稠密的这一事实给出（见定义4.2）。Q最后，我们得出了允许上极限的图的以下具体特征：引理4.6一个有限群G∈G∈ G，在L中引入一个diagr am（8），它允许colimit当且仅当它是是(i) acyclic：对于任何顶点x，唯一的路径x→x是空路径，(ii) 连通：对于任意一对顶点x和y，存在路径x→y或路径y → x。证明给定一个对象n∈ L，回想一下，NIn是其对象是[ n ]的元素的图，并且存在箭头i → j当且仅当ig（y），所以不存在态射h：NIn→NI（n+1）使得h<$f=g。反之，给定一个有限无圈连通图G，当存在一条路x→y时，由x≤y定义的态射关系≤是全序。记n为G中的顶点数，函数f：G→NIn，它将严格低于它的顶点数wrt≤与一个顶点相关联，在引理4.5的意义下是泛函数。Q命题4.7 L的自由保守有限余完备化P等价于L的完全子范畴，其对象是满足命题4.3条件的集合P。294S. 米姆拉姆角Di Giusto/Electronic Notes in Theoretical Computer Science 298（2013）283→ L∈我...由引理4.4证明，范畴P等价于L∈G的全子范畴，其对象是由某个图G∈ G ∈ G ∈G∈G生成的保极限图的预层，即byLemma4.6无圈连通的有限图我们记Gn为以[n]为顶点和边i→（i+ 1）的图，其中0≤i n− 1。可以证明，任何非循环连通有限图都可以从图Gn中得到，对于某些n∈N，通过迭代地为某些顶点x和y添加边x→y，使得存在非空路径x→y。即，设给定一个无圈连通有限图G.当存在路径x→y时，由x≤y定义的顶点上的关系≤是全序，因此图G包含Gn，其中n是G的边数。G中一条不在Gn中的边必然具有x→y的形式，其中x≤y，否则它不是非循环的。由于命题4.3，见（7），图由以下形式被P中的预层保持（这对应于在非空路径的源和目标处的顶点之间添加一条边），这足以表明P中的预层保持由图Gn生成的图。这又由命题4.3得出，见（6）。Q我们可以注意到，一个预层P∈ P是由它的底层图来刻画的，因为P（0）被简化为一个元素，而P（n）（n > 2）是这个底层图中长度为n的路的集合：P=I（IP）。因此，We可以简化L的共同完成的描述如下：定理4.8 L的自由保守有限余完备化P等价于图的C-图G的全子图，其目标是一个有限图，使得对于每个非空路径x → y，恰好存在一条边x → y。等价地，它可以被描述为这样的范畴，其对象是配备了一个传递关系和函数关系。在这一类别中，推出可以明确描述如下：命题4.9利用上面的最后一个描述，PFG（B，B）<$−（A，A）−→（C，C）是BC/n，其中B3b<$c∈C，只要re存在a ∈ A，满足f（a）= b和f（a）= c，且具有B和C继承的关系<<的传递闭包。带标签的行。这种构造可以扩展到标记的情况（即L不一定是单例）。给集合P（1）发送一个预层P的健忘函子L→集合：设置- 是的 给定nN的元素！L（n）是长度为n/L的字u，其中！L（sn-1）（u）是从u中去掉第i个字母得到的词。 L的自由保守有限余完备化P是 切片类别L/！L，其对象是由有限预层P∈L和标记态射l：P→组成的对（P，l）！我的预处理。或者，命题4.8的描述可以直接通过标记S. 米姆拉姆角Di Giusto/Electronic Notes in Theoretical Computer Science 298（2013）283295一个一B12对象的元素被L的元素替换（标签应该被态射保留），因此证明了在下面的例子中对顶点使用标签的5示例在本节中，我们给出了一些合并（即推出）补丁的例子。例5.1假设从一个文件ab开始，一个用户在开头插入一行a，在中间插入一行c，而另一个用户在中间插入一行d合并两个补丁后，生成的文件是一个afac←−BbFa−→dB也就是cd例5.2对于有一个顶点没有边的图，记为G 1;对于有两个顶点且两顶点之间有一条边的图，记为G 2。对于P中的两个态射，我们记s，t：G1→G2.由于P是有限余完备的，所以存在余积G1+G1，它通过泛性质给出箭头序列：G1+G1→G2：%G%2，，s，，tseq或图形G1G1+G1，，G1我们称之为序列化态射。该态射对应于以下补丁：给定线的两种可能性，用户可以决定将它们转换为两个召唤线。我们也写seq：G1+G1→G2作为类似地通过在上述上锥中交换s和t而得到的态射现在，seq←−−seq′−−→是它说明了循环图如何出现在P中的同时完成L。例 5.3 用 上 例 的 记 号 ， 取 idG1 的 两 个 副 本 的 余 积 ： G1→G1 ， 有 一 个 泛 态 射G1+G1→G1，它说明了两个独立的行如何被一个面片合并（为了解决冲突）。id·合并、、id·你好，6处理行为了计算范畴L+的自由保守有限余完备化，在前面的部分中执行的所有步骤都可以被修改，以便计算范畴L的余完备化P，如定义2.1中所介绍的，因此添加、、S tseq你好，296S. 米姆拉姆角Di Giusto/Electronic Notes in Theoretical Computer Science 298（2013）28312FBBF支持删除补丁中的行。特别地，定理4.8给出的描述的推广结果如下。定理6.1范畴L的自由保守有限余完备化P是其对象为三元组（A，<，l）的范畴，其中A是A上的有限线集，<是A和l上的传递关系：A → L将一个标号与每条线相关联，态射f：（A，

下载后可阅读完整内容，剩余1页未读，立即下载