connections-0.0.2: Partial orders & Galois connections.

Safe HaskellSafe
LanguageHaskell2010

Data.Prd.Property

Contents

Description

Synopsis

Equivalence relations

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

\( \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 Source #

\( \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 Source #

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

=~ is a reflexive relation.

This is a required property.

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

\( \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 Source #

\( \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 Source #

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

<~ is a reflexive relation.

This is a required property.

transitive_le :: Prd r => r -> r -> r -> Bool Source #

\( \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 Source #

\( \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 Source #

\( \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 Source #

\( \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 Source #

\( \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 Source #

\( \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 Source #

\( \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 Source #

\( \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 Source #