Module Bap_relation

A representation of relations between two sets.

A relation between two sets is a set of pairs made from the elements of these sets. The precise mathematical defition is given below. This module implements a bidirectional mapping between two sets and computes their matching that defines bijections between the sets.

Formal Definition and Notation

Given two sets K and S, with meta-variables x,y,z ranging over K and meta-variables r,s,t ranging over S we will denote a finitary relation R as a subset of the cartesian product K x S, which is a set of pairs (x,r), ..., (z,t), which we represent as a bipartite graph G = (K,S,R).

type ('k, 's) t

the type for relation between 'k and 's.

val empty : ('k -> 'k -> int) -> ('s -> 's -> int) -> ('k, 's) t

empty compare_k compare_s the empty relation between two sets.

  • compare_k is the function that defines order of the elements of the set K.
  • compare_s is the function that defines order of the elements of the set S.

Example

let empty = Bap_relation.empty
    Int.compare
    String.compare
val is_empty : (_, _) t -> bool

is_empty rel is true if the relation rel is an empty set.

val add : ('k, 's) t -> 'k -> 's -> ('k, 's) t

add relation x s establishes a relation between x and s.

val mem : ('k, 's) t -> 'k -> 's -> bool

mem rel x s is true if (k,s) is in the relation rel.

val findl : ('k, 's) t -> 'k -> 's list

findl rel x finds all pairs in rel that have x on the left.

val findr : ('k, 's) t -> 's -> 'k list

findr rel s finds all pairs in rel that have s on the right.

val fold : ('k, 's) t -> init:'a -> f:('k -> 's -> 'a -> 'a) -> 'a

fold rel init f folds over all pairs in the relation rel.

val iter : ('k, 's) t -> f:('k -> 's -> unit) -> unit

iter rel f iterates over all pairs in the relation rel.

Bijections and matching

The set of independent edges M (the matching) of the graph G forms a finite bijection between K and S. It is guaranteed that for each pair (x,s) in M there is no other pair in M, that will include x or s.

Edges R that are not in the matching M represent a subset of R that do not match because of one the two anomalies:

type ('k, 's) non_injective =
  1. | Non_injective_fwd of 'k list * 's
    (*

    Non-injective forward mapping.

    *)
  2. | Non_injective_bwd of 's list * 'k
    (*

    Non-injective backward mapping.

    *)

the reason why the pair was left unmatched

val matching : ('k, 's) t -> ?saturated:('k -> 's -> 'a -> 'a) -> ?unmatched:(('k, 's) non_injective -> 'a -> 'a) -> 'a -> 'a

matching relation data computes the matching for the given relation.

Calls saturated x s data for each (x,s) in the matching M (see the module description) and unmatched z reason d for each (z,t) in the relation that are not matched, the reason is one of the:

  • Non_injective_fwd (xs,s) if the mapping K -> S that is induced by the relation is non-injective, because the set of values xs from K are mapped to the same value s in S.
  • Non_injective_bwd (ss,x) if the mapping S -> K that is induced by the relation is non-injective, because the set of values ss from S are mapped to the same value x in K.