Data.Order.Property

See https://en.wikipedia.org/wiki/Binary_relation#Properties.

Documentation

type Rel r b = r -> r -> b

See https://en.wikipedia.org/wiki/Binary_relation#Properties.

Note that these properties do not exhaust all of the possibilities.

As an example over the natural numbers, the relation \(a \# b \) defined by \( a > 2 \) is neither symmetric nor antisymmetric, let alone asymmetric.

(==>) :: Bool -> Bool -> Bool infix 1

(<=>) :: Bool -> Bool -> Bool infix 0

xor :: Symmetric a => a -> a -> a infixl 4

Exclusive or.

xor x y = (x \/ y) /\ (not x \/ not y)

xor3 :: Bool -> Bool -> Bool -> Bool

Orders

preorder :: Preorder r => r -> r -> Bool

Check a Preorder is internally consistent.

This is a required property.

order :: Order r => r -> r -> Bool

Check that an Order is internally consistent.

This is a required property.

Non-strict preorders

antisymmetric_le :: Preorder r => r -> r -> Bool

\( \forall a, b: (a \leq b) \wedge (b \leq a) \Rightarrow a = b \)

<~ is an antisymmetric relation.

This is a required property.

reflexive_le :: Preorder r => r -> Bool

\( \forall a: (a \leq a) \)

<~ is a reflexive relation.

This is a required property.

transitive_le :: Preorder r => r -> r -> r -> Bool

\( \forall a, b, c: ((a \leq b) \wedge (b \leq c)) \Rightarrow (a \leq c) \)

<~ is an transitive relation.

This is a required property.

connex_le :: Preorder r => r -> r -> Bool

\( \forall a, b: ((a \leq b) \vee (b \leq a)) \)

<~ is a connex relation.

Strict preorders

asymmetric_lt :: Preorder r => r -> r -> Bool

\( \forall a, b: (a \lt b) \Rightarrow \neg (b \lt a) \)

lt is an asymmetric relation.

This is a required property.

transitive_lt :: Preorder r => r -> r -> r -> Bool

\( \forall a, b, c: ((a \lt b) \wedge (b \lt c)) \Rightarrow (a \lt c) \)

lt is a transitive relation.

This is a required property.

irreflexive_lt :: Preorder r => r -> Bool

\( \forall a: \neg (a \lt a) \)

lt is an irreflexive relation.

This is a required property.

semiconnex_lt :: Preorder r => r -> r -> Bool

\( \forall a, b: \neg (a = b) \Rightarrow ((a \lt b) \vee (b \lt a)) \)

lt is a semiconnex relation.

trichotomous_lt :: Preorder r => r -> r -> Bool

\( \forall a, b, c: ((a \lt b) \vee (a = b) \vee (b \lt a)) \wedge \neg ((a \lt b) \wedge (a = b) \wedge (b \lt a)) \)

In other words, exactly one of \(a \lt b\), \(a = b\), or \(b \lt a\) holds.

If lt is a trichotomous relation then the set is totally ordered.

Semiorders

chain_22 :: Preorder r => r -> r -> r -> r -> Bool

\( \forall x, y, z, w: x \lt y \wedge y \sim z \wedge z \lt w \Rightarrow x \lt w \)

A semiorder does not allow 2-2 chains.

chain_31 :: Preorder r => r -> r -> r -> r -> Bool

Equivalence relations

symmetric_eq :: Preorder r => r -> r -> Bool

\( \forall a, b: (a = b) \Leftrightarrow (b = a) \)

~~ is a symmetric relation.

This is a required property.

reflexive_eq :: Preorder r => r -> Bool

\( \forall a: (a = a) \)

~~ is a reflexive relation.

This is a required property

transitive_eq :: Preorder r => r -> r -> r -> Bool

\( \forall a, b, c: ((a = b) \wedge (b = c)) \Rightarrow (a = c) \)

~~ is a transitive relation.

This is a required property.

Properties of generic relations

reflexive :: Rel r b -> r -> b

\( \forall a: (a \# a) \)

For example, ≥ is a reflexive relation but > is not.

irreflexive :: Rel r Bool -> r -> Bool

\( \forall a: \neg (a \# a) \)

For example, > is an irreflexive relation, but ≥ is not.

coreflexive :: Rel r Bool -> Rel r Bool -> r -> r -> Bool

\( \forall a, b: ((a \# b) \wedge (b \# a)) \Rightarrow (a \equiv b) \)

For example, the relation over the integers in which each odd number is related to itself is a coreflexive relation. The equality relation is the only example of a relation that is both reflexive and coreflexive, and any coreflexive relation is a subset of the equality relation.

quasireflexive :: Rel r Bool -> r -> r -> Bool

\( \forall a, b: (a \# b) \Rightarrow ((a \# a) \wedge (b \# b)) \)

transitive :: Rel r Bool -> r -> r -> r -> Bool

\( \forall a, b, c: ((a \# b) \wedge (b \# c)) \Rightarrow (a \# c) \)

For example, "is ancestor of" is a transitive relation, while "is parent of" is not.

euclideanL :: Rel r Bool -> r -> Rel r Bool

\( \forall a, b, c: ((b \# a) \wedge (c \# a)) \Rightarrow (b \# c) \)

For example, = is a left Euclidean relation because if x = y and x = z then y = z.

euclideanR :: Rel r Bool -> r -> r -> r -> Bool

\( \forall a, b, c: ((a \# b) \wedge (a \# c)) \Rightarrow (b \# c) \)

For example, = is a right Euclidean relation because if x = y and x = z then y = z.

connex :: Rel r Bool -> r -> r -> Bool

\( \forall a, b: ((a \# b) \vee (b \# a)) \)

For example, ≥ is a connex relation, while 'divides evenly' is not.

A connex relation cannot be symmetric, except for the universal relation.

semiconnex :: Rel r Bool -> Rel r Bool -> r -> r -> Bool

\( \forall a, b: \neg (a \equiv b) \Rightarrow ((a \# b) \vee (b \# a)) \)

A binary relation is semiconnex if it relates all pairs of _distinct_ elements in some way.

A relation is connex if and only if it is semiconnex and reflexive.

trichotomous :: Rel r Bool -> Rel r Bool -> r -> r -> Bool

\( \forall a, b, c: ((a \# b) \vee (a \doteq b) \vee (b \# a)) \wedge \neg ((a \# b) \wedge (a \doteq b) \wedge (b \# a)) \)

In other words, exactly one of \(a \# b\), \(a \doteq b\), or \(b \# a\) holds.

For example, > is a trichotomous relation, while ≥ is not.

Note that trichotomous (>) should hold for any Ord instance.

symmetric :: Rel r Bool -> r -> r -> Bool

\( \forall a, b: (a \# b) \Leftrightarrow (b \# a) \)

For example, "is a blood relative of" is a symmetric relation, because A is a blood relative of B if and only if B is a blood relative of A.

asymmetric :: Rel r Bool -> r -> r -> Bool

\( \forall a, b: (a \# b) \Rightarrow \neg (b \# a) \)

For example, > is an asymmetric relation, but ≥ is not.

A relation is asymmetric if and only if it is both antisymmetric and irreflexive.

antisymmetric :: Rel r Bool -> Rel r Bool -> r -> r -> Bool

\( \forall a, b: (a \# b) \wedge (b \# a) \Rightarrow a \equiv b \)

For example, ≥ is an antisymmetric relation; so is >, but vacuously (the condition in the definition is always false).