Can division be expressed intensionally in Relation Algebra?

Question

This blog post gives a nice introduction to relation algebra. However, the division operator is expressed extensionally, i.e. via explicit enumeration of the associated (co)domains.

Is it possible to achieve this intensionally, i.e. when a relation between A and B is represented via a function from A to a set of B?

Answer 1

Author of said post here. I'm not an expert but maybe I can help. I'm interpreting the intensional/extensional question as whether relational division can be performed without the Eq typeclass. The function to set definition I'm going to interpret as using the a -> [b] form to represent a relation R a b. The beauty of a -> [b] form is that relational composition can be performed with no requirements on a. b or c.

rcompose :: (b -> [c]) -> (a -> [b]) -> (a -> [c])
rcompose f g = \a -> [ c | b <- g a, c <- f b]

I believe the answer is no as I have framed it for relational division.

To start off, you want a function of this signature:

rdiv :: (a -> [c]) -> (b -> [c]) -> (a -> [b])

This is basically impossible for the following informal reason: We are given a function that takes an a and produces cs and a function that takes a b and produces cs and we need to make a function that takes a and produces bs. We just don't have anything to work with that produces b, so we can't do it. Formally I believe this can be proved as a free theorem, although I have not worked the details. Now, perhaps we can require some kind of producer of b to get us started. Then we can do almost the only reasonable things we can do to get it into this form.

rdiv :: (BEnum b) => (a -> [c]) -> (b -> [c]) -> (a -> [b])
rdiv g j = \a -> let cs = g a in 
                 [b | b <- enumAll,  all (\c -> ?) (j b)]

We need to somehow do something with the two different [c] lists. I believe at this point, we have to bring in equality which is needed for elem.

rdiv :: (Eq c, BEnum b) =>  (a -> [c]) -> (b -> [c]) -> (a -> [b])
rdiv g j = \a -> let cs = g a in 
                 [b | b <- enumAll,  all (\c -> c `elem` cs) (j b)]

This is however reduced requirements from what I showed in my post. Now, another question might be what representation of division would not require extra type class powers. I'm not sure. It seems plausible they may be out there, especially since we can just partially apply the definition of Eq into our representation of Rel itself or perhaps partially apply rdiv itself and use that a relational representation.

Edit: I had a moment of panic this morning wondering if my above answer was wrong. Relational division is very confusing. Anyone relying on my above answer should really double check it. I am only 70% confident.

I believe the answer is no to the question in the comment below about jinv. The trouble is that rdiv g j can have more b in it than j has in it. The definition of rdiv is that forall r, r . j <= g is equivalent to r <= rdiv g j. This implies that (rdiv g j) is the largest such relation that when composed with j is still less than g. Suppose j is the empty relation. Then (rdiv g j) = top, the complete relation , since anything composed with the empty relation gives the empty relation. We can't get those b's from the empty relation b though, so we're sunk.