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

February 12, 2014 at 9:59 pm

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.

February 12, 2014 at 10:05 pm

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

February 12, 2014 at 11:30 pm

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.

February 13, 2014 at 2:45 am

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.

February 17, 2014 at 3:34 am

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 `^`.

February 17, 2014 at 5:51 pm

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