通过分配格的并发与依赖的拓扑及逻辑结构

本文的动机是使用函数语言语义的工具包来研究包管理。结果表明，这与并发计算的语义深度相关。我们生成的模型不仅具有理论意义，还可用于分析与计算。本工作做出了若干相关贡献。首先，它将存在于从知识表示到包管理等领域的分支依赖结构规范，与并发计算语义规范联系起来。其次，它以精确方式将依赖结构与格相关联，建立与特定格子类的完全对应。随后利用此对应作为关键要素，并结合未被充分重视的 Bruns-Lakser 完备化，将依赖结构与 locale——兼具拓扑与逻辑性质的对象——相关联。接着给出此性质相互作用如何有用的示例——利用依赖结构的拓扑性质为关联 locale 的内部逻辑配备表示收缩关系（即“版本化”）的模态。该方法使我们能将链接（或更确切地说，选择链接对象，即“求解”）视为一种效应。最后，讨论此类构造如何与复杂性理论中的重要问题相关，包括可满足性问题的解。在此过程中，我们将看到该方法如何与熟悉的对象相关，如包版本策略、Merkle 树、nix 操作系统以及像 git 这样的分布式版本控制工具。