git.iko.soy/laop
on master help sign in
Added relational division operators
59f3ebcArmando Santos
src/LAoP/Matrix/Internal.hs+33−9
compare with master
unifiedsplit
@@ -134,6 +134,9 @@ module LAoP.Matrix.Internal
134 toBool,
134 toBool,
135 fromBool,
135 fromBool,
136 compRel,
136 compRel,
137+ divR,
138+ divL,
139+ divS,
137 fromFRel,
140 fromFRel,
138 fromFRel',
141 fromFRel',
139 toRel,
142 toRel,
@@ -787,6 +790,9 @@ prettyPrint = putStrLn . pretty
787
790
788-- Relational operators functions
791-- Relational operators functions
789
792
793+type Boolean = Natural 0 1
794+type Relation a b = Matrix Boolean a b
795+
790-- | Helper conversion function
796-- | Helper conversion function
791toBool :: (Num e, Eq e) => e -> Bool
797toBool :: (Num e, Eq e) => e -> Bool
792toBool n
798toBool n
@@ -799,7 +805,7 @@ fromBool True = nat 1
799fromBool False = nat 0
805fromBool False = nat 0
800
806
801-- | Relational negation
807-- | Relational negation
802−negateM :: Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows
808+negateM :: Relation cols rows -> Relation cols rows
803negateM Empty = Empty
809negateM Empty = Empty
804negateM (One (Nat 0)) = One (Nat 1)
810negateM (One (Nat 0)) = One (Nat 1)
805negateM (One (Nat 1)) = One (Nat 0)
811negateM (One (Nat 1)) = One (Nat 0)
@@ -807,7 +813,7 @@ negateM (Junc a b) = Junc (negateM a) (negateM b)
807negateM (Split a b) = Split (negateM a) (negateM b)
813negateM (Split a b) = Split (negateM a) (negateM b)
808
814
809-- | Relational addition
815-- | 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
811orM Empty Empty = Empty
817orM Empty Empty = Empty
812orM (One a) (One b) = One (fromBool (toBool a || toBool b))
818orM (One a) (One b) = One (fromBool (toBool a || toBool b))
813orM (Junc a b) (Junc c d) = Junc (orM a c) (orM b d)
819orM (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)
816orM x@(Junc _ _) y@(Split _ _) = orM (abideJS x) y
822orM x@(Junc _ _) y@(Split _ _) = orM (abideJS x) y
817
823
818-- | Relational multiplication
824-- | 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
820andM Empty Empty = Empty
826andM Empty Empty = Empty
821andM (One a) (One b) = One (fromBool (toBool a && toBool b))
827andM (One a) (One b) = One (fromBool (toBool a && toBool b))
822andM (Junc a b) (Junc c d) = Junc (andM a c) (andM b d)
828andM (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)
825andM x@(Junc _ _) y@(Split _ _) = andM (abideJS x) y
831andM x@(Junc _ _) y@(Split _ _) = andM (abideJS x) y
826
832
827-- | Relational subtraction
833-- | 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
829subM Empty Empty = Empty
835subM Empty Empty = Empty
830subM (One a) (One b) = if a - b < nat 0 then One (nat 0) else One (a - b)
836subM (One a) (One b) = if a - b < nat 0 then One (nat 0) else One (a - b)
831subM (Junc a b) (Junc c d) = Junc (subM a c) (subM b d)
837subM (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)
834subM x@(Junc _ _) y@(Split _ _) = subM (abideJS x) y
840subM x@(Junc _ _) y@(Split _ _) = subM (abideJS x) y
835
841
836-- | Matrix relational composition.
842-- | 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
838compRel Empty Empty = Empty
844compRel Empty Empty = Empty
839compRel (One a) (One b) = One (fromBool (toBool a && toBool b))
845compRel (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
841compRel (Split a b) c = Split (compRel a c) (compRel b c) -- Split fusion law
847compRel (Split a b) c = Split (compRel a c) (compRel b c) -- Split fusion law
842compRel c (Junc a b) = Junc (compRel c a) (compRel c b) -- Junc fusion law
848compRel c (Junc a b) = Junc (compRel c a) (compRel c b) -- Junc fusion law
843
849
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+
844-- | Lifts functions to relations with arbitrary dimensions.
868-- | Lifts functions to relations with arbitrary dimensions.
845--
869--
846-- NOTE: Be careful to not ask for a relation bigger than the cardinality of
870-- NOTE: Be careful to not ask for a relation bigger than the cardinality of
@@ -857,7 +881,7 @@ fromFRel ::
857 FromLists (Natural 0 1) rows cols
881 FromLists (Natural 0 1) rows cols
858 ) =>
882 ) =>
859 (a -> b) ->
883 (a -> b) ->
860− Matrix (Natural 0 1) cols rows
884+ Relation cols rows
861fromFRel f =
885fromFRel f =
862 let minA = minBound @a
886 let minA = minBound @a
863 maxA = maxBound @a
887 maxA = maxBound @a
@@ -891,7 +915,7 @@ fromFRel' ::
891 FromLists (Natural 0 1) (Normalize b) (Normalize a)
915 FromLists (Natural 0 1) (Normalize b) (Normalize a)
892 ) =>
916 ) =>
893 (a -> b) ->
917 (a -> b) ->
894− Matrix (Natural 0 1) (Normalize a) (Normalize b)
918+ Relation (Normalize a) (Normalize b)
895fromFRel' f =
919fromFRel' f =
896 let minA = minBound @a
920 let minA = minBound @a
897 maxA = maxBound @a
921 maxA = maxBound @a
@@ -923,7 +947,7 @@ toRel ::
923 KnownNat (Count (Normalize b)),
947 KnownNat (Count (Normalize b)),
924 FromLists (Natural 0 1) (Normalize b) (Normalize a)
948 FromLists (Natural 0 1) (Normalize b) (Normalize a)
925 )
949 )
926− => (a -> b -> Bool) -> Matrix (Natural 0 1) (Normalize a) (Normalize b)
950+ => (a -> b -> Bool) -> Relation (Normalize a) (Normalize b)
927toRel f =
951toRel f =
928 let minA = minBound @a
952 let minA = minBound @a
929 maxA = maxBound @a
953 maxA = maxBound @a
src/LAoP/Relation/Internal.hs+19−1
@@ -93,8 +93,14 @@ module LAoP.Relation.Internal
93 -- * Function division
93 -- * Function division
94 divisionF,
94 divisionF,
95
95
96+ -- * Relation division
97+ divR,
98+ divL,
99+ divS,
100+
96 -- * Relational pairing
101 -- * Relational pairing
97 splitR,
102 splitR,
103+
98 -- ** Projections
104 -- ** Projections
99 p1,
105 p1,
100 p2,
106 p2,
@@ -355,7 +361,7 @@ point ::
355 KnownNat (I.Count (I.Normalize a)),
361 KnownNat (I.Count (I.Normalize a)),
356 I.FromLists Boolean (I.Normalize a) One
362 I.FromLists Boolean (I.Normalize a) One
357 ) => a -> Relation One a
363 ) => a -> Relation One a
358−point a = fromF' (const a)
364+point = fromF' . const
359
365
360-- Identity Matrix
366-- Identity Matrix
361
367
@@ -369,6 +375,18 @@ identity = relationBuilder (bool (nat 0) (nat 1) . uncurry (==))
369comp :: Relation b c -> Relation a b -> Relation a c
375comp :: Relation b c -> Relation a b -> Relation a c
370comp (R a) (R b) = R (I.compRel a b)
376comp (R a) (R b) = R (I.compRel a b)
371
377
378+-- | Relational right division
379+divR :: Relation b c -> Relation b a -> Relation a c
380+divR (R x) (R y) = R (I.divR x y)
381+
382+-- | Relational left division
383+divL :: Relation c b -> Relation a b -> Relation a c
384+divL (R x) (R y) = R (I.divL x y)
385+
386+-- | Relational symmetric division
387+divS :: Relation c a -> Relation b a -> Relation c b
388+divS (R x) (R y) = R (I.divS x y)
389+
372-- | Relational application
390-- | Relational application
373pointAp ::
391pointAp ::
374 ( Bounded a,
392 ( Bounded a,