Data.Prd.Property

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

Equivalence relations

symmetric :: Prd r => r -> r -> Bool

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

=~ is a symmetric relation.

This is a required property.

coreflexive :: (Eq r, Prd r) => r -> r -> Bool

\( \forall x, y: x \eq y \Leftrightarrow x == y \)

=~ is a coreflexive relation.

See https://en.wikipedia.org/wiki/Reflexive_relation#Related_terms.

This is a required property.

reflexive_eq :: Prd r => r -> Bool

\( \forall a: (a \eq a) \)

=~ is a reflexive relation.

This is a required property.

transitive_eq :: Prd r => r -> r -> r -> Bool

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

=~ is a transitive relation.

This is a required property.

Partial orders

Non-strict partial orders

antisymmetric :: Prd r => r -> r -> Bool

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

<~ is an antisymmetric relation.

This is a required property.

reflexive_le :: Prd r => r -> Bool

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

<~ is a reflexive relation.

This is a required property.

transitive_le :: Prd 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 non-strict partial orders

connex :: Prd r => r -> r -> Bool

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

<~ is a connex relation.

Strict partial orders

asymmetric :: Eq r => Prd 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 :: Eq r => Prd 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 :: Eq r => Prd r => r -> Bool

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

lt is an irreflexive relation.

This is a required property.

Semiconnex strict partial orders

semiconnex :: Eq r => Prd r => r -> r -> Bool

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

lt is a semiconnex relation.

trichotomous :: Eq r => Prd r => r -> r -> Bool

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

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

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

Semiorders

chain_22 :: Eq r => Prd 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 :: Eq r => Prd r => r -> r -> r -> r -> Bool