Union via Join

February 12, 2014

Here is really bizarre technique: one can perform union via join! Consider:

(([p] 0 <OR> [q] a b) <AND> ([p] 1 <OR> [q] c)) v [q];

which outputs


(We assumed domain p to include {0,1} and q to include {a,b,c}, at least). You may object that the expression involves [domain dependent] union operation <OR>, but it is applied for two relations with disjoint attributes, so it is nothing like classic union.

This observation leads to more general assertion:
(z <OR> x) ^ (<NOT>z <OR> y) = (<NOT>z ^ x) <OR> (z ^ y).
which by leveraging relational lattice De Morgan’s law can be rewritten as

(x' ^ z')' ^ (y' ^ z)' = ((z' ^ x)' ^ (z ^ y)')'.

Here we have switched notation a little from D&D to Prover9Mace4, otherwise, it is just too many negation operators to struggle with. Loading this assertion into automatic prover demonstrates that it is not trivial. It doesn’t follow from semi-lattice axioms amended with distributivity of <OR> over join:

x ^ x = x.
x ^ y = y ^ x.
(x ^ y) ^ z = x ^ (y ^ z).
x ^ (y' ^ z')' = ((x ^ y)' ^ (x ^ z)')'.


6 Responses to “Union via Join”

  1. AntC Says:

    Hi Vadim, I think we can do better than that. If we use a non-standard absorption law, we can get inner union via Join.

    This seems to work in Prover9:
    x ^ y = y ^ x. % commut
    (x ^ y) ^ z = x ^ (y ^ z). % assoc
    x ^ (x v y) = x. % absorb A
    all z (x ^ z = x & y ^ z = y
    (x v y) ^ z = (x v y) ). % non-standard absorb

    From those, Prover9 shows:
    ^ is idempotent
    v is commut, assoc, idempotent
    (x v y) is uniique.
    — in those axioms, v appears always as (x v y),
    — we’re exploiting that v is the inverse of ^.

    So (maybe?) we’ve reduced the operations in the RL to one.
    And we can use plain v to get the union over [q] in your example, without risking domain dependence.

  2. AntC Says:

    Rats! WordPress has swallowed my bi-implication sign.
    It should be at the end of the line starting all z.

    To put it as a lattice ordering:
    z lesseq x and z lesseq y EQV
    z lesseq (x v y).

  3. The identity
    all z (x ^ z = x & y ^ z = y <-> (x v y) ^ z = (x v y) ).
    follows from pure lattice axioms (without need of relational specific ones), so I fail to see how it would help.

    • AntC Says:

      Yes. Or … the pure lattice axioms follow from that identity.
      There’s nothing unusual going on: McCune et al. with Prover9 verified a _single_ axiom for Lattices

      What’s different with my choice of axioms is that we can derive the uniqueness of v defined in terms of ^ (with identities) — in the same way you do for antijoin in the 2008 paper.

      Neither is there anything “relational specific” going on: , , the Rnn constants are just operations and elements in the lattice structure.

      It gets relational when we decide to intepret ^ as Natural Join, R00 as TableDum, etc; and make the Lattice operations analagous to operations on attributes and tuples — in other words, map to a model.

    • AntC Says:

      Ha! Apologies, I’m being over-enthusiastic. (Or what an axiomatist would call wrong.)
      I need to add an axiom for idempotence of ^ alongside that non-standard absorption.

      (And that `all z` isn’t really necessary because all variables are implicitly universally qualified.)

      Then both the axioms that mention `v` do so in a tight-bound form `(x v y)`. So we can derive that `v` is unique. That is, `v` is not an independent operation, but determined from `^`.

      • If you have a system with only one binary operation, that is great achievement. Just be sure to complete several doublechecks:
        i. Distributivity (you would have to express one operation in terms of the other) fails with model of size 6 (otherwise, what you most likely have is Boolean algebra)
        ii. 3 axioms from Litak&Hidders&Mikulas are provable, or at least not refuted by model checker. (When “under-specifying” the axiom system I have seen models of size 18).

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 )

Google+ photo

You are commenting using your Google+ 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 )


Connecting to %s

%d bloggers like this: