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:

A non-injective forward mapping occurs when the same value from the set S is in relation with more than one value from the set K, e.g., (x,s), (y,s) is encoded as Non_injective_fwd ([x,y],s);

A non-injective backward mapping occurs when the same value from the set K is in relation with more than one value from the set S, e.g., (x,r), (x,s) is encoded as Non_injective_bwd ([r;s],x);

type ('k, 's) non_injective =

| Non_injective_fwd of 'k list * 's
(*
Non-injective forward mapping.
*)
| 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.

Install

Dune Dependency

Authors

Maintainers

Sources

doc/bap-relation/Bap_relation/index.html

Module `Bap_relation`

Formal Definition and Notation

Bijections and matching

package bap-relation

Install

Dune Dependency

Authors

Maintainers

Sources

doc/bap-relation/Bap_relation/index.html

Module Bap_relation

Formal Definition and Notation

Bijections and matching

Module `Bap_relation`