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)

#91 · June 17, 2021, 3:23 am

Quote from AntC on June 17, 2021, 3:23 am

Quote from tobega on June 16, 2021, 8:05 pm

What I mean by lacking 'mental furniture' is your inexplicable unwillingness/inability to follow up links.

"all the math works beautifully" is not true. It might be beautiful, but it doesn't work. Because it's not 'relationally complete'. Go and read that link.

"How do you define "NOT MATCHING" in your model?". Why are you repeatedly asking this? I define as per the links I gave. You give no evidence you've read them. (Or rather, what I model is as per those definitions.)

If you want to argue any of the following are not desiderata, by all means start a new thread to discuss that. I am not going to spoon-feed you any more definitions than I have already:

relationally complete -- including expressing NOT MATCHING and project/REMOVE.

RM Pre 9, 10.

Relation values and headings are sets, including the possibility of being empty sets.

None of you inputs on this thread have been any help whatsoever. If there's something you don't understand, start a new thread asking for explanations. If you have some alternative model, not supporting the desiderata/not conforming to TTM, start a new thread.

Quote from AntC on June 16, 2021, 6:30 am

Quote from tobega on June 16, 2021, 4:48 am

Quote from AntC on June 16, 2021, 2:33 am

Quote from tobega on June 15, 2021, 4:57 am

Quote from AntC on June 14, 2021, 11:55 pm

Quote from tobega on June 14, 2021, 6:44 pm

Thought I'd spend a few more moments on this and the concept of an empty relation seems to be rather elusive

Do you mean "empty relation" as in no tuples? Or as in 'empty heading'?

"empty relation" is an empty set. What's elusive about that? The set of Polar bears in Antarctica. The set of Penguins in Arctica.

There's two relation values with empty heading: one is also empty of tuples (aka DUM); one isn't empty of tuples (aka DEE).

if we just go with some set of elements and the NatJoin and InnerUnion operators.

See 'relationally complete' here; or Appendix A page 7 'Closing Remarks'; or pretty much any text book on relational theory. To be adequate to express all possible queries, you need MINUS or NOT MATCHING or equivalent: then consider r NOT MATCHING r for any r in the set of elements; the given set of elements must include that result. To be adequate to express all possible queries, you need projection or REMOVE/ALL BUT or equivalent: then consider 'Are there any Polar bears in Canada?', 'Are there any Parts in Rome?', etc; note this is not asking to identify the bears or the Parts.

You are absolutely correct concerning the thing you want to model. I am talking about your mathematical model, which by my observations, also models a lot of things we don't want to model. So, unless you put in rules that mandate the existence of the necessary structure, your model will not necessarily reflect what you expect.

I am modelling relations as defined in TTM (particularly RM Pre 9, 10). I expect that to include DUM, DEE: RM Pro 5:

5. D shall not forget that relations with no attributes are respectable and interesting, ...

I haven't "put in rules" over and above TTM Prescriptions. RM Pre 10.b. says the body of a relation is a set. Inevitably that allows a relation with empty body -- unless I "put in rules" to ban that. I expect to model relations with empty body -- for example a relation that identifies all Polar bears in Antarctica.

RM Pre 9. says a heading is a set. Inevitably that allows a relation with empty heading -- unless I "put in rules" to ban that. Furthermore since I have chosen to model using lattice algebra, I must model the value that is Identity for NatJoin -- that is, DEE. Inevitably I must model the relation value with same heading as DEE but empty body -- that is, DUM.

