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

Quote from AntC on May 21, 2021, 11:37 pmQuote from Vadim on May 21, 2021, 2:45 pmQuote from AntC on May 21, 2021, 12:44 amQuote from Vadim on May 20, 2021, 3:08 pmQuote from AntC on May 20, 2021, 8:00 am

There's a counter-example with just 4 elements: suppose in this Universe there's only one attribute, and its type has only value, then there's a single relation with non-empty heading (degree 1) and non-empty body (cardinality 1), call it

`R11`

; the 4 elements`DEE, DUM, Dumpty, R11`

. The axioms and operators all work if we take`R11`

as a false`DUM`

, and leave the true`DUM`

as just some other element.Another example: take the universe inhabited by 4 unary relations [latex] X = \langle \{ p \}, \{ \langle 0 \rangle \}\rangle [/latex], [latex] Y = \langle \{ p \}, \{ \langle 1 \rangle \}\rangle [/latex], [latex] X \wedge Y [/latex], [latex] X \vee Y [/latex]. Some may argue that there are "genuine" DUM and DEE hidden somewhere in that universe, but I'd think their roles can perfectly be played by unary relations, so that those 4 relations is all that you will ever see.

Some mistakes in my post, corrected in line here (also corrected in the original)

There is a

`DEE`

-- that is, a relation whose heading is a subset of every other relation (not necessarily proper), and content a~~subset~~superset of every other relation projected on that heading. That is`X ^ Y`

.There isn't a

`DUM`

