The Forum for Discussion about The Third Manifesto and Related Matters

Please or Register to create posts and topics.

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

Quote from Vadim on June 21, 2021, 5:57 pm
Quote 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 AntC on June 21, 2021, 11:12 pm

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.

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 Vadim on June 22, 2021, 12:10 am
Quote from AntC on June 21, 2021, 11:12 pm

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.

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

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

 

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 ab, 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.