I'm modelling NatJoin is defined in Appendix A 'FORMAL DEFINITIONS` <AND>. I'm modelling NOT MATCHING and other operators as defined in 'HOW Tutorial D BUILDS ON A'.

I'm modelling exactly what I expect. "your model will not necessarily reflect what you expect" is vague and unhelpful waffle. Can you point something specific that is a consequence of my rules but which is not what expected? More hand-waving is not an answer.

If you have InnerUnion, consider REL{TUP{ A a }} InnerUnion REL{TUP{ B b }};: what's the heading for that?

What is the rule that says the model contains either of those two things in the first place? You don't define either tuples or attributes.

(Can we perhaps call these objects "relational lattices"?)

No.

It struck me that most relational lattices don't even contain DUM.

All relational lattices contain DUM. There might be arbitrary sets of relation values that don't contain DUM; you might be able to construct a lattice over them; that's a lattice-of-relations, not a "relational lattice".

Fair enough, I am talking of "lattice-of-relations" then, which is what the model is unless you specify enough structure.

No. A "lattice-of-relations" exhibits more restrictive structure than the TTM model: you'll need to say how/why certain values are excluded (such as those with empty heading). You'll have to identify the identity value for NatJoin, and demonstrate that it is unique.

To illustrate, consider all relations that only have attribute A.

How are you going to build a Supplier-and-Parts database with only a single attribute? Or an Employees-and-Departments database?

Further, restrict that to all relations that contain the tuple where A=a.

Ok let's say Aa := REL{TUP{ A a }}; What's the result of Aa NOT MATCHING Aa?

What's your definition of "NOT MATCHING" in the model? You may obviously not reference anything that hasn't been defined or inferred to exist, like tuples, or DUM.

Actually, we don't even need to add DEE, we have absorption of NatJoin in ({A=a}) and absorption of InnerUnion in the relation containing tuples for all possible values of A.

There are just so many weird sets of elements that fulfil the rules.

What you've described doesn't fulfil the rules.

Depends on the rules. As far as I've seen them detailed,

This thread has made many references to TTM rules, and to Appendix A. If you haven't "seen them detailed" is that because you haven't read those documents, or because you don't understand them? Specifically, this is the TTM forum. I expect all participants to understand TTM -- which is not to say "to agree with" it on all points.

Your mathematical model of TTM will only model exactly what you define with the definitions and logical requirements you put into it.

Yes. It's a model. That's what 'model' means in a mathematical sense.

I see no point in continuing this vacuous discussion.

If you put in too few definitions, your model will reflect not only TTM but also a lot of other things. Logic/mathematics cannot tell that you intended something different or more.

So if you take the set consisting of just DEE, for example,

... then I'm bound to include also DUM. DEE is a non-empty set. The definitions in TTM require also including all possible bodies for that heading. To put it in terms of operations: the result from DEE NOT MATCHING DEE. To put it in terms of lattices: to count as a lattice needs at least two elements; and specifically a bounded lattice needs both a top and bottom, IOW an identity and an absorbing element for the 'meet' operation aka NaturalJoin.

I'm not sure anything of what you're saying here is relevant. What forces you to include DUM? DEE NatJoin DEE is DEE, DEE InnerUnion DEE is DEE, all the math works beautifully. If you do require two elements, have you specified a model rule for that? Even if you have, I have also provided sets of infinite number of elements that do not contain either DEE or DUM as we know them that remain closed under our operations and have both a lattice top and a lattice bottom.

or one of these I have described, which of your rules prohibits that from being the universe of values being considered in the mathematics of your model?

In TTM, the universe of values is very clearly defined. So far I believe you have said that you don't define either attributes or tuples in your model. So what rules introduce the required structure? What rules prohibit your model from also depicting a set (closed under your operations) such as I have described?

I've said all along the lattice structure is modelling TTM-defined relations. The 'rules' of the lattice are lattice rules -- as per wikipedia, for example.

"such as [you] have described" is not coherent -- either as a lattice structure, or as a set of TTM-style relation values. I'd go so far as to say you've failed to describe anything as exhibiting a structure. This isn't a case of 'Neurodiversity'. You seem to lack the mental furniture.

You're right, in this case neurodiversity has nothing to do with it. Your need to resort to ad hominem attacks proves something, and I don't think it's me or my intelligence it reflects poorly on.

Go ahead, try your operations on my proposed sets and everything should just work. And if they don't you should be able to say which rule is contradicted. I'm not sure I have all your definitions taken into account if you've added any beyond NatJoin and InnerUnion.

How do you define "NOT MATCHING" in your model? Once we've established that, we can just perform the operations (within the model) on one of my sets and see what the result is. Without knowing that definition I can only say what we would like it to be, not what it actually is according to the model.

Now the existence of multiple universes of values, even strange ones, is not necessarily a problem, they will still behave the right way and the correct relational universe will also be modelled well enough.

The fact that there is a set of values that work with the model where the value we think of as DEE does not exist is not a problem as long as there exists some element that works like we expect DEE to work. That would still be lattice top (or is it bottom, the choice is really arbitrary).

When the model applies to sets that don't contain DUM, then we can't say that the model contains DUM. Again this is not necessarily a problem if we can find some element that acts like DUM, but the question is how. Have you been able to prove a unique DUM yet?

If you haven't, the following could possibly work: define the function called emptify that distributes over both NatJoin and InnerUnion such that emptify(emptify(A)) = emptify(A). Now state that emptify(DEE) = DUM and DUM != DEE. I don't know if we can say anything more interesting that doesn't already follow from the specified rules.

Quote from tobega on June 16, 2021, 8:05 pm

What I mean by lacking 'mental furniture' is your inexplicable unwillingness/inability to follow up links.

"all the math works beautifully" is not true. It might be beautiful, but it doesn't work. Because it's not 'relationally complete'. Go and read that link.

"How do you define "NOT MATCHING" in your model?". Why are you repeatedly asking this? I define as per the links I gave. You give no evidence you've read them. (Or rather, what I model is as per those definitions.)

If you want to argue any of the following are not desiderata, by all means start a new thread to discuss that. I am not going to spoon-feed you any more definitions than I have already:

relationally complete -- including expressing NOT MATCHING and project/REMOVE.
RM Pre 9, 10.
Relation values and headings are sets, including the possibility of being empty sets.

None of you inputs on this thread have been any help whatsoever. If there's something you don't understand, start a new thread asking for explanations. If you have some alternative model, not supporting the desiderata/not conforming to TTM, start a new thread.

Quote from AntC on June 16, 2021, 6:30 am

Quote from tobega on June 16, 2021, 4:48 am

Quote from AntC on June 16, 2021, 2:33 am

Quote from tobega on June 15, 2021, 4:57 am

Quote from AntC on June 14, 2021, 11:55 pm

Quote from tobega on June 14, 2021, 6:44 pm

Thought I'd spend a few more moments on this and the concept of an empty relation seems to be rather elusive

Do you mean "empty relation" as in no tuples? Or as in 'empty heading'?

"empty relation" is an empty set. What's elusive about that? The set of Polar bears in Antarctica. The set of Penguins in Arctica.

There's two relation values with empty heading: one is also empty of tuples (aka DUM); one isn't empty of tuples (aka DEE).

if we just go with some set of elements and the NatJoin and InnerUnion operators.

See 'relationally complete' here; or Appendix A page 7 'Closing Remarks'; or pretty much any text book on relational theory. To be adequate to express all possible queries, you need MINUS or NOT MATCHING or equivalent: then consider r NOT MATCHING r for any r in the set of elements; the given set of elements must include that result. To be adequate to express all possible queries, you need projection or REMOVE/ALL BUT or equivalent: then consider 'Are there any Polar bears in Canada?', 'Are there any Parts in Rome?', etc; note this is not asking to identify the bears or the Parts.

You are absolutely correct concerning the thing you want to model. I am talking about your mathematical model, which by my observations, also models a lot of things we don't want to model. So, unless you put in rules that mandate the existence of the necessary structure, your model will not necessarily reflect what you expect.

I am modelling relations as defined in TTM (particularly RM Pre 9, 10). I expect that to include DUM, DEE: RM Pro 5:

5. D shall not forget that relations with no attributes are respectable and interesting, ...

I haven't "put in rules" over and above TTM Prescriptions. RM Pre 10.b. says the body of a relation is a set. Inevitably that allows a relation with empty body -- unless I "put in rules" to ban that. I expect to model relations with empty body -- for example a relation that identifies all Polar bears in Antarctica.

RM Pre 9. says a heading is a set. Inevitably that allows a relation with empty heading -- unless I "put in rules" to ban that. Furthermore since I have chosen to model using lattice algebra, I must model the value that is Identity for NatJoin -- that is, DEE. Inevitably I must model the relation value with same heading as DEE but empty body -- that is, DUM.

I'm modelling NatJoin is defined in Appendix A 'FORMAL DEFINITIONS` <AND>. I'm modelling NOT MATCHING and other operators as defined in 'HOW Tutorial D BUILDS ON A'.

I'm modelling exactly what I expect. "your model will not necessarily reflect what you expect" is vague and unhelpful waffle. Can you point something specific that is a consequence of my rules but which is not what expected? More hand-waving is not an answer.

If you have InnerUnion, consider REL{TUP{ A a }} InnerUnion REL{TUP{ B b }};: what's the heading for that?

What is the rule that says the model contains either of those two things in the first place? You don't define either tuples or attributes.

(Can we perhaps call these objects "relational lattices"?)

No.

It struck me that most relational lattices don't even contain DUM.

All relational lattices contain DUM. There might be arbitrary sets of relation values that don't contain DUM; you might be able to construct a lattice over them; that's a lattice-of-relations, not a "relational lattice".

Fair enough, I am talking of "lattice-of-relations" then, which is what the model is unless you specify enough structure.

No. A "lattice-of-relations" exhibits more restrictive structure than the TTM model: you'll need to say how/why certain values are excluded (such as those with empty heading). You'll have to identify the identity value for NatJoin, and demonstrate that it is unique.

To illustrate, consider all relations that only have attribute A.