-- that is a relation whose headings is the subset of every other relation, and content a subset of every other relation projected on that heading. (Neither`X`

's nor`Y`

's body are a subset of the other.)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`

.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 usingTTM/Tutorial Dstyle operators.rather than TTM prefix

`<NOT>`

, because the later can be easily confused with boolean algebra negation."easily confused" is what your ticks are.

`<NOT>`

with the angle brackets is not confusing: it's clearly an Appendix A operator.(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.[latex] R_{10} ' = R_{01} [/latex]

Wrong. Again those have different headings.

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

- 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?

This makes attribute inversion less intutive compared to tuple set complement.

An operator without a definition/explanation is not intuitive. That's not the operator's fault.

Quote from Vadim on May 21, 2021, 2:45 pmQuote from AntC on May 21, 2021, 12:44 amQuote from Vadim on May 20, 2021, 3:08 pmQuote from AntC on May 20, 2021, 8:00 am

There's a counter-example with just 4 elements: suppose in this Universe there's only one attribute, and its type has only value, then there's a single relation with non-empty heading (degree 1) and non-empty body (cardinality 1), call it

`R11`

; the 4 elements`DEE, DUM, Dumpty, R11`

. The axioms and operators all work if we take`R11`

as a false`DUM`

, and leave the true`DUM`

as just some other element.Another example: take the universe inhabited by 4 unary relations X = \langle \{ p \}, \{ \langle 0 \rangle \}\rangle , Y = \langle \{ p \}, \{ \langle 1 \rangle \}\rangle , X \wedge Y , X \vee Y . Some may argue that there are "genuine" DUM and DEE hidden somewhere in that universe, but I'd think their roles can perfectly be played by unary relations, so that those 4 relations is all that you will ever see.

Some mistakes in my post, corrected in line here (also corrected in the original)

There is a

`DEE`

-- that is, a relation whose heading is a subset of every other relation (not necessarily proper), and content a~~subset~~superset of every other relation projected on that heading. That is`X ^ Y`

.There isn't a

`DUM`

-- that is a relation whose headings is the subset of every other relation, and content a subset of every other relation projected on that heading. (Neither`X`

's nor`Y`

's body are a subset of the other.)

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`

.

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

X = \langle \{ p \}, \{ \langle 0 \rangle \}\rangle ,

Y = \langle \{ p \}, \{ \langle 1 \rangle \}\rangle ,

X \wedge Y = R_{10} (lattice bottom),

X \vee Y = R_{01} (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.

rather than TTM prefix

`<NOT>`

, because the later can be easily confused with boolean algebra negation.

"easily confused" is what your ticks are. `<NOT>`

with the angle brackets is not confusing: it's clearly an Appendix A operator.

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

X ' = \langle \{ p \}, \{ \langle 0 \rangle \}\rangle ' = \langle \{ p \}, \{ \langle 1 \rangle \}\rangle = Y

Y ' = X

Fine. So which is `DUM`

? Seeing as these are the only two relations adjacent to `DEE`

.

R_{01} ' = R_{10}

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.

R_{10} ' = R_{01}

Wrong. Again those have different headings.

Then, by definition

R_{00} = R_{10}'

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

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.

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.

- 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?

This makes attribute inversion less intutive compared to tuple set complement.

An operator without a definition/explanation is not intuitive. That's not the operator's fault.

Quote from tobega on May 22, 2021, 5:44 amQuote from AntC on May 21, 2021, 10:57 pmQuote 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

_{1}) with elements DUM(A_{1}) which is heading A_{1}no tuples, and DEE(A_{1}) which has all possible values of A_{1}. We can extend more to D(A_{1}..A_{n}), giving DUM(A_{1}..A_{n}) and DEE(A_{1}..A_{n}). An extension can be characterized as DEE(A_{1}..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

_{1}) 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_{1}) you'll arrive at DEE(A_{1})? And inversely subtracting? ) That'll be true if DEE(A_{1}) 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

_{1}..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_{1}..A_{n}) must be the set of all possible tuples for that heading. And D(A_{1}..A_{n}) must be the set of all possible subsets of DEE(A_{1}..A_{n}). Do we need to generate them or can we take them as existing?For any relation in D(A

_{1}..A_{n}), any DEE(B_{1}..B_{k}) where B_{1}..B_{k}is a subset of A_{1}..A_{n}works as identity for join, and any DUM(C_{1}..C_{m}) where C_{1}..C_{m}is a superset of A_{1}..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

_{1}..B_{k}and maximal C_{1}..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

_{1}..A_{n}, all possible subsets of DEE(A_{1}..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 21, 2021, 10:57 pmQuote 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

_{1}) with elements DUM(A_{1}) which is heading A_{1}no tuples, and DEE(A_{1}) which has all possible values of A_{1}. We can extend more to D(A_{1}..A_{n}), giving DUM(A_{1}..A_{n}) and DEE(A_{1}..A_{n}). An extension can be characterized as DEE(A_{1}..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

_{1}) 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_{1}) you'll arrive at DEE(A_{1})? And inversely subtracting? ) That'll be true if DEE(A_{1}) 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_{1}..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_{1}..A_{n}) must be the set of all possible tuples for that heading. And D(A_{1}..A_{n}) must be the set of all possible subsets of DEE(A_{1}..A_{n}). Do we need to generate them or can we take them as existing?

For any relation in D(A

_{1}..A_{n}), any DEE(B_{1}..B_{k}) where B_{1}..B_{k}is a subset of A_{1}..A_{n}works as identity for join, and any DUM(C_{1}..C_{m}) where C_{1}..C_{m}is a superset of A_{1}..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_{1}..B_{k} and maximal C_{1}..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_{1}..A_{n}, all possible subsets of DEE(A_{1}..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 amQuote from tobega on May 22, 2021, 5:44 amQuote from AntC on May 21, 2021, 10:57 pmQuote 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

_{1}) with elements DUM(A_{1}) which is heading A_{1}no tuples, and DEE(A_{1}) which has all possible values of A_{1}. We can extend more to D(A_{1}..A_{n}), giving DUM(A_{1}..A_{n}) and DEE(A_{1}..A_{n}). An extension can be characterized as DEE(A_{1}..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

_{1}) 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_{1}) you'll arrive at DEE(A_{1})? And inversely subtracting? ) That'll be true if DEE(A_{1}) 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

_{1}..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_{1}..A_{n}) must be the set of all possible tuples for that heading. And D(A_{1}..A_{n}) must be the set of all possible subsets of DEE(A_{1}..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

_{1}..A_{n}), any DEE(B_{1}..B_{k}) where B_{1}..B_{k}is a subset of A_{1}..A_{n}works as identity for join, and any DUM(C_{1}..C_{m}) where C_{1}..C_{m}is a superset of A_{1}..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

_{1}..B_{k}and maximal C_{1}..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

_{1}..A_{n}, all possible subsets of DEE(A_{1}..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, 5:44 amQuote from AntC on May 21, 2021, 10:57 pmQuote from tobega on May 21, 2021, 8:06 pm

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

_{1}) with elements DUM(A_{1}) which is heading A_{1}no tuples, and DEE(A_{1}) which has all possible values of A_{1}. We can extend more to D(A_{1}..A_{n}), giving DUM(A_{1}..A_{n}) and DEE(A_{1}..A_{n}). An extension can be characterized as DEE(A_{1}..A_{n}) join DEE(A_{n+1})_{1}) 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_{1}) you'll arrive at DEE(A_{1})? And inversely subtracting? ) That'll be true if DEE(A_{1}) 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._{1}..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_{1}..A_{n}) must be the set of all possible tuples for that heading. And D(A_{1}..A_{n}) must be the set of all possible subsets of DEE(A_{1}..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.

_{1}..A_{n}), any DEE(B_{1}..B_{k}) where B_{1}..B_{k}is a subset of A_{1}..A_{n}works as identity for join, and any DUM(C_{1}..C_{m}) where C_{1}..C_{m}is a superset of A_{1}..A_{n}works as an identity for inner union.`NatJoin`

to any element of any heading._{1}..B_{k}and maximal C_{1}..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._{1}..A_{n}, all possible subsets of DEE(A_{1}..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.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.

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

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 pmQuote from AntC on May 22, 2021, 9:19 amQuote from tobega on May 22, 2021, 5:44 amQuote from AntC on May 21, 2021, 10:57 pmQuote from tobega on May 21, 2021, 8:06 pm

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

_{1}) with elements DUM(A_{1}) which is heading A_{1}no tuples, and DEE(A_{1}) which has all possible values of A_{1}. We can extend more to D(A_{1}..A_{n}), giving DUM(A_{1}..A_{n}) and DEE(A_{1}..A_{n}). An extension can be characterized as DEE(A_{1}..A_{n}) join DEE(A_{n+1})_{1}) 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_{1}) you'll arrive at DEE(A_{1})? And inversely subtracting? ) That'll be true if DEE(A_{1}) 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._{1}..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_{1}..A_{n}) must be the set of all possible tuples for that heading. And D(A_{1}..A_{n}) must be the set of all possible subsets of DEE(A_{1}..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.

_{1}..A_{n}), any DEE(B_{1}..B_{k}) where B_{1}..B_{k}is a subset of A_{1}..A_{n}works as identity for join, and any DUM(C_{1}..C_{m}) where C_{1}..C_{m}is a superset of A_{1}..A_{n}works as an identity for inner union.`NatJoin`

to any element of any heading._{1}..B_{k}and maximal C_{1}..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._{1}..A_{n}, all possible subsets of DEE(A_{1}..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.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.`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.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 AntC on May 22, 2021, 9:19 amQuote from tobega on May 22, 2021, 5:44 amQuote from AntC on May 21, 2021, 10:57 pmQuote from tobega on May 21, 2021, 8:06 pm

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

_{1}) with elements DUM(A_{1}) which is heading A_{1}no tuples, and DEE(A_{1}) which has all possible values of A_{1}. We can extend more to D(A_{1}..A_{n}), giving DUM(A_{1}..A_{n}) and DEE(A_{1}..A_{n}). An extension can be characterized as DEE(A_{1}..A_{n}) join DEE(A_{n+1})_{1}) 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_{1}) you'll arrive at DEE(A_{1})? And inversely subtracting? ) That'll be true if DEE(A_{1}) 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._{1}..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_{1}..A_{n}) must be the set of all possible tuples for that heading. And D(A_{1}..A_{n}) must be the set of all possible subsets of DEE(A_{1}..A_{n}). Do we need to generate them or can we take them as existing?_{1}..A_{n}), any DEE(B_{1}..B_{k}) where B_{1}..B_{k}is a subset of A_{1}..A_{n}works as identity for join, and any DUM(C_{1}..C_{m}) where C_{1}..C_{m}is a superset of A_{1}..A_{n}works as an identity for inner union.`NatJoin`

