Semitopologies model consensus in distributed system by equating the notion of a quorum -- a set of participants sufficient to make local progress -- with that of an open set. This yields a topology-like theory of consensus, but semitopologies generalise topologies, since the intersection of two quorums need not necessarily be a quorum. The semitopological model of consensus is naturally heterogeneous and local, just like topologies can be heterogenous and local, and for the same reasons: points may have different quorums and there is no restriction that open sets / quorums be uniformly generated (e.g. open sets can be something other than two-thirds majorities of the points in the space). Semiframes are an algebraic abstraction of semitopologies. They are to semitopologies as frames are to topologies. We give a notion of semifilter, which plays a role analogous to filters, and show how to build a semiframe out of the open sets of a semitopology, and a semitopology out of the semifilters of a semiframe. We define suitable notions of category and morphism and prove a categorical duality between (sober) semiframes and (spatial) semitopologies, and investigate well-behavedness properties on semitopologies and semiframes across the duality. Surprisingly, the structure of semiframes is not what one might initially expect just from looking at semitopologies, and the canonical structure required for the duality result -- a compatibility relation *, generalising sets intersection -- is also canonical for expressing well-behavedness properties. Overall, we deliver a new categorical, algebraic, abstract framework within which to study consensus on distributed systems, and which is also simply interesting to consider as a mathematical theory in its own right.
翻译:半拓扑通过将法定人数(足以实现局部进展的参与者集合)等同于开集的概念,对分布式系统中的共识进行建模。这产生了类似拓扑的共识理论,但半拓扑是拓扑的推广,因为两个法定人数的交集未必是法定人数。与拓扑一样,半拓扑共识模型天然具有异构性和局部性,原因相同:不同点可能拥有不同的法定人数,且开集/法定人数无需一致生成(例如开集可以是空间中点的三分之二多数以外的其他形式)。半标架是半拓扑的代数抽象——它们之于半拓扑正如标架之于拓扑。我们提出半滤子的概念(其作用类似于滤子),展示如何从半拓扑的开集构建半标架,以及如何从半标架的半滤子构建半拓扑。我们定义了范畴与态射的恰当概念,证明了(sober)半标架与(空间性)半拓扑之间的范畴对偶性,并研究了该对偶性下半拓扑与半标架的良性质。令人惊讶的是,半标架的结构并非仅从半拓扑就能直观推测,而对偶性结果所需的正则结构——兼容关系*(泛化集合交运算)——同时也是表达良性质的正则方式。总体而言,我们提供了一个新的范畴化、代数化、抽象化框架,既可用于研究分布式系统的共识问题,其自身作为数学理论也值得深入探究。