Quote from tobega on May 22, 2021, 5:44 am

Quote from AntC on May 21, 2021, 10:57 pm

Quote from tobega on May 21, 2021, 8:06 pm

 

We start with the lattice with no attributes, say D, with elements DUM and DEE.

To count as a lattice, we need a (partial) ordering. Or (equivalently as it turns out) a pair of operators that operate on any two elements to produce a third (not necessarily distinct), and that are commutative, associative, idempotent, and mutually dual such that they absorb each other. Read the wiki page on Lattice (ordering), it's simple algebra, unlike Galois theory.

You seem to be building a set of elements. Not every set of elements is a lattice. You seem to have an ordering only amongst relations of the same heading. That's not a lattice: you need an (partial) ordering amongst relations of different headings.

OK, right that's not a lattice. Ignore "Galois theory" as well, the only thing I take from there is the concept of "extension" just to see if the breakdown can lead us somewhere interesting.

EDIT: actually D does form a lattice under the operations this thread has been concerned with, inner union and natural join, see below.

Then we extend with an attribute, say A1, to form the lattice D(A₁) with elements DUM(A₁) which is heading A₁ no tuples, and DEE(A₁) which has all possible values of A₁. We can extend more to D(A₁..A_n), giving DUM(A₁..A_n) and DEE(A₁..A_n). An extension can be characterized as DEE(A₁..A_n) join DEE(A_n+1)

How do we generate non-empty relations with less than all possible tuples for that heading? How to prove that subtracting one tuple from DEE(A₁) then subtracting another yields the same relation as subtracting in the reverse ordering? (How to prove that adding tuples to DUM(A1) likewise produces the same yield? How to prove that if you add enough tuples to DUM(A₁) you'll arrive at DEE(A₁)? And inversely subtracting? ) That'll be true if DEE(A₁) is a set, but you haven't given any axioms saying it's a set. Neither have you given axioms saying how the set contents relate to the ordering.

Since we are basically working with relations, I though it was obvious that A₁..A_n formed a heading, i.e. is a set of attributes. I know you want to ignore attributes, maybe we can get there. Equally obvious should be that DEE(A₁..A_n) must be the set of all possible tuples for that heading. And D(A₁..A_n) must be the set of all possible subsets of DEE(A₁..A_n). Do we need to generate them or can we take them as existing?

For any relation in D(A₁..A_n), any DEE(B₁..B_k) where B₁..B_k is a subset of A₁..A_n works as identity for join, and any DUM(C₁..C_m) where C₁..C_m is a superset of A₁..A_n works as an identity for inner union.

I don't understand "works as an identity for ...". The consequence of the lattice structure, and characteristics of the lattice operators, is there is exactly one identity element. It must work as identity for NatJoin to any element of any heading.

Well, yes and no. Any possible heading in the lattice. For any choice of minimal B₁..B_k and maximal C₁..C_m you can form a lattice between them. But I suppose the concept of "lattice" itself is not really important either unless it gives us something. Let's just work with a family of sets for now.

For a fixed set of attributes A₁..A_n, all possible subsets of DEE(A₁..A_n) form a set of relations with that heading. Your objections are making it obvious that while the union operator does something, there is no inverse to it and the join operator is patently useless. So we need a more fundamental operator in this direction, I think "minus" should work well, but that remains to be proven.

All the different DEEs form a set, where join can compose them, but again that is inadequate. I was thinking of using some definition of "project", but perhaps "remove" is better.

So if we take all possible relations between DUM and Fullest as given, we define DUM and Fullest, and also "minus" such that for X minus Y, all tuples in X that either are a subset or a superset of a tuple in Y are removed from X with those remaining being the result, and "remove" such that for X remove Y, all attributes common to X and Y are removed from X to give the result.

Could all those be sensibly defined and is that enough?

EDIT: All we need is really Fullest, minus and remove.

DEE = Fullest remove Fullest

Dumpty = Fullest minus Fullest

DUM = DEE minus DEE = Dumpty remove Dumpty

Don't know if that gets us anywhere, but it gives the thought that DUM and DEE could be functions (emptify and fullify). It seems be enough to have just DUM and the biggest possible DEE, call it F (I was going to call it DOLLY but that's probably not PC), the others are easily derived from them and the relation we are looking at.

