@@ -62,6 +62,7 @@ module LAoP.Relation.Internal
6262 toList,
6363 toBool,
6464 pt,
65+ belongs,
6566 relationBuilder,
6667 zeros,
6768 ones,
@@ -197,6 +198,7 @@ instance Num (Relation a b) where
197198 -- | Matrix multiplication becomes Boolean matrix conjunction
198199 (R a) * (R b) = R (I.andM a b)
199200
201+ -- | Matrix negation becomes Boolean matrix negation
200202 negate (R a) = R (I.negateM a)
201203
202204-- Type alias
@@ -222,6 +224,8 @@ junc (R a) (R b) = R (I.Junc a b)
222224
223225infixl 3 |||
224226-- | Boolean Matrix 'Junc' constructor
227+--
228+-- See 'eitherR'.
225229(|||) ::
226230 (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
227231 Relation a c ->
@@ -304,6 +308,22 @@ toRel ::
304308 => (a -> b -> Bool) -> Relation a b
305309toRel = R . I.toRel
306310
311+-- | Lowers a 'Relation' to a function
312+fromRel ::
313+ ( Bounded a,
314+ Bounded b,
315+ Enum a,
316+ Enum b,
317+ Eq a,
318+ Eq b,
319+ KnownNat (I.Count (I.Normalize a)),
320+ KnownNat (I.Count (I.Normalize b)),
321+ I.FromLists Boolean (I.Normalize a) One,
322+ I.FromLists Boolean (I.Normalize b) One
323+ )
324+ => Relation a b -> (a -> b -> Bool)
325+fromRel r a b = pointApBool a b r
326+
307327-- Conversion
308328
309329-- | Converts a matrix to a list of lists of elements.
@@ -314,13 +334,15 @@ toLists (R m) = I.toLists m
314334toList :: Relation a b -> [Boolean]
315335toList (R m) = I.toList m
316336
317−-- | Converts a well typed @'Relation'@ to @'Bool'@.
337+-- | Converts a well typed 'Relation' to 'Bool'.
318338toBool :: Relation One One -> Bool
319339toBool r = case toList r of
320340 [Nat 0] -> False
321341 _ -> True
322342
323−-- | Power transpose
343+-- | Power transpose.
344+--
345+-- Maps a relation to a set valued function.
324346pt ::
325347 ( Bounded a,
326348 Bounded b,
@@ -333,14 +355,36 @@ pt ::
333355 I.FromLists Boolean (I.Normalize a) One,
334356 I.FromLists Boolean (I.Normalize b) One
335357 )
336− => Relation a b -> (a -> [b])
358+ => Relation a b -> (a -> Powerset b)
337359pt r a =
338− let lb = [minBound .. maxBound]
339− in [ b | b <- lb, toBool (pointAp a b r) ]
360+ let (PS lb) = maxBound
361+ in PS [ b | b <- lb, toBool (pointAp a b r) ]
362+
363+-- | Belongs relation
364+belongs ::
365+ ( Bounded a,
366+ Enum a,
367+ Eq a,
368+ KnownNat (I.Count (I.Normalize (Powerset a))),
369+ KnownNat (I.Count (I.Normalize a)),
370+ I.FromLists Boolean (I.Normalize a) (I.Normalize (Powerset a))
371+ )
372+ => Relation (Powerset a) a
373+belongs = toRel (flip elemR)
374+ where
375+ elemR x (PS l) = x `elem` l
340376
341377-- Zeros Matrix
342378
343−-- | The zero matrix. A matrix wholly filled with zeros.
379+-- | The zero relation. A relation where no element of type @a@ relates
380+-- with elements of type @b@.
381+--
382+-- Also known as ⊥ (Bottom) Relation or empty Relation.
383+--
384+-- @
385+-- r `'comp'` ⊥ == ⊥ `'comp'` r == ⊥
386+-- ⊥ `'sse'` R && R `'sse'` T == True
387+-- @
344388zeros ::
345389 (I.FromLists Boolean (I.Normalize a) (I.Normalize b), KnownNat (I.Count (I.Normalize a)), KnownNat (I.Count (I.Normalize b))) =>
346390 Relation a b
@@ -348,9 +392,14 @@ zeros = relationBuilder (const (nat 0))
348392
349393-- Ones Matrix
350394
351−-- | The ones matrix. A matrix wholly filled with ones.
395+-- | The ones relation. A relation where every element of type @a@ relates
396+-- with every element of type @b@.
397+--
398+-- Also known as T (Top) Relation or universal Relation.
352399--
353−-- Also known as T (Top) matrix.
400+-- @
401+-- ⊥ `'sse'` R && R `'sse'` T == True
402+-- @
354403ones ::
355404 (I.FromLists Boolean (I.Normalize a) (I.Normalize b), KnownNat (I.Count (I.Normalize a)), KnownNat (I.Count (I.Normalize b))) =>
356405 Relation a b
@@ -358,7 +407,7 @@ ones = relationBuilder (const (nat 1))
358407
359408-- Bang Matrix
360409
361−-- | The T (Top) row vector matrix.
410+-- | The T (Top) row vector relation.
362411bang ::
363412 (I.FromLists Boolean (I.Normalize a) One, KnownNat (I.Count (I.Normalize a))) =>
364413 Relation a One
@@ -377,24 +426,44 @@ point = fromF' . const
377426-- Identity Matrix
378427
379428-- | Identity matrix
429+--
430+-- @
431+-- 'identity' `'comp'` r == r == r `'comp'` 'identity'
432+-- @
380433identity ::
381434 (I.FromLists Boolean (I.Normalize a) (I.Normalize a), KnownNat (I.Count (I.Normalize a))) =>
382435 Relation a a
383436identity = relationBuilder (bool (nat 0) (nat 1) . uncurry (==))
384437
385438-- | Relational composition
439+--
440+-- @
441+-- r `'comp'` (s `'comp'` p) = (r `'comp'` s) `'comp'` p
442+-- @
386443comp :: Relation b c -> Relation a b -> Relation a c
387444comp (R a) (R b) = R (I.compRel a b)
388445
389446-- | Relational right division
447+--
448+-- @'divR' x y@ is the largest relation @z@ which,
449+-- pre-composed with @y@, approximates @x@.
390450divR :: Relation b c -> Relation b a -> Relation a c
391451divR (R x) (R y) = R (I.divR x y)
392452
393453-- | Relational left division
454+--
455+-- The dual division operator:
456+--
457+-- @
458+-- 'divL' y x == 'conv' ('divR' ('conv' x) ('conv' y)
459+-- @
394460divL :: Relation c b -> Relation a b -> Relation a c
395461divL (R x) (R y) = R (I.divL x y)
396462
397463-- | Relational symmetric division
464+--
465+-- @'pointAp' c b ('divS' s r)@ means that @b@ and @c@
466+-- are related to exactly the same outputs by @r@ and by @s@.
398467divS :: Relation c a -> Relation b a -> Relation c b
399468divS (R x) (R y) = R (I.divS x y)
400469
@@ -422,7 +491,10 @@ overriddenBy ::
422491 ) => Relation a b -> Relation a b -> Relation a b
423492overriddenBy r s = s `union` r `intersection` divR zeros (conv s)
424493
425−-- | Relational application
494+-- | Relational application.
495+--
496+-- If @a@ and @b@ are related by 'Relation' @r@
497+-- then @'pointAp' a b r == 'one' ('Nat' 1)@
426498pointAp ::
427499 ( Bounded a,
428500 Bounded b,
@@ -438,6 +510,8 @@ pointAp ::
438510pointAp a b r = conv (point b) `comp` r `comp` point a
439511
440512-- | Relational application
513+--
514+-- The same as 'pointAp' but converts 'Boolean' to 'Bool'
441515pointApBool ::
442516 ( Bounded a,
443517 Bounded b,
@@ -453,6 +527,12 @@ pointApBool ::
453527pointApBool a b r = toBool $ conv (point b) `comp` r `comp` point a
454528
455529-- | Relational converse
530+--
531+-- Given binary 'Relation' r, writing @'pointAp' a b r@
532+-- (read: “@b@ is related to @a@ by @r@”) means the same as
533+-- @'pointAp' b a ('conv' r)@, where @'conv' r@ is said to be
534+-- the converse of @r@.
535+-- In terms of grammar, @'conv' r@ corresponds to the passive voice
456536conv :: Relation a b -> Relation b a
457537conv (R a) = R (I.tr a)
458538
@@ -471,24 +551,46 @@ iff r s = r == s
471551-- | Relational intersection
472552--
473553-- Lifts pointwise conjunction.
554+--
555+-- @
556+-- (r `'intersection'` s) `'intersection'` t == r `'intersection' (s `'intersection'` t)
557+-- x `'sse'` r `'intersection'` s == x `'intersection'` r && x `'intersection'` s
558+-- @
474559intersection :: Relation a b -> Relation a b -> Relation a b
475560intersection a b = a * b
476561
477562-- | Relational union
478563--
479564-- Lifts pointwise disjunction.
565+--
566+-- @
567+-- (r `'union'` s) `'union'` t == r `'union' (s `'union'` t)
568+-- r `'union'` s `'sse'` x == r `'sse'` x && s `'sse'` x
569+-- r `'comp'` (s `'union'` t) == (r `'comp'` s) `'union'` (r `'comp'` t)
570+-- (s `'union'` t) `'comp'` r == (s `'comp'` r) `'union'` (t `'comp'` r)
571+-- @
480572union :: Relation a b -> Relation a b -> Relation a b
481573union a b = a + b
482574
483575-- | Relation Kernel
576+--
577+-- @
578+-- 'ker' r == 'conv' r `'comp'` r
579+-- 'ker' r == 'img' ('conv' r)
580+-- @
484581ker :: Relation a b -> Relation a a
485582ker r = conv r `comp` r
486583
487584-- | Relation Image
585+--
586+-- @
587+-- 'img' r == r `'comp'` conv r
588+-- 'img' r == 'ker' ('conv' r)
589+-- @
488590img :: Relation a b -> Relation b b
489591img r = r `comp` conv r
490592
491−-- | Function division.
593+-- | Function division. Special case of 'divS'.
492594--
493595-- NOTE: _This is only valid_ if @f@ and @g@ are 'function's, i.e. 'simple' and
494596-- 'entire'.
@@ -499,23 +601,23 @@ divisionF f g = conv g `comp` f
499601
500602-- Taxonomy of binary relations
501603
502−-- | A 'Relation' @r@ is simple iff @'coreflexive' ('img' r)@
604+-- | A 'Relation' @r@ is 'simple' 'iff' @'coreflexive' ('img' r)@
503605simple :: (KnownNat (I.Count (I.Normalize b)), I.FromLists Boolean (I.Normalize b) (I.Normalize b)) => Relation a b -> Bool
504606simple = coreflexive . img
505607
506−-- | A 'Relation' @r@ is injective iff @'coreflexive' ('ker' r)@
608+-- | A 'Relation' @r@ is 'injective' 'iff' @'coreflexive' ('ker' r)@
507609injective :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a b -> Bool
508610injective = coreflexive . ker
509611
510−-- | A 'Relation' @r@ is entire iff @'reflexive' ('ker' r)@
612+-- | A 'Relation' @r@ is 'entire' 'iff' @'reflexive' ('ker' r)@
511613entire :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a b -> Bool
512614entire = reflexive . ker
513615
514−-- | A 'Relation' @r@ is surjective iff @'reflexive' ('img' r)@
616+-- | A 'Relation' @r@ is 'surjective' 'iff' @'reflexive' ('img' r)@
515617surjective :: (KnownNat (I.Count (I.Normalize b)), I.FromLists Boolean (I.Normalize b) (I.Normalize b)) => Relation a b -> Bool
516618surjective = reflexive . img
517619
518−-- | A 'Relation' @r@ is a function iff @'simple' r && 'entire' r@
620+-- | A 'Relation' @r@ is a 'function' 'iff' @'simple' r && 'entire' r@
519621--
520622-- A 'function' @f@ enjoys the following properties, where @r@ and @s@ are binary
521623-- relations:
@@ -533,7 +635,7 @@ function ::
533635 => Relation a b -> Bool
534636function r = simple r && entire r
535637
536−-- | A 'Relation' @r@ is a representation iff @'injective' r && 'entire' r@
638+-- | A 'Relation' @r@ is a 'representation' 'iff' @'injective' r && 'entire' r@
537639representation ::
538640 ( KnownNat (I.Count (I.Normalize a)),
539641 I.FromLists Boolean (I.Normalize a) (I.Normalize a)
@@ -541,7 +643,7 @@ representation ::
541643 => Relation a b -> Bool
542644representation r = injective r && entire r
543645
544−-- | A 'Relation' @r@ is an abstraction iff @'surjective' r && 'simple' r@
646+-- | A 'Relation' @r@ is an 'abstraction' 'iff' @'surjective' r && 'simple' r@
545647abstraction ::
546648 ( KnownNat (I.Count (I.Normalize b)),
547649 I.FromLists Boolean (I.Normalize b) (I.Normalize b)
@@ -549,7 +651,7 @@ abstraction ::
549651 => Relation a b -> Bool
550652abstraction r = surjective r && simple r
551653
552−-- | A 'Relation' @r@ is a surjection iff @'function' r && 'abstraction' r@
654+-- | A 'Relation' @r@ is a 'surjection' 'iff' @'function' r && 'abstraction' r@
553655surjection ::
554656 ( KnownNat (I.Count (I.Normalize b)),
555657 KnownNat (I.Count (I.Normalize a)),
@@ -559,7 +661,7 @@ surjection ::
559661 => Relation a b -> Bool
560662surjection r = function r && abstraction r
561663
562−-- | A 'Relation' @r@ is a injection iff @'function' r && 'representation' r@
664+-- | A 'Relation' @r@ is a 'injection' 'iff' @'function' r && 'representation' r@
563665injection ::
564666 ( KnownNat (I.Count (I.Normalize b)),
565667 KnownNat (I.Count (I.Normalize a)),
@@ -569,7 +671,7 @@ injection ::
569671 => Relation a b -> Bool
570672injection r = function r && representation r
571673
572−-- | A 'Relation' @r@ is an bijection iff @'injection' r && 'surjection' r@
674+-- | A 'Relation' @r@ is an 'bijection' 'iff' @'injection' r && 'surjection' r@
573675bijection ::
574676 ( KnownNat (I.Count (I.Normalize b)),
575677 KnownNat (I.Count (I.Normalize a)),
@@ -581,56 +683,56 @@ bijection r = injection r && surjection r
581683
582684-- Properties of relations
583685
584−-- | A 'Relation' @r@ is reflexive iff @'identity' `'sse'` r@
686+-- | A 'Relation' @r@ is 'reflexive' 'iff' @'identity' `'sse'` r@
585687reflexive :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
586688reflexive r = identity <= r
587689
588−-- | A 'Relation' @r@ is coreflexive iff @r `'sse'` 'identity'@
690+-- | A 'Relation' @r@ is 'coreflexive' 'iff' @r `'sse'` 'identity'@
589691coreflexive :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
590692coreflexive r = r <= identity
591693
592−-- | A 'Relation' @r@ is transitive iff @(r `'comp'` r) `'sse'` r@
694+-- | A 'Relation' @r@ is 'transitive' 'iff' @(r `'comp'` r) `'sse'` r@
593695transitive :: Relation a a -> Bool
594696transitive r = (r `comp` r) `sse` r
595697
596−-- | A 'Relation' @r@ is symmetric iff @r == conv r@
698+-- | A 'Relation' @r@ is 'symmetric' 'iff' @r == 'conv' r@
597699symmetric :: Relation a a -> Bool
598700symmetric r = r == conv r
599701
600−-- | A 'Relation' @r@ is anti-symmetric iff @(r `'intersection'` 'conv' r) `'sse'` 'identity'@
702+-- | A 'Relation' @r@ is anti-symmetric 'iff' @(r `'intersection'` 'conv' r) `'sse'` 'identity'@
601703antiSymmetric :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
602704antiSymmetric r = (r `intersection` conv r) `sse` identity
603705
604−-- | A 'Relation' @r@ is irreflexive iff @(r `'intersection'` identity) == 'zeros'@
706+-- | A 'Relation' @r@ is 'irreflexive' 'iff' @(r `'intersection'` 'identity') == 'zeros'@
605707irreflexive :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
606708irreflexive r = (r `intersection` identity) == zeros
607709
608−-- | A 'Relation' @r@ is connected iff @(r `'union'` 'conv' r) == 'ones'@
710+-- | A 'Relation' @r@ is 'connected' 'iff' @(r `'union'` 'conv' r) == 'ones'@
609711connected :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
610712connected r = (r `union` conv r) == ones
611713
612−-- | A 'Relation' @r@ is a preorder iff @'reflexive' r && 'transitive' r@
714+-- | A 'Relation' @r@ is a 'preorder' 'iff' @'reflexive' r && 'transitive' r@
613715preorder :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
614716preorder r = reflexive r && transitive r
615717
616−-- | A 'Relation' @r@ is a partial order iff @'antiSymmetric' r && 'preorder' r@
718+-- | A 'Relation' @r@ is a partial-order 'iff' @'antiSymmetric' r && 'preorder' r@
617719partialOrder :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
618720partialOrder r = antiSymmetric r && preorder r
619721
620−-- | A 'Relation' @r@ is a linear order iff @'connected' r && 'partialOrder' r@
722+-- | A 'Relation' @r@ is a linear-order 'iff' @'connected' r && 'partialOrder' r@
621723linearOrder :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
622724linearOrder r = connected r && partialOrder r
623725
624−-- | A 'Relation' @r@ is an equivalence iff @'symmetric' r && 'preorder' r@
726+-- | A 'Relation' @r@ is an 'equivalence' 'iff' @'symmetric' r && 'preorder' r@
625727equivalence :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
626728equivalence r = symmetric r && preorder r
627729
628−-- | A 'Relation' @r@ is a partial equivalence iff @'partialOrder' r && 'equivalence' r@
730+-- | A 'Relation' @r@ is a partial-equivalence 'iff' @'partialOrder' r && 'equivalence' r@
629731partialEquivalence :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
630732partialEquivalence r = partialOrder r && equivalence r
631733
632−-- | A 'Relation' @r@ is 'difunctional' or regular wherever @r `comp`
633−-- 'conv' r `comp` r == r@
734+-- | A 'Relation' @r@ is 'difunctional' or regular wherever
735+-- @r `comp` 'conv' r `comp` r == r@
634736difunctional :: Relation a b -> Bool
635737difunctional r = r `comp` conv r `comp` r == r
636738
@@ -647,6 +749,16 @@ difunctional r = r `comp` conv r `comp` r == r
647749-- @
648750--
649751-- __Emphasis__ on the 'sse'.
752+--
753+-- @
754+-- 'splitR' r s `'comp'` f == 'splitR' (r `'comp'` f) (s `'comp'` f)
755+-- (R '><' S) `'comp'` 'splitR' p q == 'splitR' (r `'comp'` p) (s `'comp'` q)
756+-- 'conv' ('splitR' r s) `'comp'` 'splitR' x y == ('conv' r `'comp'` x) `'intersection'` ('conv' s `'comp'` y)
757+-- @
758+--
759+-- @
760+-- 'eitherR' ('splitR' r s) ('splitR' t v) == 'splitR' ('eitherR' r t) ('eitherR' s v)
761+-- @
650762splitR ::
651763 ( KnownNat (I.Count (I.Normalize a)),
652764 KnownNat (I.Count (I.Normalize b)),
@@ -659,6 +771,10 @@ splitR ::
659771splitR (R f) (R g) = R (I.khatri f g)
660772
661773-- | Relational pairing first component projection
774+--
775+-- @
776+-- 'p1' `'comp'` 'splitR' r s `'sse'` r
777+-- @
662778p1 ::
663779 forall a b .
664780 ( KnownNat (I.Count (I.Normalize a)),
@@ -671,6 +787,10 @@ p1 ::
671787p1 = R (I.kp1 @Boolean @(I.Normalize a) @(I.Normalize b))
672788
673789-- | Relational pairing second component projection
790+--
791+-- @
792+-- 'p2' `'comp'` 'splitR' r s `'sse'` s
793+-- @
674794p2 ::
675795 forall a b .
676796 ( KnownNat (I.Count (I.Normalize b)),
@@ -686,6 +806,11 @@ p2 = R (I.kp2 @Boolean @(I.Normalize a) @(I.Normalize b))
686806
687807infixl 4 ><
688808-- | Relational pairing functor
809+--
810+-- @
811+-- r '><' s == 'splitR' (r `'comp'` p1) (s `'comp'` p2)
812+-- (r '><' s) `'comp'` (p '><' q) == (r `'comp'` p) '><' (s `'comp'` q)
813+-- @
689814(><) ::
690815 ( KnownNat (I.Count (I.Normalize a)),
691816 KnownNat (I.Count (I.Normalize b)),
@@ -706,11 +831,31 @@ infixl 4 ><
706831-- Relational co-products
707832
708833-- | Relational coproduct.
834+--
835+-- @
836+-- | 'eitherR' a b `'comp'` 'i1' == a
837+-- 'eitherR' a b <=> |
838+-- | 'eitherR' a b `'comp'` 'i2' == b
839+-- @
840+--
841+-- @
842+-- [R,S]·[T,U]◦= (R·T◦)∪(S·U◦)
843+-- 'eitherR' r s `'comp'` 'conv' ('eitherR' t u) == (r `'comp'` 'conv' t) `'union'` (s `'comp'` 'conv' u)
844+-- @
845+--
846+-- @
847+-- 'eitherR' ('splitR' r s) ('splitR' t v) == 'splitR' ('eitherR' r t) ('eitherR' s v)
848+-- @
709849eitherR :: (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b))
710850 => Relation a c -> Relation b c -> Relation (Either a b) c
711851eitherR = junc
712852
713853-- | Relational coproduct first component injection
854+--
855+-- @
856+-- 'img' 'i1' `union` 'img' 'i2' == 'identity'
857+-- 'i1' `'comp'` 'i2' = 'zeros'
858+-- @
714859i1 ::
715860 ( KnownNat (I.Count (I.Normalize b)),
716861 KnownNat (I.Count (I.Normalize a)),
@@ -722,6 +867,11 @@ i1 ::
722867i1 = R I.i1
723868
724869-- | Relational coproduct second component injection
870+--
871+-- @
872+-- 'img' 'i1' `union` 'img' 'i2' == 'identity'
873+-- 'i1' `'comp'` 'i2' = 'zeros'
874+-- @
725875i2 ::
726876 ( KnownNat (I.Count (I.Normalize b)),
727877 KnownNat (I.Count (I.Normalize a)),
@@ -735,6 +885,10 @@ i2 = R I.i2
735885infixl 5 -|-
736886
737887-- | Relational coproduct functor.
888+--
889+-- @
890+-- r '-|-' s == 'eitherR' ('i1' `'comp'` r) ('i2' `'comp'` s)
891+-- @
738892(-|-) ::
739893 ( KnownNat (I.Count (I.Normalize d)),
740894 KnownNat (I.Count (I.Normalize b)),
@@ -751,6 +905,10 @@ infixl 5 -|-
751905-- Relational "Currying"
752906
753907-- | Relational 'trans'
908+--
909+-- Every n-ary relation can be expressed as a binary relation through
910+-- 'trans'/'untrans';
911+-- more-over, where each particular attribute is placed (input/output) is irrelevant.
754912trans ::
755913 ( KnownNat (I.Count (I.Normalize (a, b))),
756914 KnownNat (I.Count (I.Normalize a)),
@@ -770,6 +928,10 @@ trans ::
770928trans r = splitR r p2 `comp` conv p1
771929
772930-- | Relational 'untrans'
931+--
932+-- Every n-ary relation can be expressed as a binary relation through
933+-- 'trans'/'untrans';
934+-- more-over, where each particular attribute is placed (input/output) is irrelevant.
773935untrans ::
774936 ( KnownNat (I.Count (I.Normalize (a, b))),
775937 KnownNat (I.Count (I.Normalize a)),
@@ -789,6 +951,15 @@ untrans ::
789951untrans s = p1 `comp` conv (splitR (conv s) p2)
790952
791953-- | Transforms predicate @p@ into a correflexive relation.
954+--
955+-- @
956+-- 'predR' ('const' True) == 'identity'
957+-- 'predR' ('const' False) == 'zeros'
958+-- @
959+--
960+-- @
961+-- 'predR' q `'comp'` 'predR' p == 'predR' q `'union'` 'predR' p
962+-- @
792963predR ::
793964 ( Bounded a,
794965 Enum a,
@@ -799,9 +970,14 @@ predR ::
799970 => (a -> Bool) -> Relation a a
800971predR p = identity `intersection` divisionF (fromF' (const True)) (fromF' p)
801972
802−-- | Equalizes functions @f@ and @g@.
973+-- | Equalizes functions @f@ and @g@.
803974-- That is, @'equalizer' f g@ is the largest coreflexive
804975-- that restricts @g@ so that @f@ and @g@ yield the same outputs.
976+--
977+-- @
978+-- 'equalizer' r r == 'identity'
979+-- 'equalizer' ('point' True) ('point' False) == 'zeros'
980+-- @
805981equalizer ::
806982 ( KnownNat (I.Count (I.Normalize a)),
807983 I.FromLists Boolean (I.Normalize a) (I.Normalize a)
@@ -837,6 +1013,9 @@ cond ::
8371013cond p r s = eitherR r s `comp` guard p
8381014
8391015-- | Relational domain.
1016+--
1017+-- For injective relations, 'domain' and 'ker'nel coincide,
1018+-- since @'ker' r `'sse'` 'identity'@ in such situations.
8401019domain ::
8411020 ( KnownNat (I.Count (I.Normalize a)),
8421021 I.FromLists Boolean (I.Normalize a) (I.Normalize a)
@@ -844,6 +1023,9 @@ domain ::
8441023domain r = ker r `intersection` identity
8451024
8461025-- | Relational range.
1026+--
1027+-- For functions, 'range' and 'img' (image) coincide,
1028+-- since@'img' f `'sse'` 'identity'@ for any @f@.
8471029range ::
8481030 ( I.FromLists Boolean (I.Normalize b) (I.Normalize b),
8491031 KnownNat (I.Count (I.Normalize b))