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 to univ.~r.

fun ran[r: univ->univ]

Return type:set univ

Returns the range of r. Equivalent to univ.r.

Predicates

pred total[r: univ->univ, s: set]

True iff every element of s appears in dom[r].

pred functional[r: univ->univ, s: set univ]

True iff every element of s appears at most once in the left-relations of r.

pred function[r: univ->univ, s: set univ]

True iff every element of s appears exactly once in the left-relations of r.

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 in s.

pred bijective[r: univ->univ, s: set univ]

True iff every element of s is mapped to by exactly one relation in r. This is equivalent to being both injective and surjective. There may be relations that map to elements outside of s.

pred bijection[r: univ->univ, d, c: set univ]

True iff exactly r bijects d to c.

pred reflexive[r: univ -> univ, s: set univ]

r maps every element of s 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 than not symmetric: no subset of r 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 of s.

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 set s.

pred totalOrder[r: univ -> univ, s: set univ]

r is a total order over the set s.