To repeat for the umpteenth time: there is no problem with DEE, it's easy to define, and define uniquely. The 'biggest possible' relation -- that is, with all possible attributes and all possible tuples for those attributes (let's call it Fullest) is emphatically not DEE -- because DEE is greater than Fullest in the lattice ordering, because Fullest is not identity for NatJoin for all possible relations/all headings.

Yes, but defining DEE does not seem to be getting you anywhere. If you start with DUM and Fullest, DEE is simply the inner union of them, just as Dumpty is simply the join of them.

Quote from AntC on May 22, 2021, 9:19 am

Quote from tobega on May 22, 2021, 5:44 am

Quote from AntC on May 21, 2021, 10:57 pm

Quote from tobega on May 21, 2021, 8:06 pm

 

We start with the lattice with no attributes, say D, with elements DUM and DEE.

To count as a lattice, we need a (partial) ordering. Or (equivalently as it turns out) a pair of operators that operate on any two elements to produce a third (not necessarily distinct), and that are commutative, associative, idempotent, and mutually dual such that they absorb each other. Read the wiki page on Lattice (ordering), it's simple algebra, unlike Galois theory.

 

Then we extend with an attribute, say A1, to form the lattice D(A₁) with elements DUM(A₁) which is heading A₁ no tuples, and DEE(A₁) which has all possible values of A₁. We can extend more to D(A₁..A_n), giving DUM(A₁..A_n) and DEE(A₁..A_n). An extension can be characterized as DEE(A₁..A_n) join DEE(A_n+1)

How do we generate non-empty relations with less than all possible tuples for that heading? How to prove that subtracting one tuple from DEE(A₁) then subtracting another yields the same relation as subtracting in the reverse ordering? (How to prove that adding tuples to DUM(A1) likewise produces the same yield? How to prove that if you add enough tuples to DUM(A₁) you'll arrive at DEE(A₁)? And inversely subtracting? ) That'll be true if DEE(A₁) is a set, but you haven't given any axioms saying it's a set. Neither have you given axioms saying how the set contents relate to the ordering.

Since we are basically working with relations, I though it was obvious that A₁..A_n formed a heading, i.e. is a set of attributes. I know you want to ignore attributes, maybe we can get there. Equally obvious should be that DEE(A₁..A_n) must be the set of all possible tuples for that heading. And D(A₁..A_n) must be the set of all possible subsets of DEE(A₁..A_n). Do we need to generate them or can we take them as existing?

All that (allegedly) obvious stuff has to be expressed as axioms, because it's not obvious to a theorem prover. You can express the axioms in set theory, but beware relations are a very specific structure of sets (and sets of sets of pairs, etc). I've no idea how to axiomatise the setbuilder specifications in Appendix A. Hence no idea how to go about defining 'what is a relation' in such a way to express operations. Yes we can take them as existing as 'black boxes' with invisible internal structure -- which is what I'm doing -- but then your "obvious" stuff is not visible.

For any relation in D(A₁..A_n), any DEE(B₁..B_k) where B₁..B_k is a subset of A₁..A_n works as identity for join, and any DUM(C₁..C_m) where C₁..C_m is a superset of A₁..A_n works as an identity for inner union.

I don't understand "works as an identity for ...". The consequence of the lattice structure, and characteristics of the lattice operators, is there is exactly one identity element. It must work as identity for NatJoin to any element of any heading.

Well, yes and no. Any possible heading in the lattice. For any choice of minimal B₁..B_k and maximal C₁..C_m you can form a lattice between them. But I suppose the concept of "lattice" itself is not really important either unless it gives us something. Let's just work with a family of sets for now.

For a fixed set of attributes A₁..A_n, all possible subsets of DEE(A₁..A_n) form a set of relations with that heading. Your objections are making it obvious that while the union operator does something, there is no inverse to it and the join operator is patently useless. So we need a more fundamental operator in this direction, I think "minus" should work well, but that remains to be proven.

All the different DEEs form a set, where join can compose them, but again that is inadequate. I was thinking of using some definition of "project", but perhaps "remove" is better.

So if we take all possible relations between DUM and Fullest as given, we define DUM and Fullest,

There is a possible lattice over all relations with DUM as top, the Fullest becomes bottom. Lattice meet is Appendix A's <OR>, q.v. Vadim has explored it a little.

A latticist would object there's no clear dual operation. A relationalist would object there's no way to define NatJoin (or indeed DEE). An algebraist would object it's domain-dependent -- that is, the result of <OR> depends not only on the 'visible' content of its relation operands, but also on the content of the attribute types' sets of values.

and also "minus" such that for X minus Y, all tuples in X that either are a subset or a superset of a tuple in Y are removed from X with those remaining being the result, and "remove" such that for X remove Y, all attributes common to X and Y are removed from X to give the result.

Could all those be sensibly defined and is that enough?

Without NatJoin you can't express Intersection, WHERE, Extension, nor Matching, NotMatching I suspect. (Nor Cartesian product, but perhaps that's less critical.) So no that's not enough.

