Relation data type.

Boolean type synonym for working with boolean matrices

Constraint type synonyms to keep the type signatures less convoluted

Empty matrix constructor

Unit matrix constructor

Boolean Matrix Junc constructor, also known as relational coproduct.

See eitherR.

Boolean Matrix Junc constructor

See eitherR.

Boolean Matrix Split constructor, also known as relational product.

Boolean Matrix Split constructor

Type family that computes of a given type dimension from a given natural

Thanks to Li-Yao Xia this type family is super fast.

Type family that computes the cardinality of a given type dimension.

It can also count the cardinality of custom types that implement the Generic instance.

Type family that normalizes the representation of a given data structure

Type class for defining the fromList conversion function.

Given that it is not possible to branch on types at the term level type classes are needed bery much like an inductive definition but on types.

Build a matrix out of a list of list of elements. Throws a runtime error if the dimensions do not match.

Lifts functions to matrices with arbitrary dimensions.

NOTE: Be careful to not ask for a matrix bigger than the cardinality of types a or b allows.

Lifts functions to matrices with dimensions matching a and b cardinality's.

Lifts relation functions to Relation

Converts a matrix to a list of lists of elements.

Converts a matrix to a list of elements.

Converts a well typed Relation to Bool.

Power transpose.

Maps a relation to a set valued function.

Belongs relation

Matrix builder function. Constructs a matrix provided with a construction function.

The zero relation. A relation where no element of type a relates with elements of type b.

Also known as ⊥ (Bottom) Relation or empty Relation.

  r `comp` ⊥ == ⊥ `comp` r == ⊥
  ⊥ `sse` R && R `sse` T == True
  

The ones relation. A relation where every element of type a relates with every element of type b.

Also known as T (Top) Relation or universal Relation.

  ⊥ `sse` R && R `sse` T == True
  

The T (Top) row vector relation.

Point constant relation

Relational converse

Given binary Relation r, writing pointAp a b r (read: “b is related to a by r”) means the same as pointAp b a (conv r), where conv r is said to be the converse of r. In terms of grammar, conv r corresponds to the passive voice

Relational intersection

Lifts pointwise conjunction.

(r `intersection` s) `intersection` t == r `intersection` (s `intersection` t)
x `sse` r `intersection` s == x `intersection` r && x `intersection` s

Relational union

Lifts pointwise disjunction.