How are you going to build a Supplier-and-Parts database with only a single attribute? Or an Employees-and-Departments database?

Further, restrict that to all relations that contain the tuple where A=a.

Ok let's say Aa := REL{TUP{ A a }}; What's the result of Aa NOT MATCHING Aa?

What's your definition of "NOT MATCHING" in the model? You may obviously not reference anything that hasn't been defined or inferred to exist, like tuples, or DUM.

Actually, we don't even need to add DEE, we have absorption of NatJoin in ({A=a}) and absorption of InnerUnion in the relation containing tuples for all possible values of A.

There are just so many weird sets of elements that fulfil the rules.

What you've described doesn't fulfil the rules.

Depends on the rules. As far as I've seen them detailed,

This thread has made many references to TTM rules, and to Appendix A. If you haven't "seen them detailed" is that because you haven't read those documents, or because you don't understand them? Specifically, this is the TTM forum. I expect all participants to understand TTM -- which is not to say "to agree with" it on all points.

Your mathematical model of TTM will only model exactly what you define with the definitions and logical requirements you put into it.

Yes. It's a model. That's what 'model' means in a mathematical sense.

I see no point in continuing this vacuous discussion.

If you put in too few definitions, your model will reflect not only TTM but also a lot of other things. Logic/mathematics cannot tell that you intended something different or more.

So if you take the set consisting of just DEE, for example,

... then I'm bound to include also DUM. DEE is a non-empty set. The definitions in TTM require also including all possible bodies for that heading. To put it in terms of operations: the result from DEE NOT MATCHING DEE. To put it in terms of lattices: to count as a lattice needs at least two elements; and specifically a bounded lattice needs both a top and bottom, IOW an identity and an absorbing element for the 'meet' operation aka NaturalJoin.

I'm not sure anything of what you're saying here is relevant. What forces you to include DUM? DEE NatJoin DEE is DEE, DEE InnerUnion DEE is DEE, all the math works beautifully. If you do require two elements, have you specified a model rule for that? Even if you have, I have also provided sets of infinite number of elements that do not contain either DEE or DUM as we know them that remain closed under our operations and have both a lattice top and a lattice bottom.

or one of these I have described, which of your rules prohibits that from being the universe of values being considered in the mathematics of your model?

In TTM, the universe of values is very clearly defined. So far I believe you have said that you don't define either attributes or tuples in your model. So what rules introduce the required structure? What rules prohibit your model from also depicting a set (closed under your operations) such as I have described?

I've said all along the lattice structure is modelling TTM-defined relations. The 'rules' of the lattice are lattice rules -- as per wikipedia, for example.

"such as [you] have described" is not coherent -- either as a lattice structure, or as a set of TTM-style relation values. I'd go so far as to say you've failed to describe anything as exhibiting a structure. This isn't a case of 'Neurodiversity'. You seem to lack the mental furniture.

You're right, in this case neurodiversity has nothing to do with it. Your need to resort to ad hominem attacks proves something, and I don't think it's me or my intelligence it reflects poorly on.

Go ahead, try your operations on my proposed sets and everything should just work. And if they don't you should be able to say which rule is contradicted. I'm not sure I have all your definitions taken into account if you've added any beyond NatJoin and InnerUnion.

How do you define "NOT MATCHING" in your model? Once we've established that, we can just perform the operations (within the model) on one of my sets and see what the result is. Without knowing that definition I can only say what we would like it to be, not what it actually is according to the model.

Now the existence of multiple universes of values, even strange ones, is not necessarily a problem, they will still behave the right way and the correct relational universe will also be modelled well enough.

The fact that there is a set of values that work with the model where the value we think of as DEE does not exist is not a problem as long as there exists some element that works like we expect DEE to work. That would still be lattice top (or is it bottom, the choice is really arbitrary).

When the model applies to sets that don't contain DUM, then we can't say that the model contains DUM. Again this is not necessarily a problem if we can find some element that acts like DUM, but the question is how. Have you been able to prove a unique DUM yet?

If you haven't, the following could possibly work: define the function called emptify that distributes over both NatJoin and InnerUnion such that emptify(emptify(A)) = emptify(A). Now state that emptify(DEE) = DUM and DUM != DEE. I don't know if we can say anything more interesting that doesn't already follow from the specified rules.

#92 · June 17, 2021, 11:01 am

Quote from tobega on June 17, 2021, 11:01 am

Quote from AntC on June 17, 2021, 3:23 am

Quote from tobega on June 16, 2021, 8:05 pm

What I mean by lacking 'mental furniture' is your inexplicable unwillingness/inability to follow up links.

"all the math works beautifully" is not true. It might be beautiful, but it doesn't work. Because it's not 'relationally complete'. Go and read that link.

I can certainly do so, but I fail to see what significance that has with regards to your model? What definitions in your model guarantee that the set of values is relationally complete? I only want to use the logic propositions that govern your model.

"How do you define "NOT MATCHING" in your model?". Why are you repeatedly asking this? I define as per the links I gave. You give no evidence you've read them. (Or rather, what I model is as per those definitions.)

If you want to argue any of the following are not desiderata, by all means start a new thread to discuss that. I am not going to spoon-feed you any more definitions than I have already:

relationally complete -- including expressing NOT MATCHING and project/REMOVE.

RM Pre 9, 10.

Relation values and headings are sets, including the possibility of being empty sets.

None of you inputs on this thread have been any help whatsoever. If there's something you don't understand, start a new thread asking for explanations. If you have some alternative model, not supporting the desiderata/not conforming to TTM, start a new thread.

Sorry that I couldn't be of any help because I think you're onto something interesting and have made a brilliant start. IIRC you were the one asking for criticism?

If you set up a model, then, in mathematics, I can choose whatever I wish to apply it to, as long as it follows the rules of the model (expressed as cold hard logic, not some wishful thinking about implied relationship with TTM or relational algebra in general)

In your model, I assume you have a definition for "NOT MATCHING" in terms of NatJoin and/or InnerUnion? Supply that definition and I can apply those operations to one of my universes of values and see what happens. (and, of course, the definition of "NOT MATCHING" in TTM cannot be applied directly in your model, so it is in this case not relevant)

