A Mathematical Model of Package Management Systems

TL;DR

This paper develops a mathematical framework using Dependency Structures with Choice (DSC) to model package dependencies and version policies in software systems, linking them to antimatroids and lattice theory.

Contribution

It introduces DSCs as a novel mathematical model for package dependencies, establishing their categorical properties and connections to lattice structures.

Findings

DSCs are isomorphic to the category of antimatroids.

The category of DSCs is finitely complete and has finite coproducts.

A functor relates DSCs to finite distributive lattices, modeling package version policies.

Abstract

This paper brings mathematical tools to bear on the study of package dependencies in software systems. We introduce structures known as Dependency Structures with Choice (DSC) that provide a mathematical account of such dependencies, inspired by the definition of general event structures in the study of concurrency. We equip DSCs with a particular notion of morphism and show that the category of DSCs is isomorphic to the category of antimatroids. We study the exactness properties of these equivalent categories, and show that they are finitely complete, have finite coproducts but not all coequalizers. Further, we construct a functor from a category of DSCs equipped with a certain subclass of morphisms to the opposite of the category of finite distributive lattices, making use of a simple finite characterization of the Bruns-Lakser completion, and finally, we introduce a formal account of versions of packages and introduce a mathematical account of package version-bound policies.