Quote from AntC on May 23, 2021, 8:08 am

Quote from tobega on May 23, 2021, 5:40 am

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

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

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

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

 

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

 

 

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

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

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

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

Could all those be sensibly defined and is that enough?

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

 

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

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

We want to define A NatJoin B:

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

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

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

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

Where did you define minus?

And A InnerUnion B:

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

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

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

DEE = Fullest remove Fullest

Dumpty = Fullest minus Fullest

DUM = Dumpty remove Dumpty = DEE minus DEE

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

Forgive me, I should collect it all together and try to "stiffen it up". Here's the problem with not keeping up with the field, though,

I was never in the field/never taught about lattices. I learnt it all from wikipedia (and the Stamford Encyclopedia of Philosophy -- but that rapidly got too hard). Please go away and read the wiki, and stop asking questions that are much better answered there.

I don't really know what building blocks I can use. Or perhaps it is the constraints of the solver I would need to know?

You need to know no more than First-Order Propositional Logic with equality. You've got all the Boolean operators, plus 'mathematical' relations (differentish sense of 'relations'). You have functions -- which are just shorthand for mathematical relations. You have a 'universe' which is single-sorted, unless you build some functions which in effect apply a type system to divvie up the universe. (I don't do that.)

What you don't have is sets or set operations; no way to tell a set versus an element of a set. That is, unless you build a Zermelo-Fraenkel model within your FOPL. (I don't do that.)

But let's see what I would need mathematically. I assume infinity is not a problem?

