The Third Manifesto ForumDatabases: Database TheoryANNOUNCE: a relational algebra wi …

Please or Register to create posts and topics.

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

#71 · May 24, 2021, 9:21 pm

Quote from AntC on May 24, 2021, 9:21 pm

Quote from tobega on May 24, 2021, 11:52 am

Take relation R that does not contain attribute a. The tuples of R evaluate to TRUE for R's predicate whatever the value of a. Now take relation A whose heading consists only of attribute a and whose body consists of all possible values of a. If we define R´ = R join A, we can conclude that R´ still evaluates the same for R's predicate. By the same token, we can simply remove the attribute a (where every possible value of a occurs with every tuple from R) from R´ and not change anything significant.

This thread has been talking about manipulating values and equivalence of operations doing that. It's assuming the meaning is given elsewhere. Now you've shifted to talking about meanings/predicates. This is again basic stuff that shows you don't understand how the semantics of the relational model works (or rather should work -- SQL doesn't).

I make the claim that the absence of an attribute is equivalent to having the cross-product with every possible value for that attribute.

What do you mean by "equivalent" here? It's not the same value. We don't know if it's the same meaning until we know what query the value results from.

Look at J = R join S. If S contains a, then J = R´ join S as well. If S does not contain a, then J´ = J join A = R´ join S, but since we then just have the cross product with every possible value of a, J and J´ would then be equivalent as well.

Again the resulting values in your two scenarios are different. What do you mean by "equivalent"?

It turns out that R and R´ are interchangeable for inner union as well, if my claim is accepted.

Again the resulting values in your two scenarios are different. What do you mean by "equivalent"/"interchangeable"?

Even more interesting, if we can agree my claim is true (or agree that we don't do anything completely insane by defining it to be true),

I'm tending to 'insane'. You're muddling up values (uninterpreted) with predicates.

then DEE is equivalent to Fullest (i.e. they are different representations of the same element), which makes sense, because they both say "the predicate is true whatever the value of any attribute". (Also equivalent to any DEE(A₁..A_n) as I described them previously)

By a similar reasoning, DUM is equivalent to Dumpty, i.e. "nothing is true whatever attributes we look at". In that case, no need to search for DUM, we already have it represented as Dumpty.

Quote from tobega on May 24, 2021, 11:52 am

Take relation R that does not contain attribute a. The tuples of R evaluate to TRUE for R's predicate whatever the value of a. Now take relation A whose heading consists only of attribute a and whose body consists of all possible values of a. If we define R´ = R join A, we can conclude that R´ still evaluates the same for R's predicate. By the same token, we can simply remove the attribute a (where every possible value of a occurs with every tuple from R) from R´ and not change anything significant.

This thread has been talking about manipulating values and equivalence of operations doing that. It's assuming the meaning is given elsewhere. Now you've shifted to talking about meanings/predicates. This is again basic stuff that shows you don't understand how the semantics of the relational model works (or rather should work -- SQL doesn't).

I make the claim that the absence of an attribute is equivalent to having the cross-product with every possible value for that attribute.

What do you mean by "equivalent" here? It's not the same value. We don't know if it's the same meaning until we know what query the value results from.

Look at J = R join S. If S contains a, then J = R´ join S as well. If S does not contain a, then J´ = J join A = R´ join S, but since we then just have the cross product with every possible value of a, J and J´ would then be equivalent as well.

Again the resulting values in your two scenarios are different. What do you mean by "equivalent"?

It turns out that R and R´ are interchangeable for inner union as well, if my claim is accepted.

Again the resulting values in your two scenarios are different. What do you mean by "equivalent"/"interchangeable"?