Don't know if that gets us anywhere, but it gives the thought that DUM and DEE could be functions (emptify and fullify). It seems be enough to have just DUM and the biggest possible DEE, call it F (I was going to call it DOLLY but that's probably not PC), the others are easily derived from them and the relation we are looking at.

To repeat for the umpteenth time: there is no problem with DEE, it's easy to define, and define uniquely. The 'biggest possible' relation -- that is, with all possible attributes and all possible tuples for those attributes (let's call it Fullest) is emphatically not DEE -- because DEE is greater than Fullest in the lattice ordering, because Fullest is not identity for NatJoin for all possible relations/all headings.

Yes, but defining DEE does not seem to be getting you anywhere. If you start with DUM and Fullest, DEE is simply the inner union of them, just as Dumpty is simply the join of them.

All you've done is turned the problem orthogonal: You can't define NatJoin, so you can't define InnerUnion, so there's no "simply" getting DEE, Dumpty.

Quote from tobega on May 22, 2021, 3:11 pm

Quote from AntC on May 22, 2021, 9:19 am

Quote from tobega on May 22, 2021, 5:44 am

Quote from AntC on May 21, 2021, 10:57 pm

Quote from tobega on May 21, 2021, 8:06 pm

 

We start with the lattice with no attributes, say D, with elements DUM and DEE.

To count as a lattice, we need a (partial) ordering. Or (equivalently as it turns out) a pair of operators that operate on any two elements to produce a third (not necessarily distinct), and that are commutative, associative, idempotent, and mutually dual such that they absorb each other. Read the wiki page on Lattice (ordering), it's simple algebra, unlike Galois theory.

 

Then we extend with an attribute, say A1, to form the lattice D(A₁) with elements DUM(A₁) which is heading A₁ no tuples, and DEE(A₁) which has all possible values of A₁. We can extend more to D(A₁..A_n), giving DUM(A₁..A_n) and DEE(A₁..A_n). An extension can be characterized as DEE(A₁..A_n) join DEE(A_n+1)

