ANNOUNCE: a relational algebra with only one primitive operator (tentative) (please check/critique)
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 anInnerUnion; they don't seem to have aDUM/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 thata, b, care 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, andcare empty relations with disjoint set of attributes. Then,(a^b)v ris projection ofrontoa^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 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 takea, b, cas any relations and usea ^ R00where the formula has barea.
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
R00doesn't appear in the consequent. (The situation would be different ifR00were 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 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 takea, b, cas any relations and usea ^ R00where the formula has barea.But then it is equivalent to stronger assertion:
b^R00 = b &c^R00 = c-> ...
a with (a^R00).Well no it won't fix anything, because
R00doesn't appear in the consequent. (The situation would be different ifR00were 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.
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.
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.