A formalization of real-life license compatibility as a directed graph.

licenses-as-partial-orders.md

An elaboration of concepts proposed in this issue.

Discussion: Licenses as partial orders

Many(/most?) licenses do not adhere to a strict total compatibility ordering; for example, one license may be more strict than another in one regard but less strict in another. This imposes some design constraints on our mechanism for checking compatibility between a package checkout and its dependency:

1. There is a shared, static set of licenses corresponding to valid SPDX identifiers.
2. There will be a shared set of requirements that all licenses impose.
3. Each license declares a set of ⊂ or ⊃ "compatibility" relationships to other licenses along the relevant "requirement" axes.
   • This is to say: each ⊂ or ⊃ corresponds to exactly one requirement.
4. Each package checkout declares at most one license.
5. Each package checkout consumes each of its dependencies in a particular manner, which activates some subset of the license's requirements.
   • This "manner" largely corresponds to the type= argument of the dependency() directive (e.g. links against it vs executes a binary at build time).

Graph definition

Then, let the compatibility relationships between licenses form a directed graph C, where each relationship a ⊂ b for licenses a and b corresponds to an edge e = a -> b, where e has an edge weight r from the set of requirements. Given a package checkout a and its dependency b, define R* as the subset of requirements arising from the manner in which a consumes b.

Graph solution

Define C* as the subgraph of C restricted to vertices {a,b} and edges e_{R*} which have a weight from any element of R*. Then, a and b are marked incompatible if and only if C* contains a cycle.