How do we generate non-empty relations with less than all possible tuples for that heading? How to prove that subtracting one tuple from DEE(A₁) then subtracting another yields the same relation as subtracting in the reverse ordering? (How to prove that adding tuples to DUM(A1) likewise produces the same yield? How to prove that if you add enough tuples to DUM(A₁) you'll arrive at DEE(A₁)? And inversely subtracting? ) That'll be true if DEE(A₁) is a set, but you haven't given any axioms saying it's a set. Neither have you given axioms saying how the set contents relate to the ordering.

Since we are basically working with relations, I though it was obvious that A₁..A_n formed a heading, i.e. is a set of attributes. I know you want to ignore attributes, maybe we can get there. Equally obvious should be that DEE(A₁..A_n) must be the set of all possible tuples for that heading. And D(A₁..A_n) must be the set of all possible subsets of DEE(A₁..A_n). Do we need to generate them or can we take them as existing?

All that (allegedly) obvious stuff has to be expressed as axioms, because it's not obvious to a theorem prover. You can express the axioms in set theory, but beware relations are a very specific structure of sets (and sets of sets of pairs, etc). I've no idea how to axiomatise the setbuilder specifications in Appendix A. Hence no idea how to go about defining 'what is a relation' in such a way to express operations. Yes we can take them as existing as 'black boxes' with invisible internal structure -- which is what I'm doing -- but then your "obvious" stuff is not visible.

For any relation in D(A₁..A_n), any DEE(B₁..B_k) where B₁..B_k is a subset of A₁..A_n works as identity for join, and any DUM(C₁..C_m) where C₁..C_m is a superset of A₁..A_n works as an identity for inner union.

I don't understand "works as an identity for ...". The consequence of the lattice structure, and characteristics of the lattice operators, is there is exactly one identity element. It must work as identity for NatJoin to any element of any heading.

Well, yes and no. Any possible heading in the lattice. For any choice of minimal B₁..B_k and maximal C₁..C_m you can form a lattice between them. But I suppose the concept of "lattice" itself is not really important either unless it gives us something. Let's just work with a family of sets for now.

For a fixed set of attributes A₁..A_n, all possible subsets of DEE(A₁..A_n) form a set of relations with that heading. Your objections are making it obvious that while the union operator does something, there is no inverse to it and the join operator is patently useless. So we need a more fundamental operator in this direction, I think "minus" should work well, but that remains to be proven.

All the different DEEs form a set, where join can compose them, but again that is inadequate. I was thinking of using some definition of "project", but perhaps "remove" is better.

So if we take all possible relations between DUM and Fullest as given, we define DUM and Fullest,

There is a possible lattice over all relations with DUM as top, the Fullest becomes bottom. Lattice meet is Appendix A's <OR>, q.v. Vadim has explored it a little.

A latticist would object there's no clear dual operation. A relationalist would object there's no way to define NatJoin (or indeed DEE). An algebraist would object it's domain-dependent -- that is, the result of <OR> depends not only on the 'visible' content of its relation operands, but also on the content of the attribute types' sets of values.

and also "minus" such that for X minus Y, all tuples in X that either are a subset or a superset of a tuple in Y are removed from X with those remaining being the result, and "remove" such that for X remove Y, all attributes common to X and Y are removed from X to give the result.

Could all those be sensibly defined and is that enough?

Without NatJoin you can't express Intersection, WHERE, Extension, nor Matching, NotMatching I suspect. (Nor Cartesian product, but perhaps that's less critical.) So no that's not enough.

Don't know if that gets us anywhere, but it gives the thought that DUM and DEE could be functions (emptify and fullify). It seems be enough to have just DUM and the biggest possible DEE, call it F (I was going to call it DOLLY but that's probably not PC), the others are easily derived from them and the relation we are looking at.

To repeat for the umpteenth time: there is no problem with DEE, it's easy to define, and define uniquely. The 'biggest possible' relation -- that is, with all possible attributes and all possible tuples for those attributes (let's call it Fullest) is emphatically not DEE -- because DEE is greater than Fullest in the lattice ordering, because Fullest is not identity for NatJoin for all possible relations/all headings.

Yes, but defining DEE does not seem to be getting you anywhere. If you start with DUM and Fullest, DEE is simply the inner union of them, just as Dumpty is simply the join of them.

All you've done is turned the problem orthogonal: You can't define NatJoin, so you can't define InnerUnion, so there's no "simply" getting DEE, Dumpty.

We want to define A NatJoin B:

let F = Fullest remove (Fullest remove A remove B)

F is now the all the possible tuples of the union of the attributes of A and B

A natJoin B = F minus (F minus A) minus (F minus B)

And A InnerUnion B:

let G = Fullest minus (Fullest minus A minus B)

A InnerUnion B = G remove (G remove A) remove (G remove B)

Also, DEE and Dumpty can be gotten directly from Fullest, minus and remove:

DEE = Fullest remove Fullest

Dumpty = Fullest minus Fullest

DUM = Dumpty remove Dumpty = DEE minus DEE

Quote from Vadim on May 22, 2021, 7:12 pm