FWIW, I did think of a possible further criterion to capture the concept of emptiness (if it doesn't already follow from given criteria): emptify(R1) NatJoin R2 = emptify(R1 NatJoin R2). I suppose there could be something for InnerUnion as well, perhaps emptify(R1) InnerUnion R2 = emptify(R1 InnerUnion R2) InnerUnion R2

Quote from AntC on June 17, 2021, 3:23 am

Quote from tobega on June 16, 2021, 8:05 pm

What I mean by lacking 'mental furniture' is your inexplicable unwillingness/inability to follow up links.

"all the math works beautifully" is not true. It might be beautiful, but it doesn't work. Because it's not 'relationally complete'. Go and read that link.

I can certainly do so, but I fail to see what significance that has with regards to your model? What definitions in your model guarantee that the set of values is relationally complete? I only want to use the logic propositions that govern your model.

"How do you define "NOT MATCHING" in your model?". Why are you repeatedly asking this? I define as per the links I gave. You give no evidence you've read them. (Or rather, what I model is as per those definitions.)

If you want to argue any of the following are not desiderata, by all means start a new thread to discuss that. I am not going to spoon-feed you any more definitions than I have already:

relationally complete -- including expressing NOT MATCHING and project/REMOVE.

RM Pre 9, 10.

Relation values and headings are sets, including the possibility of being empty sets.

None of you inputs on this thread have been any help whatsoever. If there's something you don't understand, start a new thread asking for explanations. If you have some alternative model, not supporting the desiderata/not conforming to TTM, start a new thread.

Sorry that I couldn't be of any help because I think you're onto something interesting and have made a brilliant start. IIRC you were the one asking for criticism?

If you set up a model, then, in mathematics, I can choose whatever I wish to apply it to, as long as it follows the rules of the model (expressed as cold hard logic, not some wishful thinking about implied relationship with TTM or relational algebra in general)

In your model, I assume you have a definition for "NOT MATCHING" in terms of NatJoin and/or InnerUnion? Supply that definition and I can apply those operations to one of my universes of values and see what happens. (and, of course, the definition of "NOT MATCHING" in TTM cannot be applied directly in your model, so it is in this case not relevant)

FWIW, I did think of a possible further criterion to capture the concept of emptiness (if it doesn't already follow from given criteria): emptify(R1) NatJoin R2 = emptify(R1 NatJoin R2). I suppose there could be something for InnerUnion as well, perhaps emptify(R1) InnerUnion R2 = emptify(R1 InnerUnion R2) InnerUnion R2

#93 · June 17, 2021, 6:11 pm

I think my thinking on this matter has finally become complete. The model based on the operations InnerUnion that provides the least upper bound of its operands and NatJoin that provides the greatest lower bound of its operands is very interesting and aesthetically appealing. The greatest element is that which we know as DEE and the smallest has been named DUMPTY. In my explorations I have repeatedly expressed the concern that the model doesn't capture enough structure to fully represent a relationally complete model. I now believe that the essential part it lacks is a definition of emptiness. I also now feel fairly certain that enough structure can be put into the model by an appropriate definition of the "emptify" function that Anthony has discovered as crucial in expressing other relational operators.

emptify(DUMPTY) = DUMPTY
emptify(DEE) != DEE
emptify(emptify(R)) = emptify(R) for all R
emptify(R1) NatJoin R2 = emptify(R1 NatJoin R2) for all R1, R2
emptify(R1) InnerUnion R2 = emptify(R1 InnerUnion R2) InnerUnion R2 for all R1, R2

#94 · June 17, 2021, 8:33 pm

Quote from Vadim on June 17, 2021, 8:33 pm

Quote from tobega on June 17, 2021, 6:11 pm

I think my thinking on this matter has finally become complete. The model based on the operations InnerUnion that provides the least upper bound of its operands and NatJoin that provides the greatest lower bound of its operands is very interesting and aesthetically appealing. The greatest element is that which we know as DEE and the smallest has been named DUMPTY. In my explorations I have repeatedly expressed the concern that the model doesn't capture enough structure to fully represent a relationally complete model. I now believe that the essential part it lacks is a definition of emptiness. I also now feel fairly certain that enough structure can be put into the model by an appropriate definition of the "emptify" function that Anthony has discovered as crucial in expressing other relational operators.

emptify(DUMPTY) = DUMPTY

emptify(DEE) != DEE

emptify(emptify(R)) = emptify(R) for all R

emptify(R1) NatJoin R2 = emptify(R1 NatJoin R2) for all R1, R2

emptify(R1) InnerUnion R2 = emptify(R1 InnerUnion R2) InnerUnion R2 for all R1, R2

Those are just simple theorems in more basic algebraic signature:

1.
2 emptify(R01) = R01 # label(non_clause) # label(goal).  [goal].
3 x ^ y = y ^ x.  [assumption].
10 emptify(x) = R00 ^ x.  [assumption].
11 R01 = R01 ^ x.  [assumption].
12 R01 ^ x = R01.  [copy(11),flip(a)].
13 emptify(R01) != R01.  [deny(2)].
14 R00 ^ R01 != R01.  [copy(13),rewrite([10(2)])].
35 x ^ R01 = R01.  [para(12(a,1),3(a,1)),flip(a)].
36 $F.  [resolve(35,a,14,a)].
2. Debatable constraint

3.
2 emptify(emptify(R)) = emptify(R) # label(non_clause) # label(goal).  [goal].
4 (x ^ y) ^ z = x ^ (y ^ z).  [assumption].
5 x ^ (x v y) = x.  [assumption].
8 x v (x ^ y) = x.  [assumption].
10 emptify(x) = R00 ^ x.  [assumption].
13 emptify(emptify(R)) != emptify(R).  [deny(2)].
14 R00 ^ (R00 ^ R) != R00 ^ R.  [copy(13),rewrite([10(2),10(4),10(7)])].
25 x ^ x = x.  [para(8(a,1),5(a,1,2))].
38 x ^ (x ^ y) = x ^ y.  [para(25(a,1),4(a,1,1)),flip(a)].
39 $F.  [resolve(38,a,14,a)].
4.
2 emptify(R1) ^ R2 = emptify(R1 ^ R2) # label(non_clause) # label(goal).  [goal].
3 x ^ y = y ^ x.  [assumption].
4 (x ^ y) ^ z = x ^ (y ^ z).  [assumption].
10 emptify(x) = R00 ^ x.  [assumption].
13 emptify(R1 ^ R2) != emptify(R1) ^ R2.  [deny(2)].
14 R2 ^ (R00 ^ R1) != R00 ^ (R1 ^ R2).  [copy(13),rewrite([10(4),10(7),3(10)]),flip(a)].
15 x ^ (y ^ z) = z ^ (x ^ y).  [para(4(a,1),3(a,1))].
16 $F.  [resolve(15,a,14,a(flip))].
5.
1 R00 ^ (x v y) = R00 ^ (x v z) -> x ^ (y v z) = (x ^ y) v (x ^ z) # label(non_clause).  [assumption].
2 emptify(R1) v R2 = emptify(R1 v R2) v R2 # label(non_clause) # label(goal).  [goal].
3 x ^ y = y ^ x.  [assumption].
4 (x ^ y) ^ z = x ^ (y ^ z).  [assumption].
5 x ^ (x v y) = x.  [assumption].
6 x v y = y v x.  [assumption].
7 (x v y) v z = x v (y v z).  [assumption].
8 x v (x ^ y) = x.  [assumption].
9 R00 ^ (x v y) != R00 ^ (x v z) | (x ^ z) v (x ^ y) = x ^ (z v y).  [clausify(1)].
10 emptify(x) = R00 ^ x.  [assumption].
13 emptify(R1 v R2) v R2 != emptify(R1) v R2.  [deny(2)].
14 R2 v (R00 ^ (R1 v R2)) != R2 v (R00 ^ R1).  [copy(13),rewrite([10(4),6(7),10(9),6(12)])].
23 x v (y ^ x) = x.  [para(3(a,1),8(a,1,2))].
29 (R00 ^ x) v (R00 ^ y) = R00 ^ (x v y).  [para(5(a,1),9(a,1)),rewrite([5(5)]),xx(a)].
58 x v (y ^ (z ^ x)) = x.  [para(4(a,1),23(a,1,2))].
108 x v (y v (z ^ x)) = x v y.  [para(5(a,1),58(a,1,2,2)),rewrite([7(3)])].
341 x v (R00 ^ (y v x)) = x v (R00 ^ y).  [para(29(a,1),108(a,1,2))].
342 $F.  [resolve(341,a,14,a)].
Again, when you complicate algebraic signature (binary REMOVE vs. unary attribute complement, unary EMPTIFY vs. zeroary R00), you compromise your progress, not advance it.

Quote from tobega on June 17, 2021, 6:11 pm

I think my thinking on this matter has finally become complete. The model based on the operations InnerUnion that provides the least upper bound of its operands and NatJoin that provides the greatest lower bound of its operands is very interesting and aesthetically appealing. The greatest element is that which we know as DEE and the smallest has been named DUMPTY. In my explorations I have repeatedly expressed the concern that the model doesn't capture enough structure to fully represent a relationally complete model. I now believe that the essential part it lacks is a definition of emptiness. I also now feel fairly certain that enough structure can be put into the model by an appropriate definition of the "emptify" function that Anthony has discovered as crucial in expressing other relational operators.

emptify(DUMPTY) = DUMPTY

emptify(DEE) != DEE

emptify(emptify(R)) = emptify(R) for all R

emptify(R1) NatJoin R2 = emptify(R1 NatJoin R2) for all R1, R2

emptify(R1) InnerUnion R2 = emptify(R1 InnerUnion R2) InnerUnion R2 for all R1, R2

Those are just simple theorems in more basic algebraic signature:

2 emptify(R01) = R01 # label(non_clause) # label(goal).  [goal].
3 x ^ y = y ^ x.  [assumption].
10 emptify(x) = R00 ^ x.  [assumption].
11 R01 = R01 ^ x.  [assumption].
12 R01 ^ x = R01.  [copy(11),flip(a)].
13 emptify(R01) != R01.  [deny(2)].
14 R00 ^ R01 != R01.  [copy(13),rewrite([10(2)])].
35 x ^ R01 = R01.  [para(12(a,1),3(a,1)),flip(a)].
36 $F.  [resolve(35,a,14,a)].

2. Debatable constraint

2 emptify(emptify(R)) = emptify(R) # label(non_clause) # label(goal).  [goal].
4 (x ^ y) ^ z = x ^ (y ^ z).  [assumption].
5 x ^ (x v y) = x.  [assumption].
8 x v (x ^ y) = x.  [assumption].
10 emptify(x) = R00 ^ x.  [assumption].
13 emptify(emptify(R)) != emptify(R).  [deny(2)].
14 R00 ^ (R00 ^ R) != R00 ^ R.  [copy(13),rewrite([10(2),10(4),10(7)])].
25 x ^ x = x.  [para(8(a,1),5(a,1,2))].
38 x ^ (x ^ y) = x ^ y.  [para(25(a,1),4(a,1,1)),flip(a)].
39 $F.  [resolve(38,a,14,a)].

2 emptify(R1) ^ R2 = emptify(R1 ^ R2) # label(non_clause) # label(goal).  [goal].
3 x ^ y = y ^ x.  [assumption].
4 (x ^ y) ^ z = x ^ (y ^ z).  [assumption].
10 emptify(x) = R00 ^ x.  [assumption].
13 emptify(R1 ^ R2) != emptify(R1) ^ R2.  [deny(2)].
14 R2 ^ (R00 ^ R1) != R00 ^ (R1 ^ R2).  [copy(13),rewrite([10(4),10(7),3(10)]),flip(a)].
15 x ^ (y ^ z) = z ^ (x ^ y).  [para(4(a,1),3(a,1))].
16 $F.  [resolve(15,a,14,a(flip))].

1 R00 ^ (x v y) = R00 ^ (x v z) -> x ^ (y v z) = (x ^ y) v (x ^ z) # label(non_clause).  [assumption].
2 emptify(R1) v R2 = emptify(R1 v R2) v R2 # label(non_clause) # label(goal).  [goal].
3 x ^ y = y ^ x.  [assumption].
4 (x ^ y) ^ z = x ^ (y ^ z).  [assumption].
5 x ^ (x v y) = x.  [assumption].
6 x v y = y v x.  [assumption].
7 (x v y) v z = x v (y v z).  [assumption].
8 x v (x ^ y) = x.  [assumption].
9 R00 ^ (x v y) != R00 ^ (x v z) | (x ^ z) v (x ^ y) = x ^ (z v y).  [clausify(1)].
10 emptify(x) = R00 ^ x.  [assumption].
13 emptify(R1 v R2) v R2 != emptify(R1) v R2.  [deny(2)].
14 R2 v (R00 ^ (R1 v R2)) != R2 v (R00 ^ R1).  [copy(13),rewrite([10(4),6(7),10(9),6(12)])].
23 x v (y ^ x) = x.  [para(3(a,1),8(a,1,2))].
29 (R00 ^ x) v (R00 ^ y) = R00 ^ (x v y).  [para(5(a,1),9(a,1)),rewrite([5(5)]),xx(a)].
58 x v (y ^ (z ^ x)) = x.  [para(4(a,1),23(a,1,2))].
108 x v (y v (z ^ x)) = x v y.  [para(5(a,1),58(a,1,2,2)),rewrite([7(3)])].
341 x v (R00 ^ (y v x)) = x v (R00 ^ y).  [para(29(a,1),108(a,1,2))].
342 $F.  [resolve(341,a,14,a)].

Again, when you complicate algebraic signature (binary REMOVE vs. unary attribute complement, unary EMPTIFY vs. zeroary R00), you compromise your progress, not advance it.

#95 · June 18, 2021, 2:39 am

Quote from AntC on June 18, 2021, 2:39 am

Quote from Vadim on June 17, 2021, 8:33 pm

Quote from tobega on June 17, 2021, 6:11 pm

I think my thinking on this matter has finally become complete. The model based on the operations InnerUnion that provides the least upper bound of its operands and NatJoin that provides the greatest lower bound of its operands is very interesting and aesthetically appealing. The greatest element is that which we know as DEE and the smallest has been named DUMPTY. In my explorations I have repeatedly expressed the concern that the model doesn't capture enough structure to fully represent a relationally complete model. I now believe that the essential part it lacks is a definition of emptiness. I also now feel fairly certain that enough structure can be put into the model by an appropriate definition of the "emptify" function that Anthony has discovered as crucial in expressing other relational operators.

emptify(DUMPTY) = DUMPTY

emptify(DEE) != DEE

emptify(emptify(R)) = emptify(R) for all R

emptify(R1) NatJoin R2 = emptify(R1 NatJoin R2) for all R1, R2

emptify(R1) InnerUnion R2 = emptify(R1 InnerUnion R2) InnerUnion R2 for all R1, R2

Those are just simple theorems in more basic algebraic signature:

Hi Vadim, your demo doesn't look right to me. DUMPTY is the relation with all atributes, empty body. That's your R10. Your demo 1 uses R01 -- that's DEE; and emptify(R01) = R01 is not a theorem for DEE, in fact it's always false.

Your demos 3, 4, 5 use uppercase R, R1, R2; so that's skolems/existentially quantified, whereas @tobega's axioms require forall quantified.

For @tobega's benefit: Vadim has taken emptify( ) not to be a primitive. Rather he has:

emptify( r ) =df DUM NatJoin r for all r. So we get

DUM = emptify( DEE ); as a consequence (of DEE being the identity for NatJoin).

This is no help unless we can fix a definition for DUM aka Vadim's R00. And so far nobody's found such a definition.

Again, when you complicate algebraic signature (binary REMOVE vs. unary attribute complement, unary EMPTIFY vs. zeroary R00), you compromise your progress, not advance it.

If you could demonstrate a fixed definition for unary attribute complement, then we could make progress. But you haven't. (I've tried quite hard.) Taking unary complements is as far as I can see, no advance.

BTW I don't see why Vadim describes axiom 2 as "Debatable". In what possible relational lattice could DUM NatJoin DEE be DEE? Only if DUM = DEE. But that would have to be a lattice system with only that single element. That's so degenerate, all the theorists I have come across say it's not a lattice at all.

Quote from Vadim on June 17, 2021, 8:33 pm

Quote from tobega on June 17, 2021, 6:11 pm

I think my thinking on this matter has finally become complete. The model based on the operations InnerUnion that provides the least upper bound of its operands and NatJoin that provides the greatest lower bound of its operands is very interesting and aesthetically appealing. The greatest element is that which we know as DEE and the smallest has been named DUMPTY. In my explorations I have repeatedly expressed the concern that the model doesn't capture enough structure to fully represent a relationally complete model. I now believe that the essential part it lacks is a definition of emptiness. I also now feel fairly certain that enough structure can be put into the model by an appropriate definition of the "emptify" function that Anthony has discovered as crucial in expressing other relational operators.

emptify(DUMPTY) = DUMPTY

emptify(DEE) != DEE

emptify(emptify(R)) = emptify(R) for all R

emptify(R1) NatJoin R2 = emptify(R1 NatJoin R2) for all R1, R2

emptify(R1) InnerUnion R2 = emptify(R1 InnerUnion R2) InnerUnion R2 for all R1, R2

Those are just simple theorems in more basic algebraic signature:

Hi Vadim, your demo doesn't look right to me. DUMPTY is the relation with all atributes, empty body. That's your R10. Your demo 1 uses R01 -- that's DEE; and emptify(R01) = R01 is not a theorem for DEE, in fact it's always false.

Your demos 3, 4, 5 use uppercase R, R1, R2; so that's skolems/existentially quantified, whereas @tobega's axioms require forall quantified.

For @tobega's benefit: Vadim has taken emptify( ) not to be a primitive. Rather he has:

emptify( r ) =df DUM NatJoin r for all r. So we get
DUM = emptify( DEE ); as a consequence (of DEE being the identity for NatJoin).

This is no help unless we can fix a definition for DUM aka Vadim's R00. And so far nobody's found such a definition.

Again, when you complicate algebraic signature (binary REMOVE vs. unary attribute complement, unary EMPTIFY vs. zeroary R00), you compromise your progress, not advance it.

If you could demonstrate a fixed definition for unary attribute complement, then we could make progress. But you haven't. (I've tried quite hard.) Taking unary complements is as far as I can see, no advance.