Even more interesting, if we can agree my claim is true (or agree that we don't do anything completely insane by defining it to be true),

I'm tending to 'insane'. You're muddling up values (uninterpreted) with predicates.

then DEE is equivalent to Fullest (i.e. they are different representations of the same element), which makes sense, because they both say "the predicate is true whatever the value of any attribute". (Also equivalent to any DEE(A₁..A_n) as I described them previously)

By a similar reasoning, DUM is equivalent to Dumpty, i.e. "nothing is true whatever attributes we look at". In that case, no need to search for DUM, we already have it represented as Dumpty.

#72 · May 25, 2021, 12:42 am

Quote from AntC on May 25, 2021, 12:42 am

Quote from tobega on May 24, 2021, 11:52 am

The interesting thing is then being able to prove that two different sequences of operations have the same effects, at least as far as the model goes (there might be some aspect we haven't managed to capture, but hopefully not), and this can be used e.g. as a (possibly partial) proof that a query rewrite is correct.

... In my recent explorations in this thread I glimpsed an interesting rabbit-hole:

Take relation R that does not contain attribute a. The tuples of R evaluate to TRUE for R's predicate whatever the value of a. Now take relation A whose heading consists only of attribute a and whose body consists of all possible values of a. If we define R´ = R join A, we can conclude that R´ still evaluates the same for R's predicate. By the same token, we can simply remove the attribute a (where every possible value of a occurs with every tuple from R) from R´ and not change anything significant.

I make the claim that the absence of an attribute is equivalent to having the cross-product with every possible value for that attribute.

Look at J = R join S. If S contains a, ...

Then there are legitimate values for S that contain all possible a-values. How do we distinguish that from a value for S (or R) that contain all a-values gratuitously? I suppose we need to hold a heading against each value that is potentially different from the gratuitous attributes that appear in its (alleged) body; and manipulate the genuine heading to establish whether two queries are equivalent (produce the same answers for each possible value of the database). Then ...

... By a similar reasoning, DUM is equivalent to Dumpty, i.e. "nothing is true whatever attributes we look at". In that case, no need to search for DUM, we already have it represented as Dumpty.

The critical features of DUM are that not only is it empty, but also it has no attributes. To get the heading of r: r NatJoin DUM whereas r NatJoin Dumpty = Dumpty for all r. So now I can't tell whether two relations have the same heading -- by which I mean genuine heading, not gratuitously-full heading. I've tried to define emptify( r ), but all definitions turn out to be equivalent to requiring DUM.

Similarly if I want to find out if (or stipulate that) two relations have no attributes in common: (r NatJoin DUM) InnerUnion (s NatJoin DUM) = DUM. That holds because DUM has no attributes. I can't use DEE in the role of empty-heading tester (supposing DEE hasn't got all those gratuitous attributes), because r, s might be both empty, then their InnerUnion won't be DEE. And let me cut off more nonsense: r InnerUnion DEE = DEE for all r, so we can't use DEE in the role of DUM somehow. We could go by (r InnerUnion Fullest) InnerUnion (s InnerUnion Fullest) = DEE to distinguish non-overlapping headings; you've just turned the problem outside-in: how to define Fullest and distinguish it from DEE? Your post just magically waved Fullest into existence.

Quote from tobega on May 24, 2021, 11:52 am

The interesting thing is then being able to prove that two different sequences of operations have the same effects, at least as far as the model goes (there might be some aspect we haven't managed to capture, but hopefully not), and this can be used e.g. as a (possibly partial) proof that a query rewrite is correct.

... In my recent explorations in this thread I glimpsed an interesting rabbit-hole:

Take relation R that does not contain attribute a. The tuples of R evaluate to TRUE for R's predicate whatever the value of a. Now take relation A whose heading consists only of attribute a and whose body consists of all possible values of a. If we define R´ = R join A, we can conclude that R´ still evaluates the same for R's predicate. By the same token, we can simply remove the attribute a (where every possible value of a occurs with every tuple from R) from R´ and not change anything significant.

I make the claim that the absence of an attribute is equivalent to having the cross-product with every possible value for that attribute.

Look at J = R join S. If S contains a, ...

Then there are legitimate values for S that contain all possible a-values. How do we distinguish that from a value for S (or R) that contain all a-values gratuitously? I suppose we need to hold a heading against each value that is potentially different from the gratuitous attributes that appear in its (alleged) body; and manipulate the genuine heading to establish whether two queries are equivalent (produce the same answers for each possible value of the database). Then ...

... By a similar reasoning, DUM is equivalent to Dumpty, i.e. "nothing is true whatever attributes we look at". In that case, no need to search for DUM, we already have it represented as Dumpty.

The critical features of DUM are that not only is it empty, but also it has no attributes. To get the heading of r: r NatJoin DUM whereas r NatJoin Dumpty = Dumpty for all r. So now I can't tell whether two relations have the same heading -- by which I mean genuine heading, not gratuitously-full heading. I've tried to define emptify( r ), but all definitions turn out to be equivalent to requiring DUM.

Similarly if I want to find out if (or stipulate that) two relations have no attributes in common: (r NatJoin DUM) InnerUnion (s NatJoin DUM) = DUM. That holds because DUM has no attributes. I can't use DEE in the role of empty-heading tester (supposing DEE hasn't got all those gratuitous attributes), because r, s might be both empty, then their InnerUnion won't be DEE. And let me cut off more nonsense: r InnerUnion DEE = DEE for all r, so we can't use DEE in the role of DUM somehow. We could go by (r InnerUnion Fullest) InnerUnion (s InnerUnion Fullest) = DEE to distinguish non-overlapping headings; you've just turned the problem outside-in: how to define Fullest and distinguish it from DEE? Your post just magically waved Fullest into existence.

#73 · May 25, 2021, 5:20 am

The critical features of DUM are that not only is it empty, but also it has no attributes. To get the heading of r: r NatJoin DUM whereas r NatJoin Dumpty = Dumpty for all r. So now I can't tell whether two relations have the same heading -- by which I mean genuine heading, not gratuitously-full heading. I've tried to define emptify( r ), but all definitions turn out to be equivalent to requiring DUM.

True.

Maybe the real root of the problem is that you pretend to be agnostic to inner structure, yet your proofs require that something corresponding to a heading exists?

#74 · May 25, 2021, 12:52 pm

Quote from tobega on May 25, 2021, 5:20 am

The critical features of DUM are that not only is it empty, but also it has no attributes. To get the heading of r: r NatJoin DUM whereas r NatJoin Dumpty = Dumpty for all r. So now I can't tell whether two relations have the same heading -- by which I mean genuine heading, not gratuitously-full heading. I've tried to define emptify( r ), but all definitions turn out to be equivalent to requiring DUM.

True.

Maybe the real root of the problem is that you pretend to be agnostic to inner structure, yet your proofs require that something corresponding to a heading exists?

Mathematically it seems to be easy to discover the heading-like structure, but I don't know if it works in the solver:

Consider all the (sub-)lattices ordered by NatJoin (as per your spec) that have DEE as their join (and do not only consist of DEE). We can form a lattice of these lattices and order them by NatJoin on their respective meets.

The join of the (sub)lattices must be the lattice containing only DEE and DUM.

#75 · May 25, 2021, 9:53 pm

Quote from AntC on May 25, 2021, 9:53 pm

Quote from tobega on May 25, 2021, 12:52 pm

Quote from tobega on May 25, 2021, 5:20 am

The critical features of DUM are that not only is it empty, but also it has no attributes. To get the heading of r: r NatJoin DUM whereas r NatJoin Dumpty = Dumpty for all r. So now I can't tell whether two relations have the same heading -- by which I mean genuine heading, not gratuitously-full heading. I've tried to define emptify( r ), but all definitions turn out to be equivalent to requiring DUM.

True.

Maybe the real root of the problem is that you pretend to be agnostic to inner structure, yet your proofs require that something corresponding to a heading exists?

I'm notionally using the emptified value to act as heading. I'm trying to denote that by r NatJoin DUM. But since I so far can't fix DUM (with modelling all the characteristics I need), this hasn't got beyond notional.

Mathematically it seems to be easy to discover the heading-like structure, but I don't know if it works in the solver:

Consider all the (sub-)lattices ordered by NatJoin (as per your spec) that have DEE as their join (and do not only consist of DEE).

Really really you need to look at the wiki. What's "ordered by NatJoin" is elements, not lattices. You perhaps mean DEE as supremum aka top? I.e. 1 here: "A bounded lattice is an algebraic structure of the form $(L,\vee ,\wedge ,0,1)$ " You can't talk about a sub-lattice as if it's just some random subset of the elements. It must have a top and a bottom such that any NatJoin of elements from the sub-lattice falls within them. Then there's only one 'sub-lattice' with DEE as its top, and that's the whole lattice. Then it's only a 'sub-lattice' in the sense non-strict 'subset'.

We can form a lattice of these lattices and order them by NatJoin on their respective meets.

Meaningless. NatJoin is a function over elements, not over (sub-)lattices; elements 'meet', not sub-lattices. You might say sub-lattices 'overlap' then the smaller must be a sub-lattice of the larger -- that is, completely contained within it.

The join of the (sub)lattices must be the lattice containing only DEE and DUM.

Meaningless.

Quote from tobega on May 25, 2021, 12:52 pm

Quote from tobega on May 25, 2021, 5:20 am

The critical features of DUM are that not only is it empty, but also it has no attributes. To get the heading of r: r NatJoin DUM whereas r NatJoin Dumpty = Dumpty for all r. So now I can't tell whether two relations have the same heading -- by which I mean genuine heading, not gratuitously-full heading. I've tried to define emptify( r ), but all definitions turn out to be equivalent to requiring DUM.

True.

Maybe the real root of the problem is that you pretend to be agnostic to inner structure, yet your proofs require that something corresponding to a heading exists?

I'm notionally using the emptified value to act as heading. I'm trying to denote that by r NatJoin DUM. But since I so far can't fix DUM (with modelling all the characteristics I need), this hasn't got beyond notional.

Mathematically it seems to be easy to discover the heading-like structure, but I don't know if it works in the solver:

Consider all the (sub-)lattices ordered by NatJoin (as per your spec) that have DEE as their join (and do not only consist of DEE).

Really really you need to look at the wiki. What's "ordered by NatJoin" is elements, not lattices. You perhaps mean DEE as supremum aka top? I.e. 1 here: "A bounded lattice is an algebraic structure of the form $(L,\vee ,\wedge ,0,1)$ " You can't talk about a sub-lattice as if it's just some random subset of the elements. It must have a top and a bottom such that any NatJoin of elements from the sub-lattice falls within them. Then there's only one 'sub-lattice' with DEE as its top, and that's the whole lattice. Then it's only a 'sub-lattice' in the sense non-strict 'subset'.

We can form a lattice of these lattices and order them by NatJoin on their respective meets.

Meaningless. NatJoin is a function over elements, not over (sub-)lattices; elements 'meet', not sub-lattices. You might say sub-lattices 'overlap' then the smaller must be a sub-lattice of the larger -- that is, completely contained within it.

The join of the (sub)lattices must be the lattice containing only DEE and DUM.

Meaningless.

#76 · May 26, 2021, 9:29 am

Quote from tobega on May 26, 2021, 9:29 am

Quote from AntC on May 25, 2021, 9:53 pm

Quote from tobega on May 25, 2021, 12:52 pm

Quote from tobega on May 25, 2021, 5:20 am

The critical features of DUM are that not only is it empty, but also it has no attributes. To get the heading of r: r NatJoin DUM whereas r NatJoin Dumpty = Dumpty for all r. So now I can't tell whether two relations have the same heading -- by which I mean genuine heading, not gratuitously-full heading. I've tried to define emptify( r ), but all definitions turn out to be equivalent to requiring DUM.

True.

Maybe the real root of the problem is that you pretend to be agnostic to inner structure, yet your proofs require that something corresponding to a heading exists?

I'm notionally using the emptified value to act as heading. I'm trying to denote that by r NatJoin DUM. But since I so far can't fix DUM (with modelling all the characteristics I need), this hasn't got beyond notional.

Exactly. You need to prove that the structure you need exists, you can't just assume there is such a thing as an emptified heading.

Mathematically it seems to be easy to discover the heading-like structure, but I don't know if it works in the solver:

Consider all the (sub-)lattices ordered by NatJoin (as per your spec) that have DEE as their join (and do not only consist of DEE).

Really really you need to look at the wiki. What's "ordered by NatJoin" is elements, not lattices. You perhaps mean DEE as supremum aka top? I.e. 1 here: "A bounded lattice is an algebraic structure of the form $(L,\vee ,\wedge ,0,1)$ " You can't talk about a sub-lattice as if it's just some random subset of the elements. It must have a top and a bottom such that any NatJoin of elements from the sub-lattice falls within them. Then there's only one 'sub-lattice' with DEE as its top, and that's the whole lattice. Then it's only a 'sub-lattice' in the sense non-strict 'subset'.

I have looked at the wiki which has fixed some of the limitations in my knowledge base.

I'll start at a very basic level, just to make sure we are on the same page (and also for the benefit of the kibitzers) and try to spell things out in as tedious detail as I care to.

We start with the set of all possible relations. In our mathematical model it is for now just a set of things, we'll have to define their interesting properties, but we know what we're modelling them on.

We have operations, NatJoin modelled on natural join and InnerUnion modelled on inner union. Again, we know how we want these to work, but in our mathematical model we will have to define their interesting properties.

The first thing of note is that our set is closed under our operations. No matter how much we NatJoin and InnerUnion we will always stay inside our set.

The second thing of note is that we can use our operations to induce a partial order on our elements. I'll reverse the order you've been assigning, because it will feel better later on. So the NatJoin of two elements will give a least upper bound (aka supremum or join) of the two elements (An example of supremum for the divisibility of the set of integers could be the lowest common multiple). The InnerUnion will give a greatest lower bound (aka infimum or meet) of the two elements (The divisibility example for integers here is greatest common divisor). As far as I can tell, this is what makes it a lattice, but how significant that fact is I don't really know.

By this ordering, we can find a unique smallest element, which turns out to correspond to DEE, anything InnerUnion DEE ends up as DEE. There is also a unique largest element, which has been called Dumpty, which corresponds to the relation with all possible attributes but no tuples. Anything NatJoin Dumpty ends up as Dumpty. (We can also note that any R NatJoin DEE is R, as is R InnerUnion Dumpty, but that may be just a curiosity so far)

At the other "corners", we would like to have DUM, which turns out to be a little elusive to pinpoint, and Fullest, which is a little hard to handle, containing all possible tuples of all possible attributes.

OK, now consider the set of all relations of a particular heading, A₁..A_n. This set turns out to have all the same properties as our full set. It is closed under our operations and we can partially order them by our operations. The largest element is what I have previously called DUM(A1..An), the relation with those attributes and no tuples , while the smallest is what I have previously called DEE(A₁..A_n), the relation with all possible tuples of those attribute. Here the largest/smallest ordering becomes counter-intuitive, but never mind, we won't stay here because DEE(A₁..A_n) is a difficult beast. Anyway, as far as I can tell, this is then a lattice ¯\_(ツ)_/¯

Let's now instead consider the set of all relations of all subsets of a particular heading A₁..A_n. Again, all the important properties apply. Our smallest element is DEE and our largest is DUM(A₁..A_n). Nice and manageable. What shall we call this? A "dictionary space" perhaps? So a DS(A₁..A_n) if we want to specify the heading.

Now a "dictionary space" is a thing, and we can create one of those for every possible heading, so we can have a set of all of them. As a curiosity, we can note that DS(A₁..A_n) is completely contained inside DS(A₁..A_n, A_n+1). Specifically, DS() is the set containing just DEE and DUM and is contained in all the others. (There are two annoying things that mathematically fulfil our properties that we need to make sure we've kept out, the set of just DEE and the set of just DUM. There may be some other sick cases as well that we need to eliminate.)

So what can we do with our set of dictionary spaces? Well, we know they all have the same smallest element, DEE, and they each have a unique largest element, a DUM(A₁..A_n), which we can use to identify the dictionary space. It also turns out that we can create a partial order on the dictionary spaces, by applying NatJoin and InnerUnion on their largest elements (or their identifying elements, if you like). As far as I can tell, this makes it a lattice, but that's probably not important. As a curiosity, the infimum of two dictionary spaces (found by InnerUnion) will be the largest dictionary space that is contained in both, while the supremum (found by NatJoin) will be the smallest dictionary space that contains both.

Now the smallest dictionary space by our ordering is DS(), containing just DEE and DUM.

Whether that may be of use to you or not, I don't know.

Quote from AntC on May 25, 2021, 9:53 pm

Quote from tobega on May 25, 2021, 12:52 pm

Quote from tobega on May 25, 2021, 5:20 am

The critical features of DUM are that not only is it empty, but also it has no attributes. To get the heading of r: r NatJoin DUM whereas r NatJoin Dumpty = Dumpty for all r. So now I can't tell whether two relations have the same heading -- by which I mean genuine heading, not gratuitously-full heading. I've tried to define emptify( r ), but all definitions turn out to be equivalent to requiring DUM.

True.

Maybe the real root of the problem is that you pretend to be agnostic to inner structure, yet your proofs require that something corresponding to a heading exists?

I'm notionally using the emptified value to act as heading. I'm trying to denote that by r NatJoin DUM. But since I so far can't fix DUM (with modelling all the characteristics I need), this hasn't got beyond notional.

Exactly. You need to prove that the structure you need exists, you can't just assume there is such a thing as an emptified heading.

Mathematically it seems to be easy to discover the heading-like structure, but I don't know if it works in the solver:

Consider all the (sub-)lattices ordered by NatJoin (as per your spec) that have DEE as their join (and do not only consist of DEE).

Really really you need to look at the wiki. What's "ordered by NatJoin" is elements, not lattices. You perhaps mean DEE as supremum aka top? I.e. 1 here: "A bounded lattice is an algebraic structure of the form $(L,\vee ,\wedge ,0,1)$ " You can't talk about a sub-lattice as if it's just some random subset of the elements. It must have a top and a bottom such that any NatJoin of elements from the sub-lattice falls within them. Then there's only one 'sub-lattice' with DEE as its top, and that's the whole lattice. Then it's only a 'sub-lattice' in the sense non-strict 'subset'.

I have looked at the wiki which has fixed some of the limitations in my knowledge base.

I'll start at a very basic level, just to make sure we are on the same page (and also for the benefit of the kibitzers) and try to spell things out in as tedious detail as I care to.

We start with the set of all possible relations. In our mathematical model it is for now just a set of things, we'll have to define their interesting properties, but we know what we're modelling them on.

We have operations, NatJoin modelled on natural join and InnerUnion modelled on inner union. Again, we know how we want these to work, but in our mathematical model we will have to define their interesting properties.

The first thing of note is that our set is closed under our operations. No matter how much we NatJoin and InnerUnion we will always stay inside our set.

The second thing of note is that we can use our operations to induce a partial order on our elements. I'll reverse the order you've been assigning, because it will feel better later on. So the NatJoin of two elements will give a least upper bound (aka supremum or join) of the two elements (An example of supremum for the divisibility of the set of integers could be the lowest common multiple). The InnerUnion will give a greatest lower bound (aka infimum or meet) of the two elements (The divisibility example for integers here is greatest common divisor). As far as I can tell, this is what makes it a lattice, but how significant that fact is I don't really know.

By this ordering, we can find a unique smallest element, which turns out to correspond to DEE, anything InnerUnion DEE ends up as DEE. There is also a unique largest element, which has been called Dumpty, which corresponds to the relation with all possible attributes but no tuples. Anything NatJoin Dumpty ends up as Dumpty. (We can also note that any R NatJoin DEE is R, as is R InnerUnion Dumpty, but that may be just a curiosity so far)

At the other "corners", we would like to have DUM, which turns out to be a little elusive to pinpoint, and Fullest, which is a little hard to handle, containing all possible tuples of all possible attributes.

OK, now consider the set of all relations of a particular heading, A₁..A_n. This set turns out to have all the same properties as our full set. It is closed under our operations and we can partially order them by our operations. The largest element is what I have previously called DUM(A1..An), the relation with those attributes and no tuples , while the smallest is what I have previously called DEE(A₁..A_n), the relation with all possible tuples of those attribute. Here the largest/smallest ordering becomes counter-intuitive, but never mind, we won't stay here because DEE(A₁..A_n) is a difficult beast. Anyway, as far as I can tell, this is then a lattice ¯\_(ツ)_/¯

Let's now instead consider the set of all relations of all subsets of a particular heading A₁..A_n. Again, all the important properties apply. Our smallest element is DEE and our largest is DUM(A₁..A_n). Nice and manageable. What shall we call this? A "dictionary space" perhaps? So a DS(A₁..A_n) if we want to specify the heading.

Now a "dictionary space" is a thing, and we can create one of those for every possible heading, so we can have a set of all of them. As a curiosity, we can note that DS(A₁..A_n) is completely contained inside DS(A₁..A_n, A_n+1). Specifically, DS() is the set containing just DEE and DUM and is contained in all the others. (There are two annoying things that mathematically fulfil our properties that we need to make sure we've kept out, the set of just DEE and the set of just DUM. There may be some other sick cases as well that we need to eliminate.)

So what can we do with our set of dictionary spaces? Well, we know they all have the same smallest element, DEE, and they each have a unique largest element, a DUM(A₁..A_n), which we can use to identify the dictionary space. It also turns out that we can create a partial order on the dictionary spaces, by applying NatJoin and InnerUnion on their largest elements (or their identifying elements, if you like). As far as I can tell, this makes it a lattice, but that's probably not important. As a curiosity, the infimum of two dictionary spaces (found by InnerUnion) will be the largest dictionary space that is contained in both, while the supremum (found by NatJoin) will be the smallest dictionary space that contains both.

Now the smallest dictionary space by our ordering is DS(), containing just DEE and DUM.

Whether that may be of use to you or not, I don't know.

#77 · May 26, 2021, 11:25 am

Quote from AntC on May 26, 2021, 11:25 am

Quote from tobega on May 26, 2021, 9:29 am

Quote from AntC on May 25, 2021, 9:53 pm

Quote from tobega on May 25, 2021, 12:52 pm

Quote from tobega on May 25, 2021, 5:20 am

The critical features of DUM are that not only is it empty, but also it has no attributes. To get the heading of r: r NatJoin DUM whereas r NatJoin Dumpty = Dumpty for all r. So now I can't tell whether two relations have the same heading -- by which I mean genuine heading, not gratuitously-full heading. I've tried to define emptify( r ), but all definitions turn out to be equivalent to requiring DUM.

True.

Maybe the real root of the problem is that you pretend to be agnostic to inner structure, yet your proofs require that something corresponding to a heading exists?

I'm notionally using the emptified value to act as heading. I'm trying to denote that by r NatJoin DUM. But since I so far can't fix DUM (with modelling all the characteristics I need), this hasn't got beyond notional.

Exactly. You need to prove that the structure you need exists, you can't just assume there is such a thing as an emptified heading.

As you point out below "No matter how much we NatJoin and InnerUnion we will always stay inside our set." Then relation value DUM is in my set, so must be r NatJoin DUM for all elements r.

Mathematically it seems to be easy to discover the heading-like structure, but I don't know if it works in the solver:

Consider all the (sub-)lattices ordered by NatJoin (as per your spec) that have DEE as their join (and do not only consist of DEE).

Really really you need to look at the wiki. What's "ordered by NatJoin" is elements, not lattices. You perhaps mean DEE as supremum aka top? I.e. 1 here: "A bounded lattice is an algebraic structure of the form $(L,\vee ,\wedge ,0,1)$ " You can't talk about a sub-lattice as if it's just some random subset of the elements. It must have a top and a bottom such that any NatJoin of elements from the sub-lattice falls within them. Then there's only one 'sub-lattice' with DEE as its top, and that's the whole lattice. Then it's only a 'sub-lattice' in the sense non-strict 'subset'.

I have looked at the wiki which has fixed some of the limitations in my knowledge base.

You'll have noticed there's a lot of formulas. What's remarkable below is you've introduced a whole lot of upside-down fluffy words, without a skerrick of logic or formulas.

I'll start at a very basic level, ...

Quote from tobega on May 26, 2021, 9:29 am

Quote from AntC on May 25, 2021, 9:53 pm

Quote from tobega on May 25, 2021, 12:52 pm

Quote from tobega on May 25, 2021, 5:20 am

The critical features of DUM are that not only is it empty, but also it has no attributes. To get the heading of r: r NatJoin DUM whereas r NatJoin Dumpty = Dumpty for all r. So now I can't tell whether two relations have the same heading -- by which I mean genuine heading, not gratuitously-full heading. I've tried to define emptify( r ), but all definitions turn out to be equivalent to requiring DUM.

True.

Maybe the real root of the problem is that you pretend to be agnostic to inner structure, yet your proofs require that something corresponding to a heading exists?

I'm notionally using the emptified value to act as heading. I'm trying to denote that by r NatJoin DUM. But since I so far can't fix DUM (with modelling all the characteristics I need), this hasn't got beyond notional.

Exactly. You need to prove that the structure you need exists, you can't just assume there is such a thing as an emptified heading.

As you point out below "No matter how much we NatJoin and InnerUnion we will always stay inside our set." Then relation value DUM is in my set, so must be r NatJoin DUM for all elements r.

Mathematically it seems to be easy to discover the heading-like structure, but I don't know if it works in the solver:

Consider all the (sub-)lattices ordered by NatJoin (as per your spec) that have DEE as their join (and do not only consist of DEE).

Really really you need to look at the wiki. What's "ordered by NatJoin" is elements, not lattices. You perhaps mean DEE as supremum aka top? I.e. 1 here: "A bounded lattice is an algebraic structure of the form $(L,\vee ,\wedge ,0,1)$ " You can't talk about a sub-lattice as if it's just some random subset of the elements. It must have a top and a bottom such that any NatJoin of elements from the sub-lattice falls within them. Then there's only one 'sub-lattice' with DEE as its top, and that's the whole lattice. Then it's only a 'sub-lattice' in the sense non-strict 'subset'.

I have looked at the wiki which has fixed some of the limitations in my knowledge base.

You'll have noticed there's a lot of formulas. What's remarkable below is you've introduced a whole lot of upside-down fluffy words, without a skerrick of logic or formulas.

I'll start at a very basic level, ...

#78 · May 26, 2021, 2:02 pm

Quote from tobega on May 26, 2021, 2:02 pm

Quote from AntC on May 26, 2021, 11:25 am

Quote from tobega on May 26, 2021, 9:29 am

Quote from AntC on May 25, 2021, 9:53 pm

Quote from tobega on May 25, 2021, 12:52 pm

Quote from tobega on May 25, 2021, 5:20 am

The critical features of DUM are that not only is it empty, but also it has no attributes. To get the heading of r: r NatJoin DUM whereas r NatJoin Dumpty = Dumpty for all r. So now I can't tell whether two relations have the same heading -- by which I mean genuine heading, not gratuitously-full heading. I've tried to define emptify( r ), but all definitions turn out to be equivalent to requiring DUM.

True.

Maybe the real root of the problem is that you pretend to be agnostic to inner structure, yet your proofs require that something corresponding to a heading exists?

I'm notionally using the emptified value to act as heading. I'm trying to denote that by r NatJoin DUM. But since I so far can't fix DUM (with modelling all the characteristics I need), this hasn't got beyond notional.

Exactly. You need to prove that the structure you need exists, you can't just assume there is such a thing as an emptified heading.

As you point out below "No matter how much we NatJoin and InnerUnion we will always stay inside our set." Then relation value DUM is in my set, so must be r NatJoin DUM for all elements r.

Mmmm. Except you seem to have a hard time finding/pinpointing DUM. I'm trying to suggest that perhaps you may need to demonstrate the property/structure that gives rise to that behaviour in order to find DUM.

Mathematically it seems to be easy to discover the heading-like structure, but I don't know if it works in the solver:

Consider all the (sub-)lattices ordered by NatJoin (as per your spec) that have DEE as their join (and do not only consist of DEE).

Really really you need to look at the wiki. What's "ordered by NatJoin" is elements, not lattices. You perhaps mean DEE as supremum aka top? I.e. 1 here: "A bounded lattice is an algebraic structure of the form $(L,\vee ,\wedge ,0,1)$ " You can't talk about a sub-lattice as if it's just some random subset of the elements. It must have a top and a bottom such that any NatJoin of elements from the sub-lattice falls within them. Then there's only one 'sub-lattice' with DEE as its top, and that's the whole lattice. Then it's only a 'sub-lattice' in the sense non-strict 'subset'.

I have looked at the wiki which has fixed some of the limitations in my knowledge base.

You'll have noticed there's a lot of formulas. What's remarkable below is you've introduced a whole lot of upside-down fluffy words, without a skerrick of logic or formulas.

Formulas, no, logic, yes, I am a mathematician of the humanist kind. The mathematics here is very trivial. I'm sorry it's not in your preferred format but it shouldn't be too hard to understand. Whether it's actually possible to turn it into the formulas you need is of course another question.

Anyway, I've already spent more time on this than I was initially inclined to, although it's been somewhat interesting. I would have hoped I might have been of some help, but if not, c'est la vie.

Quote from AntC on May 26, 2021, 11:25 am

Quote from tobega on May 26, 2021, 9:29 am

Quote from AntC on May 25, 2021, 9:53 pm

Quote from tobega on May 25, 2021, 12:52 pm

Quote from tobega on May 25, 2021, 5:20 am

The critical features of DUM are that not only is it empty, but also it has no attributes. To get the heading of r: r NatJoin DUM whereas r NatJoin Dumpty = Dumpty for all r. So now I can't tell whether two relations have the same heading -- by which I mean genuine heading, not gratuitously-full heading. I've tried to define emptify( r ), but all definitions turn out to be equivalent to requiring DUM.

True.

Maybe the real root of the problem is that you pretend to be agnostic to inner structure, yet your proofs require that something corresponding to a heading exists?

I'm notionally using the emptified value to act as heading. I'm trying to denote that by r NatJoin DUM. But since I so far can't fix DUM (with modelling all the characteristics I need), this hasn't got beyond notional.

Exactly. You need to prove that the structure you need exists, you can't just assume there is such a thing as an emptified heading.

As you point out below "No matter how much we NatJoin and InnerUnion we will always stay inside our set." Then relation value DUM is in my set, so must be r NatJoin DUM for all elements r.

Mmmm. Except you seem to have a hard time finding/pinpointing DUM. I'm trying to suggest that perhaps you may need to demonstrate the property/structure that gives rise to that behaviour in order to find DUM.

Mathematically it seems to be easy to discover the heading-like structure, but I don't know if it works in the solver:

Consider all the (sub-)lattices ordered by NatJoin (as per your spec) that have DEE as their join (and do not only consist of DEE).

Really really you need to look at the wiki. What's "ordered by NatJoin" is elements, not lattices. You perhaps mean DEE as supremum aka top? I.e. 1 here: "A bounded lattice is an algebraic structure of the form $(L,\vee ,\wedge ,0,1)$ " You can't talk about a sub-lattice as if it's just some random subset of the elements. It must have a top and a bottom such that any NatJoin of elements from the sub-lattice falls within them. Then there's only one 'sub-lattice' with DEE as its top, and that's the whole lattice. Then it's only a 'sub-lattice' in the sense non-strict 'subset'.

I have looked at the wiki which has fixed some of the limitations in my knowledge base.

You'll have noticed there's a lot of formulas. What's remarkable below is you've introduced a whole lot of upside-down fluffy words, without a skerrick of logic or formulas.

Formulas, no, logic, yes, I am a mathematician of the humanist kind. The mathematics here is very trivial. I'm sorry it's not in your preferred format but it shouldn't be too hard to understand. Whether it's actually possible to turn it into the formulas you need is of course another question.

Anyway, I've already spent more time on this than I was initially inclined to, although it's been somewhat interesting. I would have hoped I might have been of some help, but if not, c'est la vie.

#79 · May 26, 2021, 4:45 pm

Quote from Vadim on May 26, 2021, 4:45 pm

Quote from tobega on May 26, 2021, 9:29 am

We start with the set of all possible relations. In our mathematical model it is for now just a set of things, we'll have to define their interesting properties, but we know what we're modelling them on.

If each relation in this set is finite (that is their header and tuple sets are finite), then you will have difficulty identifying [latex]R_{11}[/latex], [latex]R_{10}[/latex], because they can't possibly have finite set of attributes. Can you start with a finite set of relations (such as the one at Fig.1)?

...

The second thing of note is that we can use our operations to induce a partial order on our elements. I'll reverse the order you've been assigning, because it will feel better later on. So the NatJoin of two elements will give a least upper bound (aka supremum or join) of the two elements (An example of supremum for the divisibility of the set of integers could be the lowest common multiple). The InnerUnion will give a greatest lower bound (aka infimum or meet) of the two elements (The divisibility example for integers here is greatest common divisor). As far as I can tell, this is what makes it a lattice, but how significant that fact is I don't really know.

It is the absorption law that says that the partial orders from the upper and lower semilattices are the same, so that the structure is actually a lattice. Litak&Mikulas&Hidders noticed that the lattice structure is evident by exibiting a closure operator.

By this ordering, we can find a unique smallest element, which turns out to correspond to DEE, anything InnerUnion DEE ends up as DEE. There is also a unique largest element, which has been called Dumpty, which corresponds to the relation with all possible attributes but no tuples. Anything NatJoin Dumpty ends up as Dumpty. (We can also note that any R NatJoin DEE is R, as is R InnerUnion Dumpty, but that may be just a curiosity so far)

Again, you have to restrict the set of admissible relations, or allow relations with infinite signature to have both the lattice top and the bottom.

At the other "corners", we would like to have DUM, which turns out to be a little elusive to pinpoint, and Fullest, which is a little hard to handle, containing all possible tuples of all possible attributes.

I'll add the lattice top (or bottom if you reverse the definition of lattice order) to this list.

Returning to the main theme of this and other threads, I don't subscribe to the idea that some of these 4 constants are elusive. They are well defined when you cosider a finite set of relations closed under the [latex]\wedge, \vee[/latex]. (There also might be additional requirement of the closure under unary operations of attributes inverse and tuple complement). For future references let's call such closed set of relations a universe.

It is only when we start examining the individual relation structure (assuming that we are equipped with such means), and then compare the constants from different universes, then we become somewhat confused. For example in "normal" universes, the [latex]R_{00}[/latex], [latex]R_{01}[/latex] have the empty header, but this property doesn't hold for all universes.

I'm also skeptical about the uniqueness concept promoted by Anthony. Consider a general lattice. Is the lattice top and bottom unique (if exist)? Well, yes, but why do we raise this question about only the two operations, that happen to be zilliary ones. Why don't we ask if join and meet are unique? And they don't.

Quote from tobega on May 26, 2021, 9:29 am

We start with the set of all possible relations. In our mathematical model it is for now just a set of things, we'll have to define their interesting properties, but we know what we're modelling them on.

If each relation in this set is finite (that is their header and tuple sets are finite), then you will have difficulty identifying $R_{11}$ , $R_{10}$ , because they can't possibly have finite set of attributes. Can you start with a finite set of relations (such as the one at Fig.1)?

...

The second thing of note is that we can use our operations to induce a partial order on our elements. I'll reverse the order you've been assigning, because it will feel better later on. So the NatJoin of two elements will give a least upper bound (aka supremum or join) of the two elements (An example of supremum for the divisibility of the set of integers could be the lowest common multiple). The InnerUnion will give a greatest lower bound (aka infimum or meet) of the two elements (The divisibility example for integers here is greatest common divisor). As far as I can tell, this is what makes it a lattice, but how significant that fact is I don't really know.

It is the absorption law that says that the partial orders from the upper and lower semilattices are the same, so that the structure is actually a lattice. Litak&Mikulas&Hidders noticed that the lattice structure is evident by exibiting a closure operator.

By this ordering, we can find a unique smallest element, which turns out to correspond to DEE, anything InnerUnion DEE ends up as DEE. There is also a unique largest element, which has been called Dumpty, which corresponds to the relation with all possible attributes but no tuples. Anything NatJoin Dumpty ends up as Dumpty. (We can also note that any R NatJoin DEE is R, as is R InnerUnion Dumpty, but that may be just a curiosity so far)

Again, you have to restrict the set of admissible relations, or allow relations with infinite signature to have both the lattice top and the bottom.

At the other "corners", we would like to have DUM, which turns out to be a little elusive to pinpoint, and Fullest, which is a little hard to handle, containing all possible tuples of all possible attributes.

I'll add the lattice top (or bottom if you reverse the definition of lattice order) to this list.

Returning to the main theme of this and other threads, I don't subscribe to the idea that some of these 4 constants are elusive. They are well defined when you cosider a finite set of relations closed under the $\wedge, \vee$ . (There also might be additional requirement of the closure under unary operations of attributes inverse and tuple complement). For future references let's call such closed set of relations a universe.

It is only when we start examining the individual relation structure (assuming that we are equipped with such means), and then compare the constants from different universes, then we become somewhat confused. For example in "normal" universes, the $R_{00}$ , $R_{01}$ have the empty header, but this property doesn't hold for all universes.

I'm also skeptical about the uniqueness concept promoted by Anthony. Consider a general lattice. Is the lattice top and bottom unique (if exist)? Well, yes, but why do we raise this question about only the two operations, that happen to be zilliary ones. Why don't we ask if join and meet are unique? And they don't.

#80 · May 26, 2021, 11:42 pm

Quote from AntC on May 26, 2021, 11:42 pm

Quote from Vadim on May 26, 2021, 4:45 pm

Quote from tobega on May 26, 2021, 9:29 am

We start with the set of all possible relations. In our mathematical model it is for now just a set of things, we'll have to define their interesting properties, but we know what we're modelling them on.

If each relation in this set is finite (that is their header and tuple sets are finite), then you will have difficulty identifying [latex]R_{11}[/latex], [latex]R_{10}[/latex], because they can't possibly have finite set of attributes. Can you start with a finite set of relations (such as the one at Fig.1)?

Yes you can. Specifically you can start with a non-empty relation r (which in your Figure 1 would be the one in the middle with heading x, y and 4 tuples) and build a relational lattice by taking subsets from it, down (in size) to DEE, DUM, (r NatJoin DUM). Then r is acting as R11 aka Fullest relative to this lattice, and (r NatJoin DUM) as R10 aka Dumpty. Then this earlier comment from me is wrong:

Then there's only one 'sub-lattice' with DEE as its top, and that's the whole lattice.

The thing to note here is how many Boolean algebras we induce:

We've already seen that by taking all possible subsets of the tuples in r (including the empty subset known as r NatJoin DUM), we get an 'ordering by inclusion' Pic 1 here. (And note, @tobega, that has the empty subset at the bottom. That's why empty relations are at the bottom of relational lattices and therefore why NatJoin is the way down it is.
Because this is a Boolean algebra, it's distributive, but I've not realised what is a more useful: it's uniquely (relatively) complemented and the double-complement is identity. That's why unioning a Matching, NotMatching give us back r. (See the equations on the wiki that define complement.)

We've also already noted that having emptified r, we can take all possible subsets of the heading of r (including the empty subset which is the heading for DUM, DEE), we get another ordering by inclusion, but because these are headings not bodies (there are no tuples), the ordering is in reverse: a smaller heading is the 'higher'/closer towards DUM.
This is again a Boolean algebra, distributive and uniquely (relatively) complemented.

We can also start at r with its body, take all possible subsets of the heading of r (as with emptified r, including the empty subset), project the body of r on to each heading, we get another ordering by inclusion, again in reverse: the smaller the heading is, the 'higher'/closer towards DEE -- and the procedure is bound to generate DEE because we started with non-empty r.
Because this is a Boolean algebra, it's uniquely (relatively) complemented and the double-complement is identity. So project, Remove give us complementary projections of r.

Unfortunately there's no operation (as there is with Matching, NotMatching) to get back to r from complementary project, Remove. The operation ought to be NatJoin, but since deliberately there's no attributes in common, that degenerates to Cartesian product so will in general create fictitious tuples that weren't in the original r.

To build this relational lattice that is a sub-lattice, I didn't need to know the types of the attributes of r, nor what might be all possible tuples for r's heading. So the Boolean algebra sub-lattice from r up to DEE rises 'slantwise' relative to the top face of the overall lattice containing all possible tuples.

It is only when we start examining the individual relation structure (assuming that we are equipped with such means), and then compare the constants from different universes, then we become somewhat confused. For example in "normal" universes, the [latex]R_{00}[/latex], [latex]R_{01}[/latex] have the empty header, but this property doesn't hold for all universes.

It holds for all relational lattices. I just told you how to construct a sub-'universe' starting from some non-empty relation value.

What do you mean by "different" universes? Just because two relation values within a lattice have different headings (possibly empty heading) doesn't make them significantly different. They must be joinable, at which point they produce 'merged' tuples. Do you want that to be a third 'universe'? Likewise they must support project, Remove, again producing relations with different headings. Do you want that to be a fourth and fifth 'universe'?

The one lattice structure must support the result from all relational operations, otherwise the algebra isn't complete: Codd 1972, TTM RM Pre 18, Pre 6, Pre 7, Appendix A.

I'm also skeptical about the uniqueness concept promoted by Anthony. Consider a general lattice. Is the lattice top and bottom unique (if exist)?

Yes. Proven very quickly by Prover9. Don't you always do that as a sanity check when building a new model? After I've proved the uniqueness of lattice bottom, though, it doesn't seem useful. In particular, it doesn't help find emptified r -- I know that is somewhere 'between' DUM and bottom/within the Boolean algebra of empty relation values, but only DUM is useful in finding it.

Well, yes, but why do we raise this question about only the two operations, that happen to be zilliary ones.

DEE uniqueness is proven very quickly by Prover9. Don't you always do that as a sanity check when building a new model?

Why don't we ask if join and meet are unique?

I do ask. Proven very quickly by Prover9. Don't you always do that as a sanity check when building a new model?

And they don't.

?? Who/which don't what?

I want all operations and constants to be provably unique. Otherwise any claimed equivalence between queries using them is illusory.

Quote from Vadim on May 26, 2021, 4:45 pm

Quote from tobega on May 26, 2021, 9:29 am

We start with the set of all possible relations. In our mathematical model it is for now just a set of things, we'll have to define their interesting properties, but we know what we're modelling them on.

If each relation in this set is finite (that is their header and tuple sets are finite), then you will have difficulty identifying $R_{11}$ , $R_{10}$ , because they can't possibly have finite set of attributes. Can you start with a finite set of relations (such as the one at Fig.1)?

Yes you can. Specifically you can start with a non-empty relation r (which in your Figure 1 would be the one in the middle with heading x, y and 4 tuples) and build a relational lattice by taking subsets from it, down (in size) to DEE, DUM, (r NatJoin DUM). Then r is acting as R11 aka Fullest relative to this lattice, and (r NatJoin DUM) as R10 aka Dumpty. Then this earlier comment from me is wrong:

Then there's only one 'sub-lattice' with DEE as its top, and that's the whole lattice.

The thing to note here is how many Boolean algebras we induce:

We've already seen that by taking all possible subsets of the tuples in r (including the empty subset known as r NatJoin DUM), we get an 'ordering by inclusion' Pic 1 here. (And note, @tobega, that has the empty subset at the bottom. That's why empty relations are at the bottom of relational lattices and therefore why NatJoin is the way down it is.
Because this is a Boolean algebra, it's distributive, but I've not realised what is a more useful: it's uniquely (relatively) complemented and the double-complement is identity. That's why unioning a Matching, NotMatching give us back r. (See the equations on the wiki that define complement.)
We've also already noted that having emptified r, we can take all possible subsets of the heading of r (including the empty subset which is the heading for DUM, DEE), we get another ordering by inclusion, but because these are headings not bodies (there are no tuples), the ordering is in reverse: a smaller heading is the 'higher'/closer towards DUM.
This is again a Boolean algebra, distributive and uniquely (relatively) complemented.
We can also start at r with its body, take all possible subsets of the heading of r (as with emptified r, including the empty subset), project the body of r on to each heading, we get another ordering by inclusion, again in reverse: the smaller the heading is, the 'higher'/closer towards DEE -- and the procedure is bound to generate DEE because we started with non-empty r.
Because this is a Boolean algebra, it's uniquely (relatively) complemented and the double-complement is identity. So project, Remove give us complementary projections of r.

Unfortunately there's no operation (as there is with Matching, NotMatching) to get back to r from complementary project, Remove. The operation ought to be NatJoin, but since deliberately there's no attributes in common, that degenerates to Cartesian product so will in general create fictitious tuples that weren't in the original r.

To build this relational lattice that is a sub-lattice, I didn't need to know the types of the attributes of r, nor what might be all possible tuples for r's heading. So the Boolean algebra sub-lattice from r up to DEE rises 'slantwise' relative to the top face of the overall lattice containing all possible tuples.

It is only when we start examining the individual relation structure (assuming that we are equipped with such means), and then compare the constants from different universes, then we become somewhat confused. For example in "normal" universes, the $R_{00}$ , $R_{01}$ have the empty header, but this property doesn't hold for all universes.

It holds for all relational lattices. I just told you how to construct a sub-'universe' starting from some non-empty relation value.

What do you mean by "different" universes? Just because two relation values within a lattice have different headings (possibly empty heading) doesn't make them significantly different. They must be joinable, at which point they produce 'merged' tuples. Do you want that to be a third 'universe'? Likewise they must support project, Remove, again producing relations with different headings. Do you want that to be a fourth and fifth 'universe'?

The one lattice structure must support the result from all relational operations, otherwise the algebra isn't complete: Codd 1972, TTM RM Pre 18, Pre 6, Pre 7, Appendix A.

I'm also skeptical about the uniqueness concept promoted by Anthony. Consider a general lattice. Is the lattice top and bottom unique (if exist)?

Yes. Proven very quickly by Prover9. Don't you always do that as a sanity check when building a new model? After I've proved the uniqueness of lattice bottom, though, it doesn't seem useful. In particular, it doesn't help find emptified r -- I know that is somewhere 'between' DUM and bottom/within the Boolean algebra of empty relation values, but only DUM is useful in finding it.

Well, yes, but why do we raise this question about only the two operations, that happen to be zilliary ones.

DEE uniqueness is proven very quickly by Prover9. Don't you always do that as a sanity check when building a new model?

Why don't we ask if join and meet are unique?

I do ask. Proven very quickly by Prover9. Don't you always do that as a sanity check when building a new model?

And they don't.

?? Who/which don't what?

I want all operations and constants to be provably unique. Otherwise any claimed equivalence between queries using them is illusory.

TTM Forum

The Forum for Discussion about The Third Manifesto and Related Matters

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