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 left-relations ofr
.
- pred function[r: univ->univ, s: set univ]
True iff every element of
s
appears exactly once in the left-relations 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
.