Paper detail

The Topological and Logical Structure of Concurrency and Dependency via Distributive Lattices

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.