to any element of any heading._{1}..B_{k}and maximal C_{1}..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._{1}..A_{n}, all possible subsets of DEE(A_{1}..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.So if we take all possible relations between DUM and Fullest as given, we define DUM and Fullest,

`DUM`

as top, the`Fullest`

becomes bottom. Lattice meet is Appendix A's`<OR>`

, q.v. Vadim has explored it a little.`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.Could all those be sensibly defined and is that enough?

`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.`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.`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 pmQuote from AntC on May 21, 2021, 11:37 pmCorrection: 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 usingTTM/Tutorial Dstyle 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 universeof 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 21, 2021, 11:37 pm

`{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.

`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

X = \langle \{ p \}, \{ \langle 0 \rangle \}\rangle ,

Y = \langle \{ p \}, \{ \langle 1 \rangle \}\rangle ,

X \wedge Y = R_{10} (lattice bottom),

X \vee Y = R_{01} (lattice top).

Sure. That's what I said. Where is

`DUM`

? That was the difficulty/the arbitrary choice.`<INVERSE>`

. Please go to the bother on this forum (as I do) of usingTTM/Tutorial Dstyle 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.

`<NOT>`

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

X ' = \langle \{ p \}, \{ \langle 0 \rangle \}\rangle ' = \langle \{ p \}, \{ \langle 1 \rangle \}\rangle = Y

Y ' = X

Fine. So which is

`DUM`

? Seeing as these are the only two relations adjacent to`DEE`

.R_{01} ' = R_{10}

`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 R_{01} 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" R_{00} , then I sympathize, because adding the 2 zilliary relations. moves the constants R_{00}, R_{01} (while R_{10}, R_{11} stay the same).

Then, by definition

R_{00} = R_{10}'

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

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

`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 \{ p,q \} , the R_{00} and R_{01} would still be those unary relations, and R_{01} still wont be covering (in partial order sense) R_{00} .

`<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`

?

the law for repetitive attribute inversion is more subtle:

`x``` = x``

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 amQuote from tobega on May 22, 2021, 3:11 pmQuote from AntC on May 22, 2021, 9:19 amQuote from tobega on May 22, 2021, 5:44 am

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

`DUM`

as top, the`Fullest`

becomes bottom. Lattice meet is Appendix A's`<OR>`

, q.v. Vadim has explored it a little.`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.Could all those be sensibly defined and is that enough?

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

`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 tobega on May 22, 2021, 3:11 pmQuote from AntC on May 22, 2021, 9:19 amQuote from tobega on May 22, 2021, 5:44 am

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

`DUM`

as top, the`Fullest`

becomes bottom. Lattice meet is Appendix A's`<OR>`

, q.v. Vadim has explored it a little.`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.Could all those be sensibly defined and is that enough?

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

`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 amQuote from Vadim on May 22, 2021, 7:12 pmQuote from AntC on May 21, 2021, 11:37 pm`{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 belowSee 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 22, 2021, 7:12 pmQuote from AntC on May 21, 2021, 11:37 pm`{p}`

. But that's lattice bottom`Dumpty`

aka`R10`

. It can't be`DUM`

because it's not immediately adjacent to`DEE`

.

`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 amQuote from tobega on May 21, 2021, 8:06 pmQuote from tobega on May 21, 2021, 8:06 pmI'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

_{1}) with elements DUM(A_{1}) which is heading A_{1}no tuples, and DEE(A_{1}) which has all possible values of A_{1}. We can extend more to D(A_{1}..A_{n}), giving DUM(A_{1}..A_{n}) and DEE(A_{1}..A_{n}). An extension can be characterized as DEE(A_{1}..A_{n}) join DEE(A_{n+1})_{1}..A_{n}), any DEE(B_{1}..B_{k}) where B_{1}..B_{k}is a subset of A_{1}..A_{n}works as identity for join, and any DUM(C_{1}..C_{m}) where C_{1}..C_{m}is a superset of A_{1}..A_{n}works as an identity for inner union.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 tobega on May 21, 2021, 8:06 pm

