Distributivity of union over join

August 19, 2014

Recently, Litak & Mikulas & Hidders published the extended version of their earlier work. However, in a typical mathematical tradition following the famous saying “when fine building is revealed to the public eye, the scaffolding should be removed”, reading it requires some detective work. In particular, lets investigate the motivation behind their axiom system:

x ^ (y v z) = (x ^ (z v (R00 ^ y))) v (x ^ (y v (R00 ^ z))). % AxRH1

(R00 ^ (x ^ (y v z))) v (y ^ z) =
= ((R00 ^ (x ^ y)) v z) ^ ((R00 ^ (x ^ z)) v y). % AxRH2

(x ^ y) v (x ^ z) = x ^ ( ((x v z) ^ y) v ((x v y) ^ z) ). % AxRL1

Let’s start with well known lattice inequality

x v (y ^ z) > (x v y) ^ (x v z).

Here we abused notation a little and assume the order symbol > to be reflexive relation. If the LHS of inequality is greater (or equal) than the RHS, then perhaps one can hope to substitute y and z with greater values at RHS, or with lower values at LHS so that inequality becomes an identity? This is the technique employed by Sergey Polin when refuting McKenzie’s conjecture. Specifically, he introduced a non-decreasing chain of values

y1 = y
z1 = z

y2 = y v (x ^ z1).
z2 = z v (x ^ y1).

y3 = y v (x ^ z2).
z3 = z v (x ^ y2).

together with weakened distributivity law

x v (y ^ z) = (x v yN) ^ (x v zN).

Unfortunately, literal Polin-style weakened distributivity law fails in relational lattices for n=1,…,6, at least. However, Polin’s technique can be naturally generalized when an algebra offers constant(s). The axiom AxRH1 is weakened distributivity law with y elevated to y v (R00 ^ z) and z elevated to y v (R00 ^ z).

In a similar venue, the axiom AxRL1 is Polin-style weakening applied to LHS of distributivity law. (Litak et.al. attribute the axiom to Padmanabhan work.)

Genesis of AxRH2 is probably various earlier discovered conditional distributivity identities involving the header relation R00. For professional logician converting implication into equality is a walk in the park.

How about the dual distributivity law of union over join? The stricter conditional distributivity of union over join established in an earlier paper hints that the axiom might be more complicated. One might have to lower/elevate both sides of inequality. After some trial permutations of variables and the header constant R00, it revealed the following identity:

(x v (y ^ (x v z))) ^ (x v (z ^ (x v y))) = x v ((y v (x ^ R00)) ^ (z v (x ^ R00))).

This can be translated into relational calculus expression

(( exists p1 exists p2 exists p6(x(p1,p3,p5,p7) | (y(p2,p3,p6,p7)& exists p1 exists p3 exists p4 exists p6(x(p1,p3,p5,p7) | z(p4,p5,p6,p7))))& exists p1 exists p4 exists p6(x(p1,p3,p5,p7) | (z(p4,p5,p6,p7)& exists p1 exists p5 exists p2 exists p6(x(p1,p3,p5,p7) | y(p2,p3,p6,p7)))))
exists p1(x(p1,p3,p5,p7) | ( exists p2 exists p6 exists p1 exists p5(y(p2,p3,p6,p7) | (x(p1,p3,p5,p7)&$F))& exists p4 exists p6 exists p1 exists p3(z(p4,p5,p6,p7) | (x(p1,p3,p5,p7)&$F))))).

which validity is easily verified with Prover9.

This axiom doesn’t seem to be independent from the {AxRH1,AxRH2,AxRL1} with Mace4 models lookup up to cardinality 26 at least, although Prover9 fails to confirm it after 3 hours running time. (This is not entirely surprising, with union over join distributivity law being often enforced by join over union).


4 Responses to “Distributivity of union over join”

  1. AntC Says:

    Hi Vadim, there is a version of disjunction that is distributive over a version of conjunction – actually over two versions of conjunction.
    Take a relation as a set of tuples with not necessarily the same attributes. Call this a heterogeneous set of tuples. Then disjunction is set union of tuples; conjunction is set intersection. These two operations form a conventional lattice over the powerset of all possible tuples (ordering by subsetting).
    Where it gets interesting is that we can define relational join to apply to heterogeneous sets — as the pairwise join of tuples. And that this join is also distributive across disjunction (set union).
    This join is commutative, associative and has identity DEE aka R01. Unfortunately it’s not idempotent. Neither is it clear how it spreads across the union/intersection lattice. This join is not equivalent to intersection, except where the operands’ tuples all have the same attributes – that is, are union-compatible.

  2. Hi Anthony. I wonder how do you define join when tuples don’t have common value in the common attribute: is it Cartesian join or empty set? For example, what is join of binary relation P(x,y) having one tuple x=1 with unary Q(y) having one tuple y=1? With cartesian join semantics absorption would have been lost, because after join you would be stuck extra “long” tuples. Empty set semantics doesn’t seem to have this problem, but still, say you have joined “normal” relations P(x,y) and Q(y,z). Now you apply union back with P(x,y). What happens with all those ternary tuples, do you apply projection?

  3. AntC Says:

    Thanks Vadim, het-join is very similar to regular relational join:
    take each tuple from one operand; pair it with each tuple from the other; there’s 3 possible outcomes:
    – attribs in common and same values for those,
    then join the two tuples.
    – attribs in common, differing values,
    then discard that pairing.
    – no attribs in common,
    then form the Cartesian product.
    The overall result is the union
    of all those pairings without the discards.
    So note that if the operands are
    regular relations (all tuples in each
    have same attribs), you get exactly the relational join.
    And yes, because the tuples in the operands
    have various attrib-sets,
    the same tuple might match on values in one pairing
    but give the Cartesian product in another pairing.

  4. AntC Says:

    To answer your second example.
    If you het-union P(x, y)
    with (P(x, y) join Q(y, z)),
    yes you get some of the P tuples twice
    (in a sense): both as ternary
    and as twoples.
    But note that you don’t get all
    of the P tuples twice,
    because some didn’t match any Q.
    So a more useful operation is
    (full) outer join defined with het union:
    (P join Q)
    het-union (P not_matching Q)
    het-union (Q not_matching P)

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: