Data.Prd.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.

Partial orders

consistent :: Prd r => r -> r -> Bool

Check that Lattice methods are internally consistent.

This is a required property.

Non-strict partial orders

antisymmetric_le :: Prd 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 :: 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_le :: Prd r => r -> r -> Bool

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

<~ is a connex relation.

Strict partial orders

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

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

lt is an irreflexive relation.

This is a required property.

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

Equivalence relations

symmetric_eq :: Prd r => r -> r -> Bool

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

~~ is a symmetric relation.

This is a required property.

reflexive_eq :: Prd r => r -> Bool

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

~~ is a reflexive relation.

This is a required property.

transitive_eq :: Prd 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.