relation¶
All functions and predicates in this module apply to any binary relation. univ is the set of all atoms in the model.
Functions¶

fun
dom[r: univ>univ]
¶  Return type
set univ
Returns the domain of
r
. Equivalent touniv.~r
.

fun
ran[r: univ>univ]
¶  Return type
set univ
Returns the range of
r
. Equivalent touniv.r
.
Predicates¶

pred
total[r: univ>univ, s: set]
¶ True iff every element of
s
appears indom[r]
.

pred
functional[r: univ>univ, s: set univ]
¶ True iff every element of
s
appears at most once in the leftrelations ofr
.

pred
function[r: univ>univ, s: set univ]
¶ True iff every element of
s
appears exactly once in the leftrelations ofr
.

pred
surjective[r: univ>univ, s: set univ]
¶ True iff
s in ran[r]
.

pred
injective[r: univ>univ, s: set univ]
¶ True iff no two elements of
dom[r]
map to the same element ins
.

pred
bijective[r: univ>univ, s: set univ]
¶ True iff every element of
s
is mapped to by exactly one relation inr
. This is equivalent to being both injective and surjective. There may be relations that map to elements outside ofs
.

pred
bijection[r: univ>univ, d, c: set univ]
¶ True iff exactly
r
bijectsd
toc
.

pred
reflexive[r: univ > univ, s: set univ]
¶ r
maps every element ofs
to itself.

pred
irreflexive[r: univ > univ]
¶ r
does not map any element to itself.

pred
symmetric[r: univ > univ]
¶ A > B in r implies B > A in r

pred
antisymmetric[r: univ > univ]
¶ A > B in r implies B > A notin r
. This is stronger thannot symmetric
: no subset ofr
can be symmetric either.

pred
transitive[r: univ > univ]
¶ A > B in r and B  > C in r implies A > C in r

pred
acyclic[r: univ>univ, s: set univ]
¶ r
has no cycles that have elements ofs
.

pred
complete[r: univ>univ, s: univ]
¶ all x,y:s  (x!=y => x>y in (r + ~r))

pred
preorder[r: univ > univ, s: set univ]
¶ reflexive[r, s] and transitive[r]

pred
equivalence[r: univ>univ, s: set univ]
¶ r
is reflexive, transitive, and symmetric over s.

pred
partialOrder[r: univ > univ, s: set univ]
¶ r
is a partial order over the sets
.

pred
totalOrder[r: univ > univ, s: set univ]
¶ r
is a total order over the sets
.