Quote from tobega on May 21, 2021, 8:06 pmI'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

_{1}) with elements DUM(A_{1}) which is heading A_{1}no tuples, and DEE(A_{1}) which has all possible values of A_{1}. We can extend more to D(A_{1}..A_{n}), giving DUM(A_{1}..A_{n}) and DEE(A_{1}..A_{n}). An extension can be characterized as DEE(A_{1}..A_{n}) join DEE(A_{n+1})_{1}..A_{n}), any DEE(B_{1}..B_{k}) where B_{1}..B_{k}is a subset of A_{1}..A_{n}works as identity for join, and any DUM(C_{1}..C_{m}) where C_{1}..C_{m}is a superset of A_{1}..A_{n}works as an identity for inner union.

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 amAnyone 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?

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 amQuote from Vadim on May 22, 2021, 7:12 pmQuote 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 universeof 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]

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

`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].

`<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`

?

the law for repetitive attribute inversion is more subtle:

`x``` = x``

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?

Quote from Vadim on May 22, 2021, 7:12 pmQuote from AntC on May 21, 2021, 11:37 pm

Yes, this is very counterintutive, because

`R01'` = R10`

in this universeof 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.)If this is you problem with "wobbling" R_{00} , then I sympathize, because adding the 2 zilliary relations. moves the constants R_{00}, R_{01} (while R_{10}, R_{11} stay the same).

Then, by definition

R_{00} = R_{10}'

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

`<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.`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 \{ p,q \} , the R_{00} and R_{01} would still be those unary relations, and R_{01} still wont be covering (in partial order sense) R_{00} .

`<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`

?

the law for repetitive attribute inversion is more subtle:

`x``` = x``

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?