BTW I don't see why Vadim describes axiom 2 as "Debatable". In what possible relational lattice could DUM NatJoin DEE be DEE? Only if DUM = DEE. But that would have to be a lattice system with only that single element. That's so degenerate, all the theorists I have come across say it's not a lattice at all.

#96 · June 18, 2021, 2:50 am

Quote from AntC on June 18, 2021, 2:50 am

Quote from tobega on June 17, 2021, 6:11 pm

I think my thinking on this matter has finally become complete. The model based on the operations InnerUnion that provides the least upper bound of its operands and NatJoin that provides the greatest lower bound of its operands is very interesting and aesthetically appealing. The greatest element is that which we know as DEE and the smallest has been named DUMPTY. In my explorations I have repeatedly expressed the concern that the model doesn't capture enough structure to fully represent a relationally complete model. I now believe that the essential part it lacks is a definition of emptiness.

You can take emptify( ) as primitive and define DUM in terms of it (see my reply to Vadim); or you can take DUM as primitive and define emptify( ) in terms of it. They're equivalent. And they're also equivalent in that there's no set of axioms sufficient to fix DUM/emptify( ) unambiguously. Therefore any attempt to prove equivalence of queries using one of those fails.

I also now feel fairly certain that enough structure can be put into the model by an appropriate definition of the "emptify" function that Anthony has discovered as crucial in expressing other relational operators.

