Quote from Vadim on October 4, 2019, 5:03 pm

Your complement operation doesn't seem to be well defined. Given:

x ^ y = y ^ x.
(x ^ y) ^ z = x ^ (y ^ z).
x ^ (x v y) = x.
x v y = y v x.
(x v y) v z = x v (y v z).
x v (x ^ y) = x.

x ^ (y v z) = (x ^ (z v (R00 ^ y))) v (x ^ (y v (R00 ^ z))).
(x ^ y) v (x ^ z) = x ^ ( ((x v z) ^ y) v ((x v y) ^ z) ).
(R00 ^ (x ^ (y v z))) v (y ^ z) = ((R00 ^ (x ^ y)) v z) ^ ((R00 ^ (x ^ z)) v y).

x v x' = R01.
x ^ x' = R10.

x ^ R10 = R10.
x v R01 = R01.

x''=x.

then it follows

x ^ (y v z) = (x ^ y) v (x ^ z).

To progress little more, it is tempting to interpret your complement in terms of tuple complement and header complement that I used before. To straighten up terminology and prevent notation confusion for the rest of the message here is the 3 complement-like operations defined in Prover9:

Tuple complement (ordinary quote which doesn't actually require any additional annotation in Prover9):

op(300, postfix, "'" ).

Header complement (backquote):

op(300, postfix, "`" ).

Anthony's complement:

op(300, postfix, "~" ).

I tried interpreting Anthony's complement via the prior 2:

x~ = x'`.

The first identity

x v x~ = R00'.

is a theorem in the axiom system that I will exhibit shortly. The second one

x ^ x~ = R11'.

is not.

The axiom system used (+standard lattice axioms):

x' ^ x = x ^ R00.
x' v x = x v R11.

x` ^ x = R11 ^ x.
x` v x = R00 v x.

x = (x ^ y') v (x ^ y`).     % generalized FDI (decomposition of relation into header and content)

x ^ (y' ^ z')' = ((x ^ y)' ^ (x ^ z)')'.  % distributivity of <OR> over join  

(y` ^ x') v (y' ^ x `) = (y' v x') ^ (y` v x `). % generalized De Morgan's law 

 

 

 

 

 

 

 

 

Quote from AntC on October 4, 2019, 9:00 pm

Quote from Vadim on October 4, 2019, 5:03 pm

Your complement operation doesn't seem to be well defined.

Vadim, that's the standard definition of complement (just substituting your constants for lattice top, bottom), as per the wiki, as per Wolfram, as per the texts I can find. It is not "Anthony's complement". The standard complement is not in general unique, as I said, as per the wiki, etc.

Given: ...

x''=x.

No that does not hold in general. As I said. As the wiki says. It does hold for Relational Lattices if x is empty (or if x = R10, or some other circumstances which are unrealistic for Relational Lattices).

then it follows

x ^ (y v z) = (x ^ y) v (x ^ z).

Yes, that's what brings the connection between complement and distributivity. But we know Relational Lattices are not distributive, so we don't expect double-complement to be identity in general.

I ignored the rest of your message.

Quote from Vadim on October 6, 2019, 7:11 pm

Your new operation - complementation - can be fully expressed in terms of tuple negation, and attribute inversion, and therefore, is well defined:

x~ = x`'.

Note, that in this, corrected version, the operation of tuple negation is applied after attribute inversion, which apparently makes a difference. Please also note, that there is no ambiguity in how this version of complementation is defined.

Now, both identities from your first message

x v x~ = R00'.

and

x ^ x~ = R11'.

are theorems in my system.

Here are some laws that complemetation complies; the weaker form of double negation:

x~~~=x~.

De Morgan's identity

x~ ^ y~ = (x v y)~.

seems to be valid. "Seems to be", because I validated it only in QBQL. Prover9 still spins for the proof, while Mace4 is currently at the model check of domain size 29...

The dual form of De Morgan

x~ v y~ = (x ^ y)~.

is invalid.

Here is another duality identity that seems to be valid:

(y~ ^ x) v (y ^ x~) = (y v x) ^ (y~ v x~).

And weakened distributivity:

x ^ (y~ v z~) = (x ^ y~) v (x ^ z~).

x~ v (y ^ z~) = (x~ v y) ^ (x~ v z~).

Unfortunately if we combine all those findings into the axiom system with (^,v,~,R01) signature, it is still insufficiently powerful to prove

(x ^ y) v (x ^ z) = x ^ ( ((x v z) ^ y) v ((x v y) ^ z) ).

And, finally, to get back to your original question, I have no clue how to define R00 in this system.

Quote from AntC on October 8, 2019, 2:17 am

Quote from Vadim on October 6, 2019, 7:11 pm

Your new operation - complementation -

The wiki citation is to Birkhoff 1961. Complementation is neither "new" nor is it "Anthony's".

can be fully expressed in terms of tuple negation, and attribute inversion, and therefore, is well defined:

x~ = x`'.

Just remind me of your definitions for those operations. IIRC neither of them is well defined and/or they rely on R00 -- which is what I'm trying to fix uniquely. You are not helping.

... I validated it only in QBQL.

As if this wasn't clear already: lattice complement is from the algebraisation for lattices. It's not an operator that makes sense in the implementation of relations/therefore no sense in QBQL nor Appendix A..

 

Prover9 still spins for the proof, while Mace4 is currently at the model check of domain size 29...

Of course. because your negation and inversion operators are not well defined algebraically.

...

And, finally, to get back to your original question, I have no clue how to define R00 in this system.

That's obvious. If you stop the sidetracking, my suggestion is in the first post on this thread. But I'm very unsure how to express it algebraically. I want to start with

I think we can say more about N_j sublattices (looking at Pic 11 on the wiki):

• If the top of the sublattice is R01 (i.e. top of the whole lattice, i.e. DEE):

I want to express: given elements x, y_j that are interval 1 from R01, if x NatJoin y_j is interval 1 from x but that NatJoin is at interval >1 from y_j, x = R00.

Addit:

Going by the wiki definition of 'lattice cover', I'm looking for: R01 is  cover for x, y_j, x is a cover for x NatJoin y_j, y_j > (x NatJoin yj), but y_j not a cover for the NatJoin.

Quote from Vadim on October 8, 2019, 10:41 pm

I doubt the complementation operator that you recruited in this thread can be defined in "more legitimate" fashion than the tuple complement.

Quote from AntC on October 11, 2019, 5:33 am

I'd rather 'stand on the shoulders of giants' (Birkhoff, McCune, Padmanabhan, even Dedekind) and draw from their findings than go in for 'Original Research', as wikipedia moderators call it.

Quote from Vadim on October 8, 2019, 10:41 pm

I doubt the complementation operator that you recruited in this thread can be defined in "more legitimate" fashion than the tuple complement.

I doubt that those great brains would have developed a less-than "legitimate" operation. I think lattice complement is more general than what you're presenting. I think your 'tuple complement' (and 'header complement') can be defined in terms of lattice complement. And that usefully connects it to a well-established and well-researched body of work. Consider ...

• Relational Lattices are in general not distributive. But we know there are sub-lattices embedded that are distributive. Therefore lattice complement within those sub-lattices is well defined, is unique, and its double-complement is identity.
• Take some relation/element of a Relational Lattice x. We know all the relations with the same heading form a distributive sub-lattice: essentially the elements are the powerset of all possible tuples for that heading. The sub-lattice's top is x v R11, its bottom is x ^ R00. We define tuple complement as the lattice complement within that sub-lattice:

x v tcompl(x) = x v R11.
x ^ tcompl(x) = x ^ R00.

tcompl(x) ^ R00 = x ^ R00.         % should be inferred from above definitions.

(I've used a new name tcompl to avoid confusion with Vadim's operator. I think it's unnecessary to say tcompl(x) has same heading as x.)

• We know all headings (that is, all empty relations taken as representing their headings) form a distibutive sub-lattice: essentially the elements are the powerset of all attributes appearing in the lattice. The sub-lattice's top is R00, its bottom is R10. We define heading complement as the lattice complement of the heading of x within that sub-lattice:

(x ^ R00) v hcompl(x ^ R00) = R00. 
(x ^ R00) ^ hcompl(x ^ R00) = R10.

• There's a further, distributive sub-lattice comprising (rather scarily) domain-dependent relations: their headings are the same as the headings for the empty relations; therefore they form a distributive sub-lattice, as the powerset of all attributes; each one's content is all possible tuples for each heading. The sub-lattice's top is R01, its bottom is R11. We define full-heading complement as the lattice complement of the filled-up x within that sub-lattice:

(x v R11) v fhcompl(x v R11) = R01. 
(x v R11) ^ fhcompl(x v R11) = R11.

hcompl(x) = fhcompl(x) ^ R00.      % should be inferred.

I can't avoid using R11 in these definitions; the domain-dependence worries me. I can at least define R11 in terms of less-scary elements: the heading of R11 is the same as the heading of lattice bottom; R11 has the maximum content for that heading; IOW

R11 ^ R00 = R10.
z ^ R00 = R10 <-> R11 ^ z = z.

To think of this geometrically, we have the four 'cardinal points' of a Relational Lattice:

• Top aka R01 aka DEE aka North;
• Bottom aka R10 (aka DUMPTY by my invention) aka South;
• Left aka R00 aka DUM (we wish) aka West;
• Right aka R11 (aka FULL?) aka East.
• The North-West face is a (trivial, two-element DEE-DUM) distributive lattice;
• The South-West face (all the empty relations) is a distributive lattice;
• The North-East face (all maximal relations) is a distributive lattice;
• The South-East face (all possible relations with all possible attributes) is a distributive lattice;
• Each 'slice' on a NE-SW 'slant' (all relations for a given heading) forms an internal face that's a distributive lattice.

So we remain with the only persistent problem: how to define R00 uniquely? (We get lattice top and bottom/R01, R10 'for free' as the identity element and absorbing element respectively of lattice meet ^ aka NaturalJoin.)

 

Quote from Vadim on October 11, 2019, 5:13 pm

Quote from AntC on October 11, 2019, 5:33 am

• Relational Lattices are in general not distributive. But we know there are sub-lattices embedded that are distributive. Therefore lattice complement within those sub-lattices is well defined, is unique, and its double-complement is identity.

Yes, but the two unary operations that I'm promoting have the same property. Even more, tuple complement obeys double complement law over the entire lattice (not just some distributive sublattices).

• Take some relation/element of a Relational Lattice x. We know all the relations with the same heading form a distributive sub-lattice: essentially the elements are the powerset of all possible tuples for that heading. The sub-lattice's top is x v R11, its bottom is x ^ R00. We define tuple complement as the lattice complement within that sub-lattice:

x v tcompl(x) = x v R11.
x ^ tcompl(x) = x ^ R00.

tcompl(x) ^ R00 = x ^ R00.         % should be inferred from above definitions.

(I've used a new name tcompl to avoid confusion with Vadim's operator. I think it's unnecessary to say tcompl(x) has same heading as x.)

As you are using the same two axioms that I use, then I fail to see any difference.

• We know all headings (that is, all empty relations taken as representing their headings) form a distibutive sub-lattice: essentially the elements are the powerset of all attributes appearing in the lattice. The sub-lattice's top is R00, its bottom is R10. We define heading complement as the lattice complement of the heading of x within that sub-lattice:

(x ^ R00) v hcompl(x ^ R00) = R00. 
(x ^ R00) ^ hcompl(x ^ R00) = R10.

This operation is the inversion -- postfix back quote in in the (^,v,',`) axiom system that I posted couple messages back. Both identities are theorems.

• There's a further, distributive sub-lattice comprising (rather scarily) domain-dependent relations: their headings are the same as the headings for the empty relations; therefore they form a distributive sub-lattice, as the powerset of all attributes; each one's content is all possible tuples for each heading. The sub-lattice's top is R01, its bottom is R11. We define full-heading complement as the lattice complement of the filled-up x within that sub-lattice:

(x v R11) v fhcompl(x v R11) = R01. 
(x v R11) ^ fhcompl(x v R11) = R11.

hcompl(x) = fhcompl(x) ^ R00.      % should be inferred.

This is inversion as well.

I can't avoid using R11 in these definitions; the domain-dependence worries me. I can at least define R11 in terms of less-scary elements: the heading of R11 is the same as the heading of lattice bottom; R11 has the maximum content for that heading; IOW

R11 ^ R00 = R10.
z ^ R00 = R10 <-> R11 ^ z = z.

To think of this geometrically, we have the four 'cardinal points' of a Relational Lattice:

• Top aka R01 aka DEE aka North;
• Bottom aka R10 (aka DUMPTY by my invention) aka South;
• Left aka R00 aka DUM (we wish) aka West;
• Right aka R11 (aka FULL?) aka East.
• The North-West face is a (trivial, two-element DEE-DUM) distributive lattice;
• The South-West face (all the empty relations) is a distributive lattice;
• The North-East face (all maximal relations) is a distributive lattice;
• The South-East face (all possible relations with all possible attributes) is a distributive lattice;
• Each 'slice' on a NE-SW 'slant' (all relations for a given heading) forms an internal face that's a distributive lattice.

So we remain with the only persistent problem: how to define R00 uniquely? (We get lattice top and bottom/R01, R10 'for free' as the identity element and absorbing element respectively of lattice meet ^ aka NaturalJoin.)

The other perspective to your geometric picture would be that there is second lattice structure with R11 as top and R00 as bottom. Take Hasse diagram of the original lattice and reorient the edges so that in order for element S to cover R, the header of R should be subset of the header S, and the tuple content of S projected to attributes of R should be superset of the tuple content of R. (In "classic" relational lattice those conditions are the opposite). At the moment I don't know any identities that hold in that lattice (those from Litak & Mikulas & Hidders paper don't carry over).

P.S. I tried uploading an image, but after I choose to upload the file nothing happens. Here it is; from another wordpress website:-)

 

 

Quote from Dave Voorhis on October 11, 2019, 11:51 pm

Quote from Vadim on October 11, 2019, 5:13 pm

P.S. I tried uploading an image, but after I choose to upload the file nothing happens.

How did you upload the image?

I just tried it -- via the "Upload Files" mechanism below the message edit box -- and it worked.

Here's an image:

 

Quote from AntC on October 12, 2019, 7:28 am

Quote from Vadim on October 11, 2019, 5:13 pm

Quote from AntC on October 11, 2019, 5:33 am

• Relational Lattices are in general not distributive. But we know there are sub-lattices embedded that are distributive. Therefore lattice complement within those sub-lattices is well defined, is unique, and its double-complement is identity.

Yes, but the two unary operations that I'm promoting have the same property.

For the umpteenth time, I did not start this thread to 'promote' some operation. What I'm trying to do is build on well-established work, to get insights into the lattice structure, to fix R00 as corresponding to DUM. What you've failed to do with the "operations that I'm promoting" is show how they build on what is already established.

• Take some relation/element of a Relational Lattice x. We know all the relations with the same heading form a distributive sub-lattice: essentially the elements are the powerset of all possible tuples for that heading. The sub-lattice's top is x v R11, its bottom is x ^ R00. We define tuple complement as the lattice complement within that sub-lattice:

x v tcompl(x) = x v R11.
x ^ tcompl(x) = x ^ R00.

tcompl(x) ^ R00 = x ^ R00.         % should be inferred from above definitions.

(I've used a new name tcompl to avoid confusion with Vadim's operator. I think it's unnecessary to say tcompl(x) has same heading as x.)

As you are using the same two axioms that I use, then I fail to see any difference.

I'm not saying there is a difference. I am explaining what I'm doing in terms of lattice structures and theory. Merely, I don't know what's the motivation behind what you're doing.

... tuple complement obeys double complement law ...

I'm failing to see how you can make any claims about obeying laws: you've not connected your operations to well-established theory, so we can't get assurance from prior work. Your definitions are in terms of R00 aot, about which you've failed to demonstrate any laws holding.

To think of this geometrically, we have the four 'cardinal points' of a Relational Lattice:

• ...

So we remain with the only persistent problem: how to define R00 uniquely? (We get lattice top and bottom/R01, R10 'for free' as the identity element and absorbing element respectively of lattice meet ^ aka NaturalJoin.)

The other perspective to your geometric picture would be that there is second lattice structure with R11 as top and R00 as bottom.

What lattice theory does that connect to? What insights does it give? How does it help fix R00 in terms of the already well-developed analysis?

There are an almost-infinity of lattice structures over the same set of elements (as we discussed in an earlier thread): we can pick almost any two elements as top, bottom; then all we need is to concoct some operations for lattice meet/join. For R11 as top, lattice meet would be Appendix A's <OR>. I don't like using that because it's domain-dependent. For the dual of that, I have no intuition what it does. Contrast that for R01/DEE as lattice top, lattice meet is NaturalJoin, which is a very familiar and intuitive operation, corresponding to FOPL AND of the characteristic predicate for the relation operands. The dual to NaturalJoin as lattice join is InnerUnion, which is not so intuitive, but at least is not domain-dependent, and can be explained in terms of familiar Projection and Codd's/set-theoretic Union.

I should add that InnerUnion is well-established enough to have been discovered/rediscovered several times: it was spelled UNION in ISBL; it's spelled UNION CORRESPONDING in SQL (not that many vendors support it).