Quote from AntC on May 21, 2021, 11:37 pm

Correction: there is a relation like that subset, subset -- it's the empty relation with heading {p}. But that's lattice bottom Dumpty aka R10. It can't be DUM because it's not immediately adjacent to DEE.

The "immediate adjacency" is not algebraic property. It fails in this example with 4 unary relations, and it fails in many other universes.

But I suspect my definitions would work 'fine' (as well/badly as I'm currently experiencing) by interpreting DUM = X. But equally well/badly by interpreting DUM = Y. The choice is arbitrary -- which is the problem.

I don't see any arbitrarines. We have

[latex] X = \langle \{ p \}, \{ \langle 0 \rangle \}\rangle [/latex],

[latex] Y = \langle \{ p \}, \{ \langle 1 \rangle \}\rangle [/latex],

[latex] X \wedge Y  = R_{10} [/latex]  (lattice bottom),

[latex] X \vee Y = R_{01} [/latex]  (lattice top).

Sure. That's what I said. Where is DUM? That was the difficulty/the arbitrary choice.

Then, we have the operation of tuple set complement. I'd prefer to use the quote symbol notation as a postfix operation,

Don't. It's unreadable -- especially when you also use a tick for <INVERSE>. Please go to the bother on this forum (as I do) of using TTM/Tutorial D style operators.

It's compact. The axiom system that I have exibited would be awfully verbose otherwise. Yes, the quotation mark symbols are not perfect choice for this purpose, but we are limited to what Prover9 accepts. It would have been nice to have rich set of UNICODE symbols allowed, but they are no go.

(In the relational lattice the analog of boolean negation is the composition of the attribute set complement (AKA inversion) and tuple set complement).

I think that's wrong: a boolean negation of the proposition for which some relation is the extension must have an extension whose heading is the same. IOW (if I'm following you), it's the tuple set complement only. See Appendix A FORMAL DEFINITIONS for <NOT>.

The calculation of the tuple set complement of the each unverse inhabitant is straightforward:

If it's straightforward, why have you got it wrong below? Or perhaps I don't understand which operator you mean by the tick. Please don't use ticks, use words. and please give Appendix A-style definitions of what your operators do.

[latex] X ' = \langle \{ p \}, \{ \langle 0 \rangle \}\rangle ' = \langle \{ p \}, \{ \langle 1 \rangle \}\rangle = Y [/latex]

[latex] Y ' = X [/latex]

Fine. So which is DUM? Seeing as these are the only two relations adjacent to DEE.

[latex] R_{01} ' = R_{10} [/latex]

Wrong. The tuple inverse of DEE aka R01 is DUM. R10 aka Dumpty has a different heading, it can't be merely the complement of tuples with that heading.

What is [latex] R_{01} [/latex] in that universe? The lattice top -- the unary relation with the two tuples. What its tuple complement? The unary empty relation, which is the lattice bottom.

Yes, this is very counterintutive, because

R01'` = R10

is a theorem in RL. Therefore, the only way to consolidate both equalities is to stipulate that in this universe of 4 unary relations, the attribute inverse is an operator which doesn't flip the attribute set, in particular it's the identity on R10! (It doesn't have to be the identity on X  and Y though.)

Keep in mind that the confusion is primarily due to the absence of the two zilliary relations. Add them to the universe, and everything is intuitive again.

If this is you problem with "wobbling" [latex] R_{00} [/latex], then I sympathize, because adding the 2 zilliary relations. moves the constants  [latex] R_{00}, R_{01} [/latex] (while [latex] R_{10}, R_{11} [/latex] stay the same).

Then, by definition

[latex] R_{00} = R_{10}' [/latex]

This fixes [latex] R_{00}  [/latex] uniquely in our universe as [latex] \langle \{ p \}, \emptyset \rangle [/latex]

That's also wrong, (or perhaps I mean it's right, but it disagrees with the above). Above has <NOT> R10 = R01. But whatever you're doing, you can't say that fixes anything "uniquely" without a proof. And you haven't mentioned how the lattice operations correspond to these operators. I did try to prove uniqueness of what I thought your operators were. It failed.

