Module PolymorphicValued.PersistentArrayNCA

Persistent array based polymorphic labeled union-find lattice with values. Same as PersitentArray, but builds join on the nearest common ancestor instead of one of the branches.

Parameters

module Value : Parameters.POLYMORPHIC_VALUE with type ('a, 'b) relation = ('a, 'b) Relation.t and type 'a node = 'a Node.t

Signature

include Sig.POLYMORPHIC_LABELED_UNION_FIND_LATTICE with type 'a node = 'a Node.t with type ('a, 'b) relation = ('a, 'b) Relation.t
type 'a node = 'a Node.t

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

type ('a, 'b) relation = ('a, 'b) Relation.t

The type of relations. A ('a, 'b) relation relates an 'a node and a 'b node. Mathematically, relations have a group structure.

type t

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

type 'a find_result =
  1. | FindResult : {
    1. representative : 'b node;
    2. relation : ('a, 'b) relation;
    } -> 'a find_result

The true type of find is 'a t -> 'a node -> ∃ 'b. 'b t * ('a, 'b) relation * 'b value option Since we can't express existential types directly in OCaml, we need this wrapper type.

val make : int -> t

Create a new union-find, see UNION_FIND_LATTICE.make

val find : t -> 'a node -> 'a find_result

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 -> 'a node -> 'b node -> ('a, 'b) relation -> (t, ('a, 'b) 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

type wrapped_relation =
  1. | Rel : 'a node * ('a, 'b) relation * 'b node -> wrapped_relation

Existential wrapper for a relation between two nodes, used by meet.

val meet : t -> t -> t * wrapped_relation 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

type 'a value = 'a Value.t

The type of values assigned to relational classes. Relation act as group actions on values: given a ('a, 'b) relation, we can transform a 'a value into a 'b value

val get_value : t -> 'a node -> 'a value option

get_value uf x returns the value attached to x, if it exists.

val set_value : intersect:bool -> t -> 'a node -> 'a value -> t

set_value ~intersect uf n v returns a new union-find, where the value attached to the class of n is now v. If intersect is true, this value will be combined with the previous value (should one exists) via Parameters.VALUE.meet.