PartialOrders Module
This module implements functions for checking whether a given binary relation satisfies some properties of partial orders, directed sets, and lattices. It is restricted, however, to finite relations and sets.
Functions and values
| Function or value | Description |
|
Checks whether the relation rel is a partial order relation, i.e., whether it is reflexive, antisymmetric, and transitive. It returns a triple (missRefl,missAntisym,missTrans) whose sets contain the missing parts, i.e., x missing reflexivity, (x,y) being both with (y,x) in the relation but not being the same, and (x,y,z) in missTrans when (x,y) and (y,z) are in the relation but (x,z) is not.
|
|
Compute the lower and upper bounds for a given set m. The result is a pair (lowerBounds,upperBounds) with the bounds. |
|
|
get the elements that occur in a binary relation rel
|
|
write Hasse diagram to a dot file
|
|
Compute the infimum and the supremum for a given set m. The result is a pair (infimum,supremum) that should be singleton sets when the infimum and supremum, respectively, exists, and is empty otherwise. |
|
|
Check whether a given set m is a directed set in the partial order. It returns a set noUpper of pairs (x,y) that do not have an upper bound, hence, m is a directed set if the returned set is empty.
|
|
Check whether a given set m is a lattice in the partial order. It returns a pair (noInf,noSup) of sets of pairs (x,y) that do not have an infimum and supremum, respectively. |
|
parse a binary relation from a string e.g. "(a,b),(a,c),(a,d),(b,e)"
|
|
PartialOrderTool is the function to be called from the web page; it expects the following key/value pairs:
|
|
compute the reflexive-transitive closure of a binary relation
|
|
remove reflexive and transitive pairs from a relation, e.g. to draw the Hasse diagram
|