Again, I somewhat follow your desire for fixed operations, but this property doesn't seem to be algebraic.

This DUM as lattice bottom only works because all elements of the lattice have the same heading. As soon as we include relations with a different heading, this DUM stops acting as it should in definitions for difference-like operations such as NotMatching. So my definition for DUM must be that it has strictly fewer attributes in its heading than any other relation (except DEE); and the corollary is that (once we've included DUM in the set) DEE must have same heading as DUM, as well as being lattice top.

If we include binary relations with the heading [latex] \{ p,q \}  [/latex], the [latex] R_{00} [/latex] and  [latex] R_{01} [/latex] would still be those unary relations, and [latex] R_{01} [/latex] still wont be covering (in partial order sense)  [latex] R_{00} [/latex].

• You can define <INVERSE> (<INVERSE> r) = r; <NOT> (<NOT> r) = r. I think that won't fix either operation to what you want. For example, those are 'solved' if <INVERSE>, <NOT> are merely identity. I've added stupid/ugly axioms like emptify(DEE) ≠ DEE; DUM must be adjacent to DEE. That's not enough to fix anything. (So in your 4-element model, it merely fixes that R00 is the element 'opposite' R11 -- either could be X, Y, the choice is arbitrary.)

Unlike tuple set complement honoring the law of double negation

x'' = x

So you're using apostrophe for tuple set complement. Then it can't be producing a result with a different heading to its argument. So you are wrong above.

?

the law for repetitive attribute inversion is more subtle:

x``` = x`

So (as I guessed) attribute inversion gives absolute complement of the heading, with all possible tuples in the body? Is it so hard to say that?

Yes, if the relation is not empty. If it is empty than the result is the empty relation.

 

Returning to the major theme of this thread, I guess you want an algebra with all domain&attribute independent operators. I'd suggest the following binary analogs of tuple and attribute complement:

x <REMOVE> y = x v y`.
x <NotMatching> y = x ^ y'.

 

 

Quote from AntC on May 23, 2021, 12:15 am

Quote from tobega on May 22, 2021, 3:11 pm

Quote from AntC on May 22, 2021, 9:19 am

Quote from tobega on May 22, 2021, 5:44 am

 

All that (allegedly) obvious stuff has to be expressed as axioms, because it's not obvious to a theorem prover. You can express the axioms in set theory, but beware relations are a very specific structure of sets (and sets of sets of pairs, etc). I've no idea how to axiomatise the setbuilder specifications in Appendix A. Hence no idea how to go about defining 'what is a relation' in such a way to express operations. Yes we can take them as existing as 'black boxes' with invisible internal structure -- which is what I'm doing -- but then your "obvious" stuff is not visible.

 

 

So if we take all possible relations between DUM and Fullest as given, we define DUM and Fullest,

There is a possible lattice over all relations with DUM as top, the Fullest becomes bottom. Lattice meet is Appendix A's <OR>, q.v. Vadim has explored it a little.

A latticist would object there's no clear dual operation. A relationalist would object there's no way to define NatJoin (or indeed DEE). An algebraist would object it's domain-dependent -- that is, the result of <OR> depends not only on the 'visible' content of its relation operands, but also on the content of the attribute types' sets of values.

and also "minus" such that for X minus Y, all tuples in X that either are a subset or a superset of a tuple in Y are removed from X with those remaining being the result, and "remove" such that for X remove Y, all attributes common to X and Y are removed from X to give the result.

Could all those be sensibly defined and is that enough?

Without NatJoin you can't express Intersection, WHERE, Extension, nor Matching, NotMatching I suspect. (Nor Cartesian product, but perhaps that's less critical.) So no that's not enough.

 

Yes, but defining DEE does not seem to be getting you anywhere. If you start with DUM and Fullest, DEE is simply the inner union of them, just as Dumpty is simply the join of them.

All you've done is turned the problem orthogonal: You can't define NatJoin, so you can't define InnerUnion, so there's no "simply" getting DEE, Dumpty.

We want to define A NatJoin B:

let F = Fullest remove (Fullest remove A remove B)

Where did you define remove? How does it behave relative to <OR> -- which is what you fixed to determine Fullest.

F is now the all the possible tuples of the union of the attributes of A and B

A natJoin B = F minus (F minus A) minus (F minus B)

Where did you define minus?

And A InnerUnion B:

let G = Fullest minus (Fullest minus A minus B)

A InnerUnion B = G remove (G remove A) remove (G remove B)

Also, DEE and Dumpty can be gotten directly from Fullest, minus and remove:

DEE = Fullest remove Fullest

Dumpty = Fullest minus Fullest

DUM = Dumpty remove Dumpty = DEE minus DEE

If you're just going to presume operations like remove, minus, you might as well presume NatJoin, InnerUnion. We can presume Fullest is somewhere in the givens, just as are DEE, DUM, Dumpty. But we need a way to identify them uniquely.

Quote from AntC on May 23, 2021, 12:17 am

Quote from Vadim on May 22, 2021, 7:12 pm

Quote from AntC on May 21, 2021, 11:37 pm

Correction: there is a relation like that subset, subset -- it's the empty relation with heading {p}. But that's lattice bottom Dumpty aka R10. It can't be DUM because it's not immediately adjacent to DEE.

The "immediate adjacency" is not algebraic property. It fails in this example with 4 unary relations, and it fails in many other universes.

• adj(r1, r2) ≡ (r1 >= r2 & r1 ≠ r2 & (∀ s (between(r1, s, r2) ≡ r1 = s | s = r2))). immediately adjacent below

See the new thread I started. In which I consider possible 'universes'.

If you're going to continue to post unreadable code with unexplained operations, and no proven claims of uniqueness, I'm not going to bother responding.

 

Quote from Vadim on May 23, 2021, 12:39 am

Quote from tobega on May 21, 2021, 8:06 pm

Quote from tobega on May 21, 2021, 8:06 pm

I'll take the liberty to waffle on with some further thoughts from my limited understanding.

I'm still thinking of some kind of analogy to field extensions in Galois theory (which I don't really pretend to understand despite passing a class in it long ago), so I'll play with that:

We start with the lattice with no attributes, say D, with elements DUM and DEE. Then we extend with an attribute, say A1, to form the lattice D(A₁) with elements DUM(A₁) which is heading A₁ no tuples, and DEE(A₁) which has all possible values of A₁. We can extend more to D(A₁..A_n), giving DUM(A₁..A_n) and DEE(A₁..A_n). An extension can be characterized as DEE(A₁..A_n) join DEE(A_n+1)

For any relation in D(A₁..A_n), any DEE(B₁..B_k) where B₁..B_k is a subset of A₁..A_n works as identity for join, and any DUM(C₁..C_m) where C₁..C_m is a superset of A₁..A_n works as an identity for inner union.

Don't know if that gets us anywhere, but it gives the thought that DUM and DEE could be functions (emptify and fullify). It seems be enough to have just DUM and the biggest possible DEE, call it F (I was going to call it DOLLY but that's probably not PC), the others are easily derived from them and the relation we are looking at.

RL borrows many ideas from Boolean Algebra. From the BA prespective, are there any field extensions to follow as a prototype? Well, BA is not a field, but ring; is there such a thing as ring extension? (I simply don't know). For example, can natural numbers be thought as a BA ring extension? There is actually an ambiguity which BA I have in mind, is it primitive 2-element one, or the (categorical) product of primitive ones...

BTW, here is a (failed) attempt similar to your suggestion in the area of Calculus.

 

Quote from dandl on May 23, 2021, 2:03 am

Anyone care to give a summary of what if any progress is being made?

Where do you expect to get to?

How will you know if you get there?

Quote from AntC on May 23, 2021, 4:03 am

Quote from Vadim on May 22, 2021, 7:12 pm

Quote from AntC on May 21, 2021, 11:37 pm

 

Yes, this is very counterintutive, because

R01'` = R10

is a theorem in RL. Therefore, the only way to consolidate both equalities is to stipulate that in this universe of 4 unary relations, the attribute inverse is an operator which doesn't flip the attribute set, in particular it's the identity on R10! (It doesn't have to be the identity on X  and Y though.)

Keep in mind that the confusion is primarily due to the absence of the two zilliary relations. Add them to the universe, and everything is intuitive again.

If this is you problem with "wobbling" [latex] R_{00} [/latex], then I sympathize, because adding the 2 zilliary relations. moves the constants  [latex] R_{00}, R_{01} [/latex] (while [latex] R_{10}, R_{11} [/latex] stay the same).

Then, by definition

[latex] R_{00} = R_{10}' [/latex]

This fixes [latex] R_{00}  [/latex] uniquely in our universe as [latex] \langle \{ p \}, \emptyset \rangle [/latex]

That's also wrong, (or perhaps I mean it's right, but it disagrees with the above). Above has <NOT> R10 = R01. But whatever you're doing, you can't say that fixes anything "uniquely" without a proof. And you haven't mentioned how the lattice operations correspond to these operators. I did try to prove uniqueness of what I thought your operators were. It failed.

Again, I somewhat follow your desire for fixed operations, but this property doesn't seem to be algebraic.

This DUM as lattice bottom only works because all elements of the lattice have the same heading. As soon as we include relations with a different heading, this DUM stops acting as it should in definitions for difference-like operations such as NotMatching. So my definition for DUM must be that it has strictly fewer attributes in its heading than any other relation (except DEE); and the corollary is that (once we've included DUM in the set) DEE must have same heading as DUM, as well as being lattice top.

If we include binary relations with the heading [latex] \{ p,q \}  [/latex], the [latex] R_{00} [/latex] and  [latex] R_{01} [/latex] would still be those unary relations, and [latex] R_{01} [/latex] still wont be covering (in partial order sense)  [latex] R_{00} [/latex].

• You can define <INVERSE> (<INVERSE> r) = r; <NOT> (<NOT> r) = r. I think that won't fix either operation to what you want. For example, those are 'solved' if <INVERSE>, <NOT> are merely identity. I've added stupid/ugly axioms like emptify(DEE) ≠ DEE; DUM must be adjacent to DEE. That's not enough to fix anything. (So in your 4-element model, it merely fixes that R00 is the element 'opposite' R11 -- either could be X, Y, the choice is arbitrary.)

Unlike tuple set complement honoring the law of double negation

x'' = x

So you're using apostrophe for tuple set complement. Then it can't be producing a result with a different heading to its argument. So you are wrong above.

?

the law for repetitive attribute inversion is more subtle:

x``` = x`

So (as I guessed) attribute inversion gives absolute complement of the heading, with all possible tuples in the body? Is it so hard to say that?

Yes, if the relation is not empty. If it is empty than the result is the empty relation.

You need to explain this operator very carefully. All I've got is a few stray remarks. Its behaviour seems to be nonsense. From your set of axioms:

• 20. R00 = ((x' ^ x)` ^ x)`. R00  is your name for DUM. The operator with largest scope there is trailing backtick. So it must return an empty relation(?)
• 24. R11 = (x' v x`)`.  R11 is your name for what we've called Fullest -- the relation with heading all possible attributes, body all possible tuples. The operator with largest scope there is also trailing backtick. So it must return a full-as-possible relation(?) -- that is, it's domain-dependent(?)

I find domain-dependent operators very difficult to work with/my intuitions are often confounded. I find InnerUnion a little better, but I still have to be careful. An operator that's sometimes domain-dependent, sometimes not seems to me to be asking for trouble.

However it behaves, I still haven't seen any claim it's uniquely defined by your axioms -- that is, fixed wrt NatJoin.

BTW when I copy/pasted those axioms, the trailing backtick on one of them got lost, although the trailing dot didn't. Just don't use almost-invisible characters; don't use postfix operators; don't use almost-indistinguishable single characters as operators. There's no need in Prover9 to use operators like that: create a named function, like emptify( ), project( , ), Remove( , ).)

Do find a meaningful name for this weird thing; then use that name in expressions you present here (either infix or as a prefix function). Or are you deliberately trying to make this obtuse? Avoid explaining yourself at all costs?