# ANNOUNCE: a relational algebra with only one primitive operator (tentative) (please check/critique)

Quote from AntC on June 21, 2021, 11:12 pmQuote from Vadim on June 21, 2021, 5:57 pmQuote from AntC on June 19, 2021, 12:01 pm

Here is a conditional assertion from page 10 of Yannakakis&Papadimitou "Algebraic dependencies" paper:

Are you sure that's the right link? I see nothing like that on page 10 -- or indeed in the whole paper. They don't seem to have an`InnerUnion`

; they don't seem to have a`DUM/R00`

. 1982 would be before anybody 'discovered'`DUM`

, wouldn't it?On page 10, Figure 2 there is a tableau, and the two nonequivalent project-join expressions.a v b=R00 & b v c=R00 & a v c=R00 -> (a^c)v(((a^b)v r)^( (b^c)v( ((a^c)v r) ^ ((a^b)v ( ((b^c)v r)^( (a^c)v(((b^c)v r)^((a^b)v r)) ) )) ) ) )= (a^c)v( ((a^b)v ( ((b^c)v r)^( (a^c)v(((b^c)v r)^((a^b)v r)) ) )) ^ ( (b^c)v(((a^b)v r)^((a^c)v r)) ) ).It is independent of the Litak et.al. axioms (Mace4 generates counterexample of order 31 which fails to be interpreted as relational universe).

The antecedent

`a v b=R00 & b v c=R00 & a v c=R00 -> ...`

means that`a, b, c`

are all empty (and have mutually disjoint headings). That's hardly a useful place to start -- especially to generate such a monster consequent. Can't we say that the sub-lattice of empty relations is a Boolean algebra?The

`a`

,`b`

, and`c`

are empty relations with disjoint set of attributes. Then,`(a^b)v r`

is projection of`r`

onto`a^b`

, that is the [latex]\pi_{AB}[/latex] tree node at the diagram fig 2, and so on.Hmm we'd like them to be empty relations, but since we're failing to fix

`R00`

, we can't say that's what the antecedent means. We could just take`a, b, c`

as any relations and use`a ^ R00`

where the formula has bare`a`

.The entire assertion has to be valid in the project-join algebra as argued in the paper. Again, it seems to be independent of the three LMH axioms. Unfortunately, adding it into the system (admittedly making it quasi-variety) still doesn't fix the

`R00`

.Well no it won't fix anything, because

`R00`

doesn't appear in the consequent. (The situation would be different if`R00`

were already fixed.)

Quote from Vadim on June 21, 2021, 5:57 pmQuote from AntC on June 19, 2021, 12:01 pm

Here is a conditional assertion from page 10 of Yannakakis&Papadimitou "Algebraic dependencies" paper:

Are you sure that's the right link? I see nothing like that on page 10 -- or indeed in the whole paper. They don't seem to have an`InnerUnion`

; they don't seem to have a`DUM/R00`

. 1982 would be before anybody 'discovered'`DUM`

, wouldn't it?On page 10, Figure 2 there is a tableau, and the two nonequivalent project-join expressions.a v b=R00 & b v c=R00 & a v c=R00 -> (a^c)v(((a^b)v r)^( (b^c)v( ((a^c)v r) ^ ((a^b)v ( ((b^c)v r)^( (a^c)v(((b^c)v r)^((a^b)v r)) ) )) ) ) )= (a^c)v( ((a^b)v ( ((b^c)v r)^( (a^c)v(((b^c)v r)^((a^b)v r)) ) )) ^ ( (b^c)v(((a^b)v r)^((a^c)v r)) ) ).It is independent of the Litak et.al. axioms (Mace4 generates counterexample of order 31 which fails to be interpreted as relational universe).

The antecedent

`a v b=R00 & b v c=R00 & a v c=R00 -> ...`

means that`a, b, c`

are all empty (and have mutually disjoint headings). That's hardly a useful place to start -- especially to generate such a monster consequent. Can't we say that the sub-lattice of empty relations is a Boolean algebra?The

`a`

,`b`

, and`c`

are empty relations with disjoint set of attributes. Then,`(a^b)v r`

is projection of`r`

onto`a^b`

, that is the \pi_{AB} tree node at the diagram fig 2, and so on.

Hmm we'd like them to be empty relations, but since we're failing to fix `R00`

, we can't say that's what the antecedent means. We could just take `a, b, c`

as any relations and use `a ^ R00`

where the formula has bare `a`

.

The entire assertion has to be valid in the project-join algebra as argued in the paper. Again, it seems to be independent of the three LMH axioms. Unfortunately, adding it into the system (admittedly making it quasi-variety) still doesn't fix the