No your axioms below don't put in "enough structure". Your axioms can be fairly trivially derived from more powerful axioms -- as Vadim demonstrates. Those more powerful axioms are not powerful enough to demonstrate emptify( )'s definition is unique.

The formal process to demonstrate that: set up a parallel definition emptify2( ) using your same axioms. Then ask the prover to derive emptify( r ) = emptify2( r ) for all r. It can't. For full disclosure: neither can it show emptify( r ) ≠ emptify2( r ) for all r -- you have a typical undecidable proposition. Having to hand a proof of the Collatz Conjecture would help.

emptify(DUMPTY) = DUMPTY

emptify(DEE) != DEE

emptify(emptify(R)) = emptify(R) for all R

emptify(R1) NatJoin R2 = emptify(R1 NatJoin R2) for all R1, R2

emptify(R1) InnerUnion R2 = emptify(R1 InnerUnion R2) InnerUnion R2 for all R1, R2

Quote from tobega on June 17, 2021, 6:11 pm

I think my thinking on this matter has finally become complete. The model based on the operations InnerUnion that provides the least upper bound of its operands and NatJoin that provides the greatest lower bound of its operands is very interesting and aesthetically appealing. The greatest element is that which we know as DEE and the smallest has been named DUMPTY. In my explorations I have repeatedly expressed the concern that the model doesn't capture enough structure to fully represent a relationally complete model. I now believe that the essential part it lacks is a definition of emptiness.

