[ANN] Union-find-lattice library

Community
1

I’m happy to announce the release of union-find-lattice v0.1.0 to opam ! This library provides a persistent union-find with fast operations to compute the join, meet and inclusion of two union-find instances (i.e. respectively the conjunction, disjunction and implication of the represented equivalence relations).

These new algorithms are best explained in the SAS 26 paper A Lattice of Union-Finds I co-wrote with @Matthieu_Lemerre. We hope to use this data-structure to represent relations between variables in program analysis, but there may well be other uses cases as well.

The core signature of the library is thus a functor of type:

module UF(Node: NODE) = sig
  type t

  (** ==== Standard union-find operations ========= *)
  val make: int -> t
  val find: t -> Node.t
  val union: t -> Node.t -> Node.t -> t
  (** persistent union-find: union does not modify its argument *)

  val check_related: t -> Node.t -> Node.t -> bool
  (** [check_related t a b] is true IFF [a] and [b] are in the same class *)

  (** ==== Lattice operations ====================== *)
  (** Lattice operands run in O(d*alpha(n)) where 
      - n is the number of nodes
      - d is the difference between both arguments (nodes with different parents)
      - alpha is the inverse Ackermann function *)


  val join: t -> t -> t
  (** [check_related (join u v) a v <=> check_related u a b && check_related v a b] *)

  val meet: t -> t -> t
  (** [check_related (meet u v) a v] is true IFF 
      [a] and [b] are related in the transitive closure of [u] and [v], i.e.
      there exists c1 .. cn, [check_related u a c1 && check_related v c1 c2 && .. && check_related u cn b] *)

  val incl: t -> t -> bool
  (** [incl uf_a uf_b] is lattice inclusion, [uf_a <= uf_b], i.e.
      forall [x] [y], if [check_related uf_b x y] then [check_related uf_a x y] *)
end

We provide multiple implementations of this signature:

  • Internally, there three underlying data structure choices: standard arrays (with explicit copy), persistent arrays (same speed as array but pay a cost for all version switches) or Patricia trees (using our patricia-tree library, truly immutable but add a log(nb_unions) cost to all operations).
  • We include variants for labeled union-find (extension which annotates the parent edges with a group of labels, it can represent more complex relations like equality up-to a constant) see our PLDI 25 paper, Relational Abstractions based on Labeled Union-Find and for valued union-find, where each class has a unique associated value (values also have a lattice structure).
10 Likes