Yes it's a problem: how do you define infinity? You can assume your 'universe' has an infinite number of elements. But you don't get any way to count it or state that it is (or isn't) infinite. (I don't do that. I build the model so it'll cope equally with a finite or infinite 'universe'.)

Also study Pic 8, with it's narrative about why it's not a lattice structure, even though you could certainly use it as an espalier.

A heading H is a set of identifiers.

A tuple of a heading, T<H> is a set of pairs (i, v) such that:

I'll stop you at "set". Also at "pairs".

 

 

Out of curiosity, how do you specify NatJoin without referring to any internal structure?

I don't -- which is what you don't seem to be grokking. NatJoin wrt internal structure is specified in Appendix A FORMAL DEFINITIONS <AND>. All I need to know about NatJoin is that it takes (any) two relations as operands and necessarily produces a relation as result. (It's a total function.) So I take as given the whole set of relations -- that is the domain of NatJoin is coincident with its codomain. I further observe that a consequence of the specification is NatJoin is commutative, associative, idempotent. And that it gives a (partial) ordering of its domain. If it didn't, I couldn't model it using lattices.

But the point is that the lattice structure models the interaction of relations as 'black box' elements of a set. It doesn't model the internal structure; it doesn't specify how to construct the result of NatJoin from its operands.

 

Quote from AntC on May 23, 2021, 9:11 am

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

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

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

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

Ok here's three reasons why your 4-element model (all elements with heading {p}) can't model a relational lattice. I'll give reasons later why no 4-element model can be a model of a relational lattice. (Actually it's more like two-and-a-half reasons: the third is a semantic corollary of the first's equations.)

To be clear: I'm not denying your 4 elements are a lattice of some sort. It just can't be a model of relations. We know models of relations have lots of structure, even though we don't (usually) bother specifying it:

• The M3 non-modular lattice Pic 10 does not appear embedded.
• There's a Boolean Algebra (distributive sub-lattice) 'descending' from every element to the empty relation with that heading, being all possible combinations of the tuples in the body of that element.
• There's a Boolean Algebra (distributive sub-lattice) 'descending' from DUM to lattice bottom (the empty relation with every possible attribute), being all possible combinations of attributes, and including/connecting up to each empty relation at the 'foot' of the 'descender' from each element (previous bullet).

Addit: heh, heh, fun discovery: If you don't bother specifying that last, you find Remove is ill-defined. What you get is the below 'quickly dismiss'ed 4-element model, in which Removing the 'some other' empty relation from Dumpty would give a relation with only that mysterious 'extra attribute'. Except there's no relation with that heading, so Mace4 plumps for making it DUM. So then your equations are banjaxed.

1. In your model, the Fundamental Empty Relation Axiom doesn't hold: r NatJoin DUM ≠ r ≡ r InnerUnion DUM = DUM. That is, there should be two equivalent ways to detect whether a relation is empty. (Errk! If you saw an early version of this post, the lhs of the equivalence had an equality: s/b disequality.)
2. That model is not scalable: as soon as you allow for elements with different headings (and therefore elements with the union of those headings), there's no element that models DUM.
3. That model can't express the result from yes/no queries. It's like asking if the Congo is the second-longest river in Africa yes or no?, and getting told the Nile is 6,650 kms long. Perhaps I already know the Nile is the longest; perhaps I even know it's length;  perhaps I know the length of the Congo. I don't know if the Congo is second-longest, which is why I'm asking. Telling me the length of the Niger, or the lengths of all the rivers, also wouldn't be an answer. I just want yes or no. If all possible relations have exactly the same heading, it can't give those answers.

 

To dismiss quickly the 4-element model with DEE, DUM, some empty relation with a non-empty heading, Dumpty (lattice bottom: empty relation with maximal heading):

• Dumpty's heading must be larger than 'some empty's; so there must be an extra attribute; then there must be an empty relation with heading that attribute only.
• So a 5-element model is ok: all relations empty except DEE.

Before we get to the third possible 4-element model, consider a business requirement in which there are only 4 states of the world: the shop is open True/False; Cartesian product the alarm is set True/False. So we have DEE/DUM representing (say) shop open True/False; and another relation with non-empty heading and one possible tuple vs empty representing alarm is set True/False. What if the alarm is not set? Then we must have an empty relation value; so it can't be DEE, so we can't represent both the shop is open and the alarm not set.

This goes wider to ban any attribute type with only one possible value: for all possible non-empty relation values (that is, all possible non-empty answers to queries over the database, other than yes/no questions), that attribute must hold TheValue. It therefore cannot convey information content. Useless. Not a model of relations.

Picking up the 4-element lattice model for the shop/alarm example:

1. The Fundamental Empty Relation Axiom can be expressed. But not uniquely: it would work equally well whether we took DUM  (the relation with empty heading, no tuple) as DUM in that equation, or Fullest (aka R11 the relation with maximal heading and maximal tuples) as fake-DUM -- in which case the (dis-)equations being true allege DUM is non-empty.
2. The model is not scalable: not only if you introduce extra attributes (whether or not their type allows more than one value -- see para above); but also if you subsequently allow more than one value for the attribute's type. Now it's revealed that using fake-DUM  as DUM in that equation breaks down.
3. We can kinda answer yes/no questions. Except if we ask is the shop open when the alarm is not set, we'll get the wrong answer.
   More importantly (semantically speaking) we can't take this 4-element model as representing the extension of some predicate in which we substitute attribute values from the tuple(s) into the predicate.

Equationally, the 'Fundamental Empty Relation Axiom' is equivalent to saying DUM must be immediately adjacent below DEE. Semantically that's to say there's no answer between Yes/No. IOW we don't facilitate 'Up to a point, Lord Copper'. You can figure that out by trying a model with an intervening element.

Quote from tobega on May 23, 2021, 1:58 pm

Quote from AntC on May 23, 2021, 8:08 am

Quote from tobega on May 23, 2021, 5:40 am

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

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

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

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

 

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

 

 

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

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

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

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

Could all those be sensibly defined and is that enough?

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

 

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

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

We want to define A NatJoin B:

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

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

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

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

Where did you define minus?

And A InnerUnion B:

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

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

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

DEE = Fullest remove Fullest

Dumpty = Fullest minus Fullest

DUM = Dumpty remove Dumpty = DEE minus DEE

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

Forgive me, I should collect it all together and try to "stiffen it up". Here's the problem with not keeping up with the field, though,

I was never in the field/never taught about lattices. I learnt it all from wikipedia (and the Stamford Encyclopedia of Philosophy -- but that rapidly got too hard). Please go away and read the wiki, and stop asking questions that are much better answered there.

I don't really care about lattices, I'm not convinced they are necessary

I don't really know what building blocks I can use. Or perhaps it is the constraints of the solver I would need to know?

You need to know no more than First-Order Propositional Logic with equality. You've got all the Boolean operators, plus 'mathematical' relations (differentish sense of 'relations'). You have functions -- which are just shorthand for mathematical relations. You have a 'universe' which is single-sorted, unless you build some functions which in effect apply a type system to divvie up the universe. (I don't do that.)

What you don't have is sets or set operations; no way to tell a set versus an element of a set. That is, unless you build a Zermelo-Fraenkel model within your FOPL. (I don't do that.)

But let's see what I would need mathematically. I assume infinity is not a problem?