You can take emptify( ) as primitive and define DUM in terms of it (see my reply to Vadim); or you can take DUM as primitive and define emptify( ) in terms of it. They're equivalent. And they're also equivalent in that there's no set of axioms sufficient to fix DUM/emptify( ) unambiguously. Therefore any attempt to prove equivalence of queries using one of those fails.

I also now feel fairly certain that enough structure can be put into the model by an appropriate definition of the "emptify" function that Anthony has discovered as crucial in expressing other relational operators.

No your axioms below don't put in "enough structure". Your axioms can be fairly trivially derived from more powerful axioms -- as Vadim demonstrates. Those more powerful axioms are not powerful enough to demonstrate emptify( )'s definition is unique.

The formal process to demonstrate that: set up a parallel definition emptify2( ) using your same axioms. Then ask the prover to derive emptify( r ) = emptify2( r ) for all r. It can't. For full disclosure: neither can it show emptify( r ) ≠ emptify2( r ) for all r -- you have a typical undecidable proposition. Having to hand a proof of the Collatz Conjecture would help.

emptify(DUMPTY) = DUMPTY

emptify(DEE) != DEE

emptify(emptify(R)) = emptify(R) for all R

emptify(R1) NatJoin R2 = emptify(R1 NatJoin R2) for all R1, R2

emptify(R1) InnerUnion R2 = emptify(R1 InnerUnion R2) InnerUnion R2 for all R1, R2

#97 · June 18, 2021, 2:58 am

Quote from tobega on June 17, 2021, 11:01 am

Quote from AntC on June 17, 2021, 3:23 am

Quote from tobega on June 16, 2021, 8:05 pm

What I mean by lacking 'mental furniture' is your inexplicable unwillingness/inability to follow up links.

"all the math works beautifully" is not true. It might be beautiful, but it doesn't work. Because it's not 'relationally complete'. Go and read that link.

I can certainly do so,

But you haven't. What's wrong with you?

but I fail to see what significance that has with regards to your model?

You have failed to read something, so arguing from a position of ignorance, you fail to see the significance. Go and read it. This correspondence is closed until you do.

Sorry that I couldn't be of any help because I think you're onto something interesting and have made a brilliant start. IIRC you were the one asking for criticism?

I asked for 'critique'. So far from you I've seen comments from a deep pool of ignorance/arising from some weird refusal to read up on the subject matter. All your 'criticisms' have been null and void because of your ignorance.

#98 · June 18, 2021, 4:26 am

Quote from AntC on June 18, 2021, 2:58 am

Quote from tobega on June 17, 2021, 11:01 am

Quote from AntC on June 17, 2021, 3:23 am

Quote from tobega on June 16, 2021, 8:05 pm

What I mean by lacking 'mental furniture' is your inexplicable unwillingness/inability to follow up links.

"all the math works beautifully" is not true. It might be beautiful, but it doesn't work. Because it's not 'relationally complete'. Go and read that link.

I can certainly do so,

But you haven't. What's wrong with you?

Of course I have read it. I just fail to see what in it is relevant to your model? It just pertains to that which you WISH to model, not the model itself. I have no problem with what you would like to model.

#99 · June 18, 2021, 4:46 am

Quote from tobega on June 18, 2021, 4:46 am

Quote from AntC on June 18, 2021, 2:50 am

Quote from tobega on June 17, 2021, 6:11 pm

I think my thinking on this matter has finally become complete. The model based on the operations InnerUnion that provides the least upper bound of its operands and NatJoin that provides the greatest lower bound of its operands is very interesting and aesthetically appealing. The greatest element is that which we know as DEE and the smallest has been named DUMPTY. In my explorations I have repeatedly expressed the concern that the model doesn't capture enough structure to fully represent a relationally complete model. I now believe that the essential part it lacks is a definition of emptiness.

You can take emptify( ) as primitive and define DUM in terms of it (see my reply to Vadim); or you can take DUM as primitive and define emptify( ) in terms of it. They're equivalent. And they're also equivalent in that there's no set of axioms sufficient to fix DUM/emptify( ) unambiguously. Therefore any attempt to prove equivalence of queries using one of those fails.

I also now feel fairly certain that enough structure can be put into the model by an appropriate definition of the "emptify" function that Anthony has discovered as crucial in expressing other relational operators.

No your axioms below don't put in "enough structure". Your axioms can be fairly trivially derived from more powerful axioms -- as Vadim demonstrates. Those more powerful axioms are not powerful enough to demonstrate emptify( )'s definition is unique.

Ah, that's too bad. My definitions would indeed (apart from number 2) also apply to the identity function, so I'm not entirely surprised that there is still ambiguity.

Then in my opinion you need to do more to define the structure of empty vs not empty, since it is the fundamental difference of true vs false. The empties themselves form a lattice, but in it only the header-affecting part of the operations is in play. So how to define that as being part of the full lattice? Another tack could be to start from DEE + DUM, so you have true/false already at the core, and work out how to represent the attribute extensions I've talked about earlier.

Quote from AntC on June 18, 2021, 2:50 am

Quote from tobega on June 17, 2021, 6:11 pm

I think my thinking on this matter has finally become complete. The model based on the operations InnerUnion that provides the least upper bound of its operands and NatJoin that provides the greatest lower bound of its operands is very interesting and aesthetically appealing. The greatest element is that which we know as DEE and the smallest has been named DUMPTY. In my explorations I have repeatedly expressed the concern that the model doesn't capture enough structure to fully represent a relationally complete model. I now believe that the essential part it lacks is a definition of emptiness.

You can take emptify( ) as primitive and define DUM in terms of it (see my reply to Vadim); or you can take DUM as primitive and define emptify( ) in terms of it. They're equivalent. And they're also equivalent in that there's no set of axioms sufficient to fix DUM/emptify( ) unambiguously. Therefore any attempt to prove equivalence of queries using one of those fails.

I also now feel fairly certain that enough structure can be put into the model by an appropriate definition of the "emptify" function that Anthony has discovered as crucial in expressing other relational operators.

No your axioms below don't put in "enough structure". Your axioms can be fairly trivially derived from more powerful axioms -- as Vadim demonstrates. Those more powerful axioms are not powerful enough to demonstrate emptify( )'s definition is unique.

