Module Labeled.PersistentArray

Persistent array based labeled union-find lattice with values.

Parameters

Signature

type node = Node.t

The type of union-find nodes i.e. the elements of the partition set

type relation = Relation.t

The type of relations between nodes. These relations have a group structure.

type t

The type of the persistent labeled union-find (PUF) data-structure

Union-find operations

val make : int -> t

Create a new union-find, see UNION_FIND_LATTICE.make

val find : t -> node -> node * relation

find uf x returns:

  • the reprensentative of x
  • the relation between x and its representative It performs both the 'find' and 'get_value' operations from the paper.
val add_relation : t -> node -> node -> relation -> (t, relation) Stdlib.result

add_relation uf x y r returns a new persistent union-find, where the relation x --(r)--> y was added.

This is the union operation of classical union find, only this time it takes the new relation as an extra argument.

This fails if x and y were already related by a different relation in uf. In that case, that other relation is returned.

check_related uf x y checks if x and y are in the same relational class in uf. If so, the relation between them is returned. Otherwise, None is returned.

Lattice operations

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

val join : t -> t -> t

join uf_a uf_b is the least upper-bound of uf_a and uf_b, i.e. forall x y, check_related (join uf_a uf_b) x y iff check_related uf_b x y and check_related uf_a x y

val meet : t -> t -> t * (node * relation * node) list

meet uf_a uf_b is a pair meet, extra_rel:

  • meet is (one of) the greatest lower bound of uf_a and uf_b. It contains all relations of uf_a and some of the relations of uf_b. (All nodes that are related in uf_b are still related, but their relation might be changed, as all relations may not be preserved)
  • extra_rel is a minimal list of relations from uf_b that could not be preserved. For example, if uf_a contains x --(r)--> y and uf_b contains x --(r')--> y with r != r', r' will either be in the list, or a transitive/symmetric consequence of relations that are in the list.

Testing and debugging

val copy : t -> t

To compare persistent union-find with non-persistent version, we need an explicit copy operation. This is Fun.id for all persistent versions.

val check_invariants : t -> string option

check_invariants uf is used in testing, to assert that the data-structures internal invariants, if any, are still true after complex operations.

Returns None if they hold, Some error_msg otherwise.

val pretty : Stdlib.Format.formatter -> t -> unit

pretty-printer