`R00`

.

Well no it won't fix anything, because `R00`

doesn't appear in the consequent. (The situation would be different if `R00`

were already fixed.)

Quote from Vadim on June 22, 2021, 12:10 amQuote from AntC on June 21, 2021, 11:12 pmHmm we'd like them to be empty relations, but since we're failing to fix

`R00`

, we can't say that's what the antecedent means. We could just take`a, b, c`

as any relations and use`a ^ R00`

where the formula has bare`a`

.But then it is equivalent to stronger assertion:

a^R00 = a & b^R00 = b & c^R00 = c -> (a^c)v(((a^b)v r)^( (b^c)v( ((a^c)v r) ^ ((a^b)v ( ((b^c)v r)^( (a^c)v(((b^c)v r)^((a^b)v r)) ) )) ) ) )= (a^c)v( ((a^b)v ( ((b^c)v r)^( (a^c)v(((b^c)v r)^((a^b)v r)) ) )) ^ ( (b^c)v(((a^b)v r)^((a^c)v r)) ) ) .I probed it in QBQL, and it does seem to hold.

Well no it won't fix anything, because

`R00`

doesn't appear in the consequent. (The situation would be different if`R00`

were already fixed.)

But then, per your suggestion applied to stronger conditional assertion we can convert it into equality:

((a^R00)^(c^R00))v((((a^R00)^(b^R00))v r)^( ((b^R00)^(c^R00))v( (((a^R00)^(c^R00))v r) ^ (((a^R00)^(b^R00))v ( (((b^R00)^(c^R00))v r)^( ((a^R00)^(c^R00))v((((b^R00)^(c^R00))v r)^(((a^R00)^(b^R00))v r)) ) )) ) ) )= ((a^R00)^(c^R00))v( (((a^R00)^(b^R00))v ( (((b^R00)^(c^R00))v r)^( ((a^R00)^(c^R00))v((((b^R00)^(c^R00))v r)^(((a^R00)^(b^R00))v r)) ) )) ^ ( ((b^R00)^(c^R00))v((((a^R00)^(b^R00))v r)^(((a^R00)^(c^R00))v r)) ) ) .Again, this is a conjecture at the moment.

More importantly, perhaps there are other tableaux which can be scavenged for less monstrous identities?

Quote from AntC on June 21, 2021, 11:12 pm`R00`

, we can't say that's what the antecedent means. We could just take`a, b, c`

as any relations and use`a ^ R00`

where the formula has bare`a`

.

But then it is equivalent to stronger assertion:

a^R00 = a & b^R00 = b & c^R00 = c -> (a^c)v(((a^b)v r)^( (b^c)v( ((a^c)v r) ^ ((a^b)v ( ((b^c)v r)^( (a^c)v(((b^c)v r)^((a^b)v r)) ) )) ) ) )= (a^c)v( ((a^b)v ( ((b^c)v r)^( (a^c)v(((b^c)v r)^((a^b)v r)) ) )) ^ ( (b^c)v(((a^b)v r)^((a^c)v r)) ) ) .

I probed it in QBQL, and it does seem to hold.

`R00`

doesn't appear in the consequent. (The situation would be different if`R00`

were already fixed.)

But then, per your suggestion applied to stronger conditional assertion we can convert it into equality:

((a^R00)^(c^R00))v((((a^R00)^(b^R00))v r)^( ((b^R00)^(c^R00))v( (((a^R00)^(c^R00))v r) ^ (((a^R00)^(b^R00))v ( (((b^R00)^(c^R00))v r)^( ((a^R00)^(c^R00))v((((b^R00)^(c^R00))v r)^(((a^R00)^(b^R00))v r)) ) )) ) ) )= ((a^R00)^(c^R00))v( (((a^R00)^(b^R00))v ( (((b^R00)^(c^R00))v r)^( ((a^R00)^(c^R00))v((((b^R00)^(c^R00))v r)^(((a^R00)^(b^R00))v r)) ) )) ^ ( ((b^R00)^(c^R00))v((((a^R00)^(b^R00))v r)^(((a^R00)^(c^R00))v r)) ) ) .

Again, this is a conjecture at the moment.

More importantly, perhaps there are other tableaux which can be scavenged for less monstrous identities?

Quote from AntC on June 22, 2021, 12:40 amQuote from Vadim on June 22, 2021, 12:10 amQuote from AntC on June 21, 2021, 11:12 pm`R00`

, we can't say that's what the antecedent means. We could just take`a, b, c`

as any relations and use`a ^ R00`

where the formula has bare`a`

