## 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

```[q] a b c```

(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
http://www.cs.unm.edu/~mccune/papers/ltsax/

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).