connections-0.0.2.1: Partial orders & Galois connections.

Data.Prd.Property

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.

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 #