@@ -134,6 +134,9 @@ module LAoP.Matrix.Internal
134134 toBool,
135135 fromBool,
136136 compRel,
137+ divR,
138+ divL,
139+ divS,
137140 fromFRel,
138141 fromFRel',
139142 toRel,
@@ -787,6 +790,9 @@ prettyPrint = putStrLn . pretty
787790
788791-- Relational operators functions
789792
793+type Boolean = Natural 0 1
794+type Relation a b = Matrix Boolean a b
795+
790796-- | Helper conversion function
791797toBool :: (Num e, Eq e) => e -> Bool
792798toBool n
@@ -799,7 +805,7 @@ fromBool True = nat 1
799805fromBool False = nat 0
800806
801807-- | Relational negation
802−negateM :: Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows
808+negateM :: Relation cols rows -> Relation cols rows
803809negateM Empty = Empty
804810negateM (One (Nat 0)) = One (Nat 1)
805811negateM (One (Nat 1)) = One (Nat 0)
@@ -807,7 +813,7 @@ negateM (Junc a b) = Junc (negateM a) (negateM b)
807813negateM (Split a b) = Split (negateM a) (negateM b)
808814
809815-- | Relational addition
810−orM :: Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows
816+orM :: Relation cols rows -> Relation cols rows -> Relation cols rows
811817orM Empty Empty = Empty
812818orM (One a) (One b) = One (fromBool (toBool a || toBool b))
813819orM (Junc a b) (Junc c d) = Junc (orM a c) (orM b d)
@@ -816,7 +822,7 @@ orM x@(Split _ _) y@(Junc _ _) = orM x (abideJS y)
816822orM x@(Junc _ _) y@(Split _ _) = orM (abideJS x) y
817823
818824-- | Relational multiplication
819−andM :: Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows
825+andM :: Relation cols rows -> Relation cols rows -> Relation cols rows
820826andM Empty Empty = Empty
821827andM (One a) (One b) = One (fromBool (toBool a && toBool b))
822828andM (Junc a b) (Junc c d) = Junc (andM a c) (andM b d)
@@ -825,7 +831,7 @@ andM x@(Split _ _) y@(Junc _ _) = andM x (abideJS y)
825831andM x@(Junc _ _) y@(Split _ _) = andM (abideJS x) y
826832
827833-- | Relational subtraction
828−subM :: Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows
834+subM :: Relation cols rows -> Relation cols rows -> Relation cols rows
829835subM Empty Empty = Empty
830836subM (One a) (One b) = if a - b < nat 0 then One (nat 0) else One (a - b)
831837subM (Junc a b) (Junc c d) = Junc (subM a c) (subM b d)
@@ -834,13 +840,31 @@ subM x@(Split _ _) y@(Junc _ _) = subM x (abideJS y)
834840subM x@(Junc _ _) y@(Split _ _) = subM (abideJS x) y
835841
836842-- | Matrix relational composition.
837−compRel :: Matrix (Natural 0 1) cr rows -> Matrix (Natural 0 1) cols cr -> Matrix (Natural 0 1) cols rows
843+compRel :: Relation cr rows -> Relation cols cr -> Relation cols rows
838844compRel Empty Empty = Empty
839845compRel (One a) (One b) = One (fromBool (toBool a && toBool b))
840−compRel (Junc a b) (Split c d) = orM (compRel a c) (compRel b d) -- Divide-and-conquer law
846+compRel (Junc a b) (Split c d) = orM (compRel a c) (compRel b d) -- Divide-and-conquer law
841847compRel (Split a b) c = Split (compRel a c) (compRel b c) -- Split fusion law
842848compRel c (Junc a b) = Junc (compRel c a) (compRel c b) -- Junc fusion law
843849
850+-- | Matrix relational right division
851+divR :: Relation b c -> Relation b a -> Relation a c
852+divR Empty Empty = Empty
853+divR (One a) (One b) = One (fromBool (not (toBool b) || toBool a)) -- b implies a
854+divR (Junc a b) (Junc c d) = andM (divR a c) (divR b d)
855+divR (Split a b) c = Split (divR a c) (divR b c)
856+divR c (Split a b) = Junc (divR c a) (divR c b)
857+
858+-- | Matrix relational left division
859+divL :: Relation c b -> Relation a b -> Relation a c
860+divL x y = tr (divR (tr y) (tr x))
861+
862+-- | Matrix relational symmetric division
863+divS :: Relation c a -> Relation b a -> Relation c b
864+divS s r = divL r s `intersection` divR (tr r) (tr s)
865+ where
866+ intersection = andM
867+
844868-- | Lifts functions to relations with arbitrary dimensions.
845869--
846870-- NOTE: Be careful to not ask for a relation bigger than the cardinality of
@@ -857,7 +881,7 @@ fromFRel ::
857881 FromLists (Natural 0 1) rows cols
858882 ) =>
859883 (a -> b) ->
860− Matrix (Natural 0 1) cols rows
884+ Relation cols rows
861885fromFRel f =
862886 let minA = minBound @a
863887 maxA = maxBound @a
@@ -891,7 +915,7 @@ fromFRel' ::
891915 FromLists (Natural 0 1) (Normalize b) (Normalize a)
892916 ) =>
893917 (a -> b) ->
894− Matrix (Natural 0 1) (Normalize a) (Normalize b)
918+ Relation (Normalize a) (Normalize b)
895919fromFRel' f =
896920 let minA = minBound @a
897921 maxA = maxBound @a
@@ -923,7 +947,7 @@ toRel ::
923947 KnownNat (Count (Normalize b)),
924948 FromLists (Natural 0 1) (Normalize b) (Normalize a)
925949 )
926− => (a -> b -> Bool) -> Matrix (Natural 0 1) (Normalize a) (Normalize b)
950+ => (a -> b -> Bool) -> Relation (Normalize a) (Normalize b)
927951toRel f =
928952 let minA = minBound @a
929953 maxA = maxBound @a