The data type of binary relations. Every pair has an element of an arbitrary data type associated.
List of Import References :
See BOOL
See DENOTATION
See Nat
See Option
See Pair
See Seq
See Set
See Triple
SIGNATURE Rel[dom:SORT, < : dom ** dom -> bool,
$Date: 2010-09-30 18:24:17 +0200 (Do, 30. Sep 2010) $ ($Revision: 616 $)
codom:SORT, < : codom ** codom -> bool,
data]
dom and codom are the domain and codomain of the relation,
data is the data type of the associated elements. The
functions < are assumed to be total orders.
SORT dom codom data FUN < : dom ** dom -> bool FUN < : codom ** codom -> bool
IMPORT Set[dom,<] ONLY set
Set[codom,<] ONLY set
Pair[dom, codom] ONLY pair
Triple[dom, codom, data] ONLY triple
Option[data] ONLY option
Option[pair] ONLY option
Option[triple] ONLY option
Seq[dom] ONLY seq
Seq[codom] ONLY seq
Seq[data] ONLY seq
Nat ONLY nat
SORT rel
Empty relation
FUN {} : rel
Add element to relation. If pair is already in the relation, old associated data is dicarded.
FUN incl: dom ** codom ** data ** rel -> rel FUN incl: dom ** codom ** (dom ** codom -> data) ** rel -> rel
The singleton relation (d :-> c)(#).
FUN :-> : dom ** codom -> data -> rel FUN :-> : dom ** codom -> (dom ** codom -> data) -> rel
Add element to relation
FUN incl: dom ** codom ** data ** rel -> rel
Remove element from relation
FUN excl: dom ** codom ** rel -> rel
Extend relation by pairs of corresponding sequences.Supply data either by a third sequence or by a function.
FUN extend: rel ** seq[dom] ** seq[codom] ** seq[data] -> rel FUN extend: rel ** seq[dom] ** seq[codom] ** (dom ** codom -> data) -> rel
Add all pairs A x B to the relation, use function to compute associated data.
FUN x : set[dom, <] ** set[codom, <] -> (dom ** codom -> data) -> rel FUN x : dom ** set[codom, <] -> (dom ** codom -> data) -> rel FUN x : set[dom, <] ** codom -> (dom ** codom -> data) -> rel
Lift the set operations union, difference, intersection. Associated data is not considered. If a pair (d, c) is element of both relations, but has different data associated, one of the data is chosen arbitrarily.
FUN + : rel ** rel -> rel FUN - : rel ** rel -> rel FUN * : rel ** rel -> rel
Restrict relation to elements whose domain/codomain is element of the given set.
FUN <| : set[dom, <] ** rel -> rel FUN |> : rel ** set[codom, <] -> rel
Restrict relation to elements whose domain/codomain is not element of the given set.
FUN <~| : set[dom, <] ** rel -> rel FUN |~> : rel ** set[codom, <] -> rel
Pick one element of the relation, with or without data.
FUN arb: rel -> dom ** codom FUN arb: rel -> dom ** codom ** data
Get all elements which are in relation with given domain element(s).
FUN ! : rel ** dom -> set[codom, <] FUN ! : rel ** set[dom,<] -> set[codom, <]
Get all elements which are in relation with given codomain element(s).
FUN !_c : rel ** codom -> set[dom, <] FUN !_c : rel ** set[codom,<] -> set[dom, <]
Get associated data.
FUN ! : rel ** dom ** codom -> data FUN !? : rel ** dom ** codom -> option[data]
Empty relation?
FUN {}? : rel -> bool
Pair contained in relation?
FUN in : dom ** codom ** rel -> bool
Is (co)domain element related to some (co)domain element?
FUN def? : rel ** dom -> bool FUN def_c? : rel ** codom -> bool
Size of the relation
FUN # : rel -> nat
Actual domain and codomain of the relation
FUN dom: rel -> set[dom, <] FUN codom: rel -> set[codom, <]
Is relation a bijection or a function?
FUN bijective? : rel -> bool FUN function? : rel -> bool
Minimum and maximum element of the relation
FUN min: rel -> dom ** codom FUN max: rel -> dom ** codom
Check properties of elements, with and without data
FUN exist? : (dom ** codom -> bool) ** rel -> bool
FUN find? : (dom ** codom -> bool) ** rel -> option[pair[dom, codom]]
FUN forall? :(dom ** codom -> bool) ** rel -> bool
FUN exist? : (dom ** codom ** data -> bool) ** rel -> bool
FUN find? : (dom ** codom ** data -> bool) ** rel ->
option[triple[dom, codom, data]]
FUN forall? :(dom ** codom ** data -> bool) ** rel -> bool
Equality, proper subset and subset. Associated data is not considered.
FUN = : rel ** rel -> bool FUN < : rel ** rel -> bool FUN <= :rel ** rel -> bool
Test for disjointness.
FUN disjoint? : rel ** rel -> bool
Total ordering of relations; associated data is not considered.
FUN {<} : rel ** rel -> bool
next node: RelNotForUserPurpose,
prev node: Subsystem Binary Relations,
up to node: Subsystem Binary Relations