Yes it's a problem: how do you define infinity? You can assume your 'universe' has an infinite number of elements. But you don't get any way to count it or state that it is (or isn't) infinite. (I don't do that. I build the model so it'll cope equally with a finite or infinite 'universe'.)

Also study Pic 8, with it's narrative about why it's not a lattice structure, even though you could certainly use it as an espalier.

A heading H is a set of identifiers.

A tuple of a heading, T<H> is a set of pairs (i, v) such that:

I'll stop you at "set". Also at "pairs".

 

 

Out of curiosity, how do you specify NatJoin without referring to any internal structure?

I don't -- which is what you don't seem to be grokking. NatJoin wrt internal structure is specified in Appendix A FORMAL DEFINITIONS <AND>. All I need to know about NatJoin is that it takes (any) two relations as operands and necessarily produces a relation as result. (It's a total function.) So I take as given the whole set of relations -- that is the domain of NatJoin is coincident with its codomain. I further observe that a consequence of the specification is NatJoin is commutative, associative, idempotent. And that it gives a (partial) ordering of its domain. If it didn't, I couldn't model it using lattices.

But the point is that the lattice structure models the interaction of relations as 'black box' elements of a set. It doesn't model the internal structure; it doesn't specify how to construct the result of NatJoin from its operands.

 

OK, so the problem is the actual solver, because my mathematics works fine. NP, I'll leave you to it.

Quote from AntC on May 23, 2021, 10:52 pm

Quote from tobega on May 23, 2021, 1:58 pm

Quote from AntC on May 23, 2021, 8:08 am

Quote from tobega on May 23, 2021, 5:40 am

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

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

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

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

 

Forgive me, I should collect it all together and try to "stiffen it up". Here's the problem with not keeping up with the field, though,

I was never in the field/never taught about lattices. I learnt it all from wikipedia (and the Stamford Encyclopedia of Philosophy -- but that rapidly got too hard). Please go away and read the wiki, and stop asking questions that are much better answered there.

I don't really care about lattices, I'm not convinced they are necessary

No indeed, there are many possible tools to model the logic of relations. For me it's the aesthetic appeal of the structure.

 

Quote from AntC on May 24, 2021, 6:59 am

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

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

 

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

x <REMOVE> y = x v y`.

No that won't work. You're telling me that weird-inverse returns a non-empty result (sometimes). Then InnerUnion with it will include tuples from invert-y that weren't in x.

x <NotMatching> y = x ^ y'.

No that won't work. The heading of a NotMatching must be the heading of its left operand. This suggestion will return a relation with heading the union of the headings of its operands.

In both cases we need emptify(_); which might be _ NatJoin DUM -- except that your axioms allow a model in which your R00 corresponds to DEE. In which case _ NatJoin fake-DUM will be identity on the left operand.

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

Thinking a bit about the non-definition of things, this is how I understand what's being attempted:

You're assuming that there exists a set of elements, nothing much specified about them. It could be the set containing just DEE, or just DEE and DUM, or a set of things that don't look very much like relations at all. The important thing is that these elements in some important respects behave like relations, so we can take a set of relations and map onto a set of elements that "works".

Then you define an operator called NatJoin which is some operator that in some respects behaves on the set of elements like the thing we know as natural join would behave on what we know as relations. More importantly, we want to make sure that NatJoin does not behave in any way contrary to natural join. It might be possible that we could define an operator that behaves like NatJoin but isn't natural join. However, as far as the model goes, whatever we manage to prove about NatJoin would also hold for natural join. And similarly for all the relational operators we map onto this model.

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.

Would that be a reasonable summary?

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

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

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), 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 dandl on May 24, 2021, 2:09 pm

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.

This doesn't make sense. If R does not have attribute a then its predicate does not mention a and the value of a cannot be considered. You cannot write a predicate for R or R' to give effect to what you just said. And relation A is a relcon, effectively a function that returns TRUE for every value of a.

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

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

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), 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)

Again, I don't think you can write that predicate. A tuple asserts a fact that makes the predicate true. You would need to write something like a function (a relcon), something like:

S: Supplier
[S#] is named [SNAME] and has a status of [STATUS] and is located in city
[CITY] and [a] is an integer.  

This still doesn't make it take on every possible integer value.

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 Vadim on May 24, 2021, 9:03 pm

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

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

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

Don't blame me, the "^","v"  notation is credited to Marsall Spight who most likely took it from the Prover9 creator William McCune. I initially disliked it too, but eventually have grown to appreciate it.

Then, the postfix single quote is used as negation in Prover9 BA examples. Since we have 2 analogs of Boolean negation, I had to have another symbol, and have chosen the back quote for attribute negation, while keeping the original single quote for tuple complement. Yes, they are challenging to distinguish, but what is the alternative: to type more?

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

Quote from Vadim on May 24, 2021, 9:03 pm

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

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

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

Don't blame me, the "^","v"  notation is credited to Marsall Spight who most likely took it from the Prover9 creator William McCune. I initially disliked it too, but eventually have grown to appreciate it.

Then, the postfix single quote is used as negation in Prover9 BA examples. Since we have 2 analogs of Boolean negation, I had to have another symbol, and have chosen the back quote for attribute negation, while keeping the original single quote for tuple complement. Yes, they are challenging to distinguish, but what is the alternative: to type more?

Yes type more. This is a blog for communicating. Not some sort of private notation for talking to yourself. (Yes in Prover9 I use ^, v -- which is standard math notation. No I don't expect anybody here to read Prover9 formulas.)