.But then it is equivalent to stronger assertion:

a^R00 = a &b^R00 = b &c^R00 = c-> ...No that antecedent isn't the same (it doesn't say anything about headings being mutually disjoint). Sorry what I meant was the antecedent becomes `(a^R00) v (b^R00) = R00 & (a^R00) v (c^R00) = R00 & (b^R00) v (c^R00) = R00 -> ...And likewise in the consequent replace bare`a`

with`(a^R00)`

.`R00`

doesn't appear in the consequent. (The situation would be different if`R00`

were already fixed.)

More importantly, perhaps there are other tableaux which can be scavenged for less monstrous identities?

The sub-lattice consisting of empty relations is a Boolean algebra. So we get distributivity:

`(a^R00) v ((b^R00) ^ (c^R00)) = ((a^R00) v (b^R00)) ^ ((a^R00) v (c^R00))`

. And we get unique complements in the space`R00`

to`R10`

-- that is if we want to talk about lattice bottom.

Quote from Vadim on June 22, 2021, 12:10 amQuote from AntC on June 21, 2021, 11:12 pm`R00`

, we can't say that's what the antecedent means. We could just take`a, b, c`

as any relations and use`a ^ R00`

where the formula has bare`a`

.But then it is equivalent to stronger assertion:

a^R00 = a &b^R00 = b &c^R00 = c-> ...

`a`

with `(a^R00)`

.`R00`

doesn't appear in the consequent. (The situation would be different if`R00`

were already fixed.)

The sub-lattice consisting of empty relations is a Boolean algebra. So we get distributivity: `(a^R00) v ((b^R00) ^ (c^R00)) = ((a^R00) v (b^R00)) ^ ((a^R00) v (c^R00))`

. And we get unique complements in the space `R00`

to `R10`

-- that is if we want to talk about lattice bottom.

Quote from Vadim on June 22, 2021, 1:51 pmThere seems to be a way to transform the Figure 2 into an identity. Take

`c=R00`

. Then, it's a header relation and its set of attributes is disjoint to`a`

and`b`

Therefore, [latex]\pi_{AC}[/latex] and [latex]\pi_{BC}[/latex] are expressible without any condition. Then, we take a leap of faith and ignore the two remaining conditions that either`a`

or`b`

has to be empty, plus they need to be disjoint:(a^R00)v(((a^b)v r)^( (b^R00)v( ((a^R00)v r) ^ ((a^b)v ( ((b^R00)v r)^( (a^R00)v(((b^R00)v r)^((a^b)v r)) ) )) ) ) ) = (a^R00)v( ((a^b)v ( ((b^R00)v r)^( (a^R00)v(((b^R00)v r)^((a^b)v r)) ) )) ^ ( (b^R00)v(((a^b)v r)^((a^R00)v r)) ) ) .I'm not sure how useful such rather cumbersome identities are, as the LMH system amended with this axiom is still incomplete.

P.S. I don't follow your comment about distributivity of the lattice of header relations. In this example, there is pretty subtle connection between the 4 relations

`a`

,`b`

,`c`

, and`r`

, where`r`

isnot empty.

There seems to be a way to transform the Figure 2 into an identity. Take `c=R00`

. Then, it's a header relation and its set of attributes is disjoint to `a`

and `b`

Therefore, \pi_{AC} and \pi_{BC} are expressible without any condition. Then, we take a leap of faith and ignore the two remaining conditions that either `a`

or `b`

has to be empty, plus they need to be disjoint:

(a^R00)v(((a^b)v r)^( (b^R00)v( ((a^R00)v r) ^ ((a^b)v ( ((b^R00)v r)^( (a^R00)v(((b^R00)v r)^((a^b)v r)) ) )) ) ) ) = (a^R00)v( ((a^b)v ( ((b^R00)v r)^( (a^R00)v(((b^R00)v r)^((a^b)v r)) ) )) ^ ( (b^R00)v(((a^b)v r)^((a^R00)v r)) ) ) .

I'm not sure how useful such rather cumbersome identities are, as the LMH system amended with this axiom is still incomplete.

P.S. I don't follow your comment about distributivity of the lattice of header relations. In this example, there is pretty subtle connection between the 4 relations `a`

, `b`

, `c`

, and `r`

, where `r`

is *not empty*.

Quote from Vadim on June 23, 2021, 2:56 pmLittle more coherent description of the 4th axiom. Again, LMH+4th still doesn't fix R00. However, it is possible that some stronger system does.

Little more coherent description of the 4th axiom. Again, LMH+4th still doesn't fix R00. However, it is possible that some stronger system does.