论文标题
通过分布晶格的并发和依赖性的拓扑结构和逻辑结构
The Topological and Logical Structure of Concurrency and Dependency via Distributive Lattices
论文作者
论文摘要
本文是出于渴望使用功能语言语义的工具包研究包装管理的动机。随着它的发展，这与并发计算的语义密切相关。我们生产的模型不仅是理论上的兴趣，而且可以接受分析和计算。这项工作做出了许多相关的贡献。首先，它将分支依赖性结构的规范与从知识代表到软件包管理的字段中存在的规范与并发计算语义的规范有关。其次，它以精确的方式将依赖性结构与晶格联系起来，建立了与特定晶格子类的完整对应关系。然后，它将其用作关键成分，再加上未充分的Bruns-Lakser完成，将依赖性结构与依赖性结构与配备拓扑和逻辑属性的对象联系起来。然后，它提供了一个示例，说明了如何使用这种属性的相互作用 - 使用依赖关系结构的拓扑属性，以配备相关地区的内部逻辑，并具有代表收缩关系的模态（即“版本化”）。这种方法使我们可以将链接（或更确切地说，选择要链接的内容，即“解决”）作为效果。最后，它讨论了这种结构如何与复杂性理论中的重要问题有关，包括令人满意的问题。在此过程中，我们将看到这种方法与熟悉的对象（例如软件包版本策略，默克尔树，Nix操作系统和分布式版本控制工具）等熟悉对象的关系。
This paper is motivated by the desire to study package management using the toolkit of the semantics of functional languages. As it transpires, this is deeply related to the semantics of concurrent computation. The models we produce are not solely of theoretical interest, but amenable to analysis and computation. This work makes a number of related contributions. First, it relates the specification of branching dependency structures, which exist in fields from knowledge-representation to package management, to the specification of semantics of concurrent computation. Second, it relates dependency structures to lattices in a precise way, establishing a full correspondence with a particular subclass of lattices. It then makes use of this as a key ingredient, coupled with the underappreciated Bruns-Lakser completion, in relating dependency structures to locales -- objects equipped with both topological and logical properties. It then provides an example of how this interplay of properties can be of use -- using topological properties of the dependency structure to equip internal logics of associated locales with a modality representing contraction relations (i.e. "versioning"). This approach lets us see linking (or rather, the choice of what to link against, i.e. "solving") as an effect. Finally, it discusses how such constructions may relate to important questions in complexity theory, including solutions of satisfiability problems. Along the way, we will see how this approach relates to familiar objects such as package version policies, Merkle-trees, the nix operating system, and distributed version control tooling like git.
