on master help sign in
Added domain and range functions.

Added difunctional property.

commit0856f03d48edc6348402da9efc361e2b54861768 authorArmando Santos <armandoifsantos@gmail.com> dateTue 28 Jan 2020, 19:54 (7 years ago) parent6a0ea00
1 file changed+27−5
src/LAoP/Relation/Internal.hs+27−5
src/LAoP/Relation/Internal.hs+27−5
@@ -89,6 +89,8 @@ module LAoP.Relation.Internal
8989 injection,
9090 surjection,
9191 bijection,
92+ domain,
93+ range,
9294
9395 -- * Function division
9496 divisionF,
@@ -133,6 +135,7 @@ module LAoP.Relation.Internal
133135 linearOrder,
134136 equivalence,
135137 partialEquivalence,
138+ difunctional,
136139
137140 -- * Conditionals
138141 equalizer,
@@ -606,26 +609,31 @@ irreflexive r = (r `intersection` identity) == zeros
606609connected :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
607610connected r = (r `union` conv r) == ones
608611
609−-- | A 'Relation @r@ is a preorder iff @'reflexive' r && 'transitive' r@
612+-- | A 'Relation' @r@ is a preorder iff @'reflexive' r && 'transitive' r@
610613preorder :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
611614preorder r = reflexive r && transitive r
612615
613−-- | A 'Relation @r@ is a partial order iff @'antiSymmetric' r && 'preorder' r@
616+-- | A 'Relation' @r@ is a partial order iff @'antiSymmetric' r && 'preorder' r@
614617partialOrder :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
615618partialOrder r = antiSymmetric r && preorder r
616619
617−-- | A 'Relation @r@ is a linear order iff @'connected' r && 'partialOrder' r@
620+-- | A 'Relation' @r@ is a linear order iff @'connected' r && 'partialOrder' r@
618621linearOrder :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
619622linearOrder r = connected r && partialOrder r
620623
621−-- | A 'Relation @r@ is an equivalence iff @'symmetric' r && 'preorder' r@
624+-- | A 'Relation' @r@ is an equivalence iff @'symmetric' r && 'preorder' r@
622625equivalence :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
623626equivalence r = symmetric r && preorder r
624627
625−-- | A 'Relation @r@ is a partial equivalence iff @'partialOrder' r && 'equivalence' r@
628+-- | A 'Relation' @r@ is a partial equivalence iff @'partialOrder' r && 'equivalence' r@
626629partialEquivalence :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
627630partialEquivalence r = partialOrder r && equivalence r
628631
632+-- | A 'Relation' @r@ is 'difunctional' or regular wherever @r `comp`
633+-- 'conv' r `comp` r == r@
634+difunctional :: Relation a b -> Bool
635+difunctional r = r `comp` conv r `comp` r == r
636+
629637-- Relational pairing
630638
631639-- | Relational pairing.
@@ -828,6 +836,20 @@ cond ::
828836 => (b -> Bool) -> Relation b c -> Relation b c -> Relation b c
829837cond p r s = eitherR r s `comp` guard p
830838
839+-- | Relational domain.
840+domain ::
841+ ( KnownNat (I.Count (I.Normalize a)),
842+ I.FromLists Boolean (I.Normalize a) (I.Normalize a)
843+ ) => Relation a b -> Relation a a
844+domain r = ker r `intersection` identity
845+
846+-- | Relational range.
847+range ::
848+ ( I.FromLists Boolean (I.Normalize b) (I.Normalize b),
849+ KnownNat (I.Count (I.Normalize b))
850+ ) => Relation a b -> Relation b b
851+range r = img r `intersection` identity
852+
831853-- Relation pretty print
832854
833855-- | Relation pretty printing