Ah, that's too bad. My definitions would indeed (apart from number 2) also apply to the identity function, so I'm not entirely surprised that there is still ambiguity.

Then in my opinion you need to do more to define the structure of empty vs not empty, since it is the fundamental difference of true vs false. The empties themselves form a lattice, but in it only the header-affecting part of the operations is in play. So how to define that as being part of the full lattice? Another tack could be to start from DEE + DUM, so you have true/false already at the core, and work out how to represent the attribute extensions I've talked about earlier.

#100 · June 18, 2021, 4:56 am

Quote from tobega on June 18, 2021, 4:56 am

Quote from AntC on June 18, 2021, 2:39 am

Quote from Vadim on June 17, 2021, 8:33 pm

Quote from tobega on June 17, 2021, 6:11 pm

I think my thinking on this matter has finally become complete. The model based on the operations InnerUnion that provides the least upper bound of its operands and NatJoin that provides the greatest lower bound of its operands is very interesting and aesthetically appealing. The greatest element is that which we know as DEE and the smallest has been named DUMPTY. In my explorations I have repeatedly expressed the concern that the model doesn't capture enough structure to fully represent a relationally complete model. I now believe that the essential part it lacks is a definition of emptiness. I also now feel fairly certain that enough structure can be put into the model by an appropriate definition of the "emptify" function that Anthony has discovered as crucial in expressing other relational operators.

emptify(DUMPTY) = DUMPTY

emptify(DEE) != DEE

emptify(emptify(R)) = emptify(R) for all R

emptify(R1) NatJoin R2 = emptify(R1 NatJoin R2) for all R1, R2

emptify(R1) InnerUnion R2 = emptify(R1 InnerUnion R2) InnerUnion R2 for all R1, R2

Those are just simple theorems in more basic algebraic signature:

Hi Vadim, your demo doesn't look right to me. DUMPTY is the relation with all atributes, empty body. That's your R10. Your demo 1 uses R01 -- that's DEE; and emptify(R01) = R01 is not a theorem for DEE, in fact it's always false.

Your demos 3, 4, 5 use uppercase R, R1, R2; so that's skolems/existentially quantified, whereas @tobega's axioms require forall quantified.

For @tobega's benefit: Vadim has taken emptify( ) not to be a primitive. Rather he has:

emptify( r ) =df DUM NatJoin r for all r. So we get

DUM = emptify( DEE ); as a consequence (of DEE being the identity for NatJoin).

This is no help unless we can fix a definition for DUM aka Vadim's R00. And so far nobody's found such a definition.

Again, when you complicate algebraic signature (binary REMOVE vs. unary attribute complement, unary EMPTIFY vs. zeroary R00), you compromise your progress, not advance it.

If you could demonstrate a fixed definition for unary attribute complement, then we could make progress. But you haven't. (I've tried quite hard.) Taking unary complements is as far as I can see, no advance.

BTW I don't see why Vadim describes axiom 2 as "Debatable". In what possible relational lattice could DUM NatJoin DEE be DEE? Only if DUM = DEE. But that would have to be a lattice system with only that single element. That's so degenerate, all the theorists I have come across say it's not a lattice at all.

It could be debatable. As long as the ability to also represent degenerate systems doesn't compromise the correctness of the model for the desired case, you can run with it. That also lies behind Vadim's idea that you may not need to prove uniqueness as long as all the variants give the same (regarding logical structure, homomorphically) logical result.

So it may be possible that you can just say "there exists a DUM" and just run with it. Although I wouldn't entirely trust that model.

If you are interested, I could do manual calculations on a degenerate system such as I have proposed and show how an element that is not DUM still can act as such in the degenerate system and give results that probably make some sort of sense. Which is why I have asked you for your definition of "NOT MATCHING".

Quote from AntC on June 18, 2021, 2:39 am

Quote from Vadim on June 17, 2021, 8:33 pm

Quote from tobega on June 17, 2021, 6:11 pm

I think my thinking on this matter has finally become complete. The model based on the operations InnerUnion that provides the least upper bound of its operands and NatJoin that provides the greatest lower bound of its operands is very interesting and aesthetically appealing. The greatest element is that which we know as DEE and the smallest has been named DUMPTY. In my explorations I have repeatedly expressed the concern that the model doesn't capture enough structure to fully represent a relationally complete model. I now believe that the essential part it lacks is a definition of emptiness. I also now feel fairly certain that enough structure can be put into the model by an appropriate definition of the "emptify" function that Anthony has discovered as crucial in expressing other relational operators.

emptify(DUMPTY) = DUMPTY

emptify(DEE) != DEE

emptify(emptify(R)) = emptify(R) for all R

emptify(R1) NatJoin R2 = emptify(R1 NatJoin R2) for all R1, R2

emptify(R1) InnerUnion R2 = emptify(R1 InnerUnion R2) InnerUnion R2 for all R1, R2

Those are just simple theorems in more basic algebraic signature:

Hi Vadim, your demo doesn't look right to me. DUMPTY is the relation with all atributes, empty body. That's your R10. Your demo 1 uses R01 -- that's DEE; and emptify(R01) = R01 is not a theorem for DEE, in fact it's always false.

Your demos 3, 4, 5 use uppercase R, R1, R2; so that's skolems/existentially quantified, whereas @tobega's axioms require forall quantified.

For @tobega's benefit: Vadim has taken emptify( ) not to be a primitive. Rather he has:

emptify( r ) =df DUM NatJoin r for all r. So we get

DUM = emptify( DEE ); as a consequence (of DEE being the identity for NatJoin).

This is no help unless we can fix a definition for DUM aka Vadim's R00. And so far nobody's found such a definition.

Again, when you complicate algebraic signature (binary REMOVE vs. unary attribute complement, unary EMPTIFY vs. zeroary R00), you compromise your progress, not advance it.

If you could demonstrate a fixed definition for unary attribute complement, then we could make progress. But you haven't. (I've tried quite hard.) Taking unary complements is as far as I can see, no advance.

BTW I don't see why Vadim describes axiom 2 as "Debatable". In what possible relational lattice could DUM NatJoin DEE be DEE? Only if DUM = DEE. But that would have to be a lattice system with only that single element. That's so degenerate, all the theorists I have come across say it's not a lattice at all.

It could be debatable. As long as the ability to also represent degenerate systems doesn't compromise the correctness of the model for the desired case, you can run with it. That also lies behind Vadim's idea that you may not need to prove uniqueness as long as all the variants give the same (regarding logical structure, homomorphically) logical result.

So it may be possible that you can just say "there exists a DUM" and just run with it. Although I wouldn't entirely trust that model.

If you are interested, I could do manual calculations on a degenerate system such as I have proposed and show how an element that is not DUM still can act as such in the degenerate system and give results that probably make some sort of sense. Which is why I have asked you for your definition of "NOT MATCHING".

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)