(r `union` s) `union` t == r `union (s `union` t)
r `union` s `sse` x == r `sse` x && s `sse` x
r `comp` (s `union` t) == (r `comp` s) `union` (r `comp` t)
(s `union` t) `comp` r ==  (s `comp` r) `union` (t `comp` r)

Relational inclusion (subset or equal)

Relational implication (the same as sse)

Relational bi-implication

Relation Kernel

ker r == conv r `comp` r
ker r == img (conv r)

Relation Image

img r == r `comp` conv r
img r == ker (conv r)

A Relation r is injective iff coreflexive (ker r)

A Relation r is entire iff reflexive (ker r)

A Relation r is simple iff coreflexive (img r)

A Relation r is surjective iff reflexive (img r)

A Relation r is a representation iff injective r && entire r

A Relation r is a function iff simple r && entire r

A function f enjoys the following properties, where r and s are binary relations:

f `comp` r `sse` s == r `sse` f `comp` s
r `comp` f `sse` s == r `sse` s `comp` f

A Relation r is an abstraction iff surjective r && simple r

A Relation r is a injection iff function r && representation r

A Relation r is a surjection iff function r && abstraction r

A Relation r is an bijection iff injection r && surjection r

Relational domain.

For injective relations, domain and kernel coincide, since ker r `sse` identity in such situations.

Relational range.

For functions, range and img (image) coincide, since img f `sse` identity for any f.

Function division. Special case of divS.

NOTE: _This is only valid_ if f and g are functions, i.e. simple and entire.

divisionF f g == conv g `comp` f

Relational right division

divR x y is the largest relation z which, pre-composed with y, approximates x.

Relational left division

The dual division operator:

divL y x == conv (divR (conv x) (conv y)

Relational symmetric division

pointAp c b (divS s r) means that b and c are related to exactly the same outputs by r and by s.

Relational shrinking.

r `shrunkBy` s is the largest part of r such that, if it yields an output for an input x, it must be a maximum, with respect to s, among all possible outputs of x by r.

Relational overriding.

r `overriddenBy` s yields the relation which contains the whole of s and that part of r where s is undefined.

zeros `overriddenBy` s == s
r `overriddenBy` zeros == r
r `overriddenBy` r       == r

Relational pairing.

NOTE: That this is not a true categorical product, see for instance:

               | p1 `comp` splitR a b `sse` a 
splitR a b =   |
               | p2 `comp` splitR a b `sse` b

Emphasis on the sse.

splitR r s `comp` f == splitR (r `comp` f) (s `comp` f)
(R >< S) `comp` splitR p q == splitR (r `comp` p) (s `comp` q)
conv (splitR r s) `comp` splitR x y == (conv r `comp` x) `intersection` (conv s `comp` y)

eitherR (splitR r s) (splitR t v) == splitR (eitherR r t) (eitherR s v)

Relational pairing first component projection

p1 `comp` splitR r s `sse` r

Relational pairing second component projection

p2 `comp` splitR r s `sse` s

Relational pairing functor

r >< s == splitR (r `comp` p1) (s `comp` p2)
(r >< s) `comp` (p >< q) == (r `comp` p) >< (s `comp` q)

Relational coproduct.

               | eitherR a b `comp` i1 == a
eitherR a b =  |
               | eitherR a b `comp` i2 == b

eitherR r s `comp` conv (eitherR t u) == (r `comp` conv t) `union` (s `comp` conv u)

eitherR (splitR r s) (splitR t v) == splitR (eitherR r t) (eitherR s v)

Relational coproduct first component injection

img i1 `union` img i2 == identity
i1 `comp` i2 = zeros

Relational coproduct second component injection

img i1 `union` img i2 == identity
i1 `comp` i2 = zeros

Relational coproduct functor.

r -|- s == eitherR (i1 `comp` r) (i2 `comp` s)

Relational trans

Every n-ary relation can be expressed as a binary relation through 'trans'/'untrans'; more-over, where each particular attribute is placed (input/output) is irrelevant.

Relational untrans

Every n-ary relation can be expressed as a binary relation through 'trans'/'untrans'; more-over, where each particular attribute is placed (input/output) is irrelevant.

A Relation r is reflexive iff identity `sse` r

A Relation r is coreflexive iff r `sse` identity

A Relation r is transitive iff (r `comp` r) `sse` r

A Relation r is symmetric iff r == conv r

A Relation r is anti-symmetric iff (r `intersection` conv r) `sse` identity

A Relation r is irreflexive iff (r `intersection` identity) == zeros

A Relation r is connected iff (r `union` conv r) == ones

A Relation r is a preorder iff reflexive r && transitive r

A Relation r is a partial-order iff antiSymmetric r && preorder r

A Relation r is a linear-order iff connected r && partialOrder r

A Relation r is an equivalence iff symmetric r && preorder r

A Relation r is a partial-equivalence iff partialOrder r && equivalence r

A Relation r is difunctional or regular wherever r `comp` conv r `comp` r == r

Equalizes functions f and g. That is, equalizer f g is the largest coreflexive that restricts g so that f and g yield the same outputs.

equalizer r r == identity
equalizer (point True) (point False) == zeros

Transforms predicate p into a correflexive relation.

predR (const True) == identity
predR (const False) == zeros

predR q `comp` predR p == predR q `union` predR p

Relational conditional guard.

guard p = i2 `overriddenBy` i1 `comp` predR p

Relational McCarthy's conditional.

Identity matrix

identity `comp` r == r == r `comp` identity

Relational composition

r `comp` (s `comp` p) = (r `comp` s) `comp` p

Lifts functions to matrices with arbitrary dimensions.

NOTE: Be careful to not ask for a matrix bigger than the cardinality of types a or b allows.

Lifts functions to matrices with dimensions matching a and b cardinality's.

Relational application.

If a and b are related by Relation r then pointAp a b r == one (nat 1)

Relational application

The same as pointAp but converts Boolean to Bool

Relation pretty printing

Relation pretty printing