Expressing FDs without RENAME (nor COUNT)
Quote from AntC on July 26, 2019, 6:58 amQuote from Erwin on July 25, 2019, 9:20 pmQuote from AntC on July 25, 2019, 3:29 pmQuote from Erwin on July 25, 2019, 10:58 amIf step 4 amounts to WHERE y <> y' (that is, such an inequality test included for each attribute in y and all of them ORed together) ...
Step 4 takes the place of the inequality test you'd use if RENAMing. That is, that's my intent. But I'm asking if I've got it right using an injective relcon instead.
...
So with this post you officially have the confirmation that you've got it right from someone who is a member of both the set of non-algebraicists and that of non-logicians.
Thank you. The parts for which I think I need confirmation from an algebraicist/logician is whether my definition of what makes a relation represent a bijective function is robust. Note the intent is that any suitably bijective relation will do. So the compiler-writer's/implementor's guilty little secret will be that if they need 'just any' bijective relation, they can implement that as a RENAME.
OK let's recap wrt expressing dependencies in the lattice algebra:
* we have (maybe) a way to express FDs. I don't hear Vadim celebrating: this has been a difficulty for several years.
* JD constraints are easily expressed as 'lossless join decomposition'
* Therefore MVDs are easy as a special case of JDs.
* FDs 'come with' a MVD: if the definitions I've given for FDs are correct, we should be able to use the algebra to infer that MVD. Needs R00 robustly defined, of course.
* INDs are easily expressed using the lattice ordering equivalent of subset -- providing the two relations have the same attribute names for the attributes involved in the IND.
What if the IND is between differently-named attributes? Conventionally you'd use a RENAME to get the same attrib names. Instead, can I use the bijective relation idea? I think it needs both apply the bijection from subset relation to superset relation's attributes and check the subset as lattice ordering; and apply the bijection 'in reverse' from superset relation's attributes to subset's and again check the superset as lattice ordering. Why both directions? Because it would be possible to 'cheat' in the construction of the bijection if it were only to apply in one direction.
There's an ugly case of INDs where some of the attributes are same-named, some different. Then we need to split out the differently-named for the bijection treatment.
Now I'm entertaining a radical thought: is RENAME (or equivalently equi-relations) essential to relational completeness? Could we weaken the requirement to being for bijective relations? Consider
* The first appearance of (what was effectively) RENAME in the literature is in Codd 1972 'Relational Completeness ...' to give a definition of Natural Join in terms of Cartesian Product with various renamings. TTM avoids that need by making JOIN aka <AND> the primitive, then (trivially) defining Cartesian Product in terms of <AND>.
* FDs can be defined without RENAME tbc.
* INDs can be defined without RENAME tbc.
* Another common use for RENAME is where self-joining a relation (e.g. representing a hierarchy), to avoid too much joining. Again we could use a bijection to move attributes out of the way, then bring them back, or use the bijection relation in some restriction role, as I've done for FDs.
Thoughts?
What I've understood from your ramblings is you've "unveiled" a way to define <RENAME> in terms of <COMPOSE> (itself <AND> and <REMOVE>) at the expense of introducing your yy' relation.
But that yy' relation is itself a U(niversal) relation restricted to "corresponding" attributes having equal values. And you can't express that restriction as another <AND> because that <AND> would require the very thing you are trying to define. So to me it seems you're now stuck at feasible ways to pinpoint yy'.
Quote from Erwin on July 26, 2019, 2:29 pmQuote from AntC on July 26, 2019, 6:58 amQuote from Erwin on July 25, 2019, 9:20 pmQuote from AntC on July 25, 2019, 3:29 pmQuote from Erwin on July 25, 2019, 10:58 amIf step 4 amounts to WHERE y <> y' (that is, such an inequality test included for each attribute in y and all of them ORed together) ...
Step 4 takes the place of the inequality test you'd use if RENAMing. That is, that's my intent. But I'm asking if I've got it right using an injective relcon instead.
...
So with this post you officially have the confirmation that you've got it right from someone who is a member of both the set of non-algebraicists and that of non-logicians.
Thank you. The parts for which I think I need confirmation from an algebraicist/logician is whether my definition of what makes a relation represent a bijective function is robust. Note the intent is that any suitably bijective relation will do. So the compiler-writer's/implementor's guilty little secret will be that if they need 'just any' bijective relation, they can implement that as a RENAME.
OK let's recap wrt expressing dependencies in the lattice algebra:
* we have (maybe) a way to express FDs. I don't hear Vadim celebrating: this has been a difficulty for several years.
* JD constraints are easily expressed as 'lossless join decomposition'
* Therefore MVDs are easy as a special case of JDs.
* FDs 'come with' a MVD: if the definitions I've given for FDs are correct, we should be able to use the algebra to infer that MVD. Needs R00 robustly defined, of course.
* INDs are easily expressed using the lattice ordering equivalent of subset -- providing the two relations have the same attribute names for the attributes involved in the IND.
What if the IND is between differently-named attributes? Conventionally you'd use a RENAME to get the same attrib names. Instead, can I use the bijective relation idea? I think it needs both apply the bijection from subset relation to superset relation's attributes and check the subset as lattice ordering; and apply the bijection 'in reverse' from superset relation's attributes to subset's and again check the superset as lattice ordering. Why both directions? Because it would be possible to 'cheat' in the construction of the bijection if it were only to apply in one direction.
There's an ugly case of INDs where some of the attributes are same-named, some different. Then we need to split out the differently-named for the bijection treatment.
Now I'm entertaining a radical thought: is RENAME (or equivalently equi-relations) essential to relational completeness? Could we weaken the requirement to being for bijective relations? Consider
* The first appearance of (what was effectively) RENAME in the literature is in Codd 1972 'Relational Completeness ...' to give a definition of Natural Join in terms of Cartesian Product with various renamings. TTM avoids that need by making JOIN aka <AND> the primitive, then (trivially) defining Cartesian Product in terms of <AND>.
* FDs can be defined without RENAME tbc.
* INDs can be defined without RENAME tbc.
* Another common use for RENAME is where self-joining a relation (e.g. representing a hierarchy), to avoid too much joining. Again we could use a bijection to move attributes out of the way, then bring them back, or use the bijection relation in some restriction role, as I've done for FDs.
Thoughts?
What I've understood from your ramblings is you've "unveiled" a way to define <RENAME> in terms of <COMPOSE> (itself <AND> and <REMOVE>) at the expense of introducing your yy' relation.
No: I am not proposing a way to define RENAME. I am proposing a way to avoid RENAME.
But that yy' relation is itself a U(niversal) relation restricted to "corresponding" attributes having equal values.
Emphatically no: not equal values. A bijection. See all the examples here: no equal values.
And you can't express that restriction as another <AND> because that <AND> would require the very thing you are trying to define. So to me it seems you're now stuck at feasible ways to pinpoint yy'.
I believe I don't need feasible ways to pinpoint yy'. I just need to define its properties. And that's what I did in the very first post in this thread, starting at "forall relations z ...". This is what's called an existence proof: any relation that represents a bijection with the correct heading will do.
An implementor of a D whose underlying algebra is lattice-like will need to pinpoint some yy'. They're entitled to choose anything with the desired properties. It'll be jolly handy to choose a) the target attributes to correspond to the source; b) the target attribute values to be equal to the source. That's a no-brainer choice for the implementor, given an otherwise arbitrary choice.
But to prove there's nothing up my sleeves, here's an equally valid choice:
* Given that in general the bijection is wrt multiple attributes (such as all the non-key attributes in a relation),
* make the target a single attribute, whose name is a hash of the source attributes' names.
* Make the target value a pipe-delimited concatenation of the source values (suitably serialised to String), then hashed using an algorithm sure not to produce collisions.
OK, to re-iterate,
1. project {X, Y} from R;
I am personally not concerned with this projection. I am concerned with some relation schema in which some FD is supposed/required to hold and that relation schema could well be the schema of a projection view, so I think what I have to say applies regardless of your point 1.
2. COMPOSE the projection with bijection yy' to get a relation with heading {X, Y'}
My step 2 is to RENAME but it makes no difference : in both your and mine case the result is a relation in which only the attributes of the concerned FD's LHS have "kept their name" and the others haven't.
Composition involves removing relation attributes? That is requiring unary attribute inversion operation, or binary REMOVE?
3. JOIN that back to R (i.e. JOIN on attributes X in common), then we have attributes {X, Y, Y', and others}
The "and others" does not apply in my case because of my remark on point 1., but it makes no difference.
4. Take that join NOT MATCHING yy'.
So you get a relation from the original where all of the attributes in X (the FD's LHS) match but not all of the (corresponding) attributes between (those in) y and y' match. (Which is indicative of two distinct tuples in the original in which all of the attributes in X match.) Yes that's my step 4.
5. The result must be empty, if the FD holds.
Doesn't "join NOT MATCHING" involve unary negation (NOT), or is it primitive binary operation in your system?
Quote from Vadim on July 26, 2019, 6:00 pmOK, to re-iterate,
1. project {X, Y} from R;
I am personally not concerned with this projection. I am concerned with some relation schema in which some FD is supposed/required to hold and that relation schema could well be the schema of a projection view, so I think what I have to say applies regardless of your point 1.
2. COMPOSE the projection with bijection yy' to get a relation with heading {X, Y'}
My step 2 is to RENAME but it makes no difference : in both your and mine case the result is a relation in which only the attributes of the concerned FD's LHS have "kept their name" and the others haven't.
Composition involves removing relation attributes? That is requiring unary attribute inversion operation, or binary REMOVE?
Yes COMPOSE requires removing attributes in common. I define REMOVE as a relative complement of headings. I plain don't like your 'inversion' absolute complement. It seems to involve worse than domain-dependence, as I already said somewhere. I define REMOVE axiomatically in the algebra. Can't remember exactly how/I'm travelling so don't have that work with me, but to give a flavour:
* r1 REMOVE (r1 REMOVE r2) = r1 InnerUnion (r2 JOIN R00).
IOW double-REMOVE is the same as projection. Of course the axioms run smack into the indefiniteness of R00.
3. JOIN that back to R (i.e. JOIN on attributes X in common), then we have attributes {X, Y, Y', and others}
The "and others" does not apply in my case because of my remark on point 1., but it makes no difference.
4. Take that join NOT MATCHING yy'.
So you get a relation from the original where all of the attributes in X (the FD's LHS) match but not all of the (corresponding) attributes between (those in) y and y' match. (Which is indicative of two distinct tuples in the original in which all of the attributes in X match.) Yes that's my step 4.
5. The result must be empty, if the FD holds.
Doesn't "join NOT MATCHING" involve unary negation (NOT),
No. I define NOTMATCHING as relative complement. (D&D use absolute/unary <NOT>, but I'm avoiding domain dependence.)
or is it primitive binary operation in your system?
No. It's defined axiomatically as in one of your earlier papers:
* (r1 JOIN r2) InnerUnion (r1 NOTMATCHING r2) = r1.
* (r1 JOIN r2) JOIN (r1 NOTMATCHING r2) = (r1 JOIN r2) JOIN R00.
That's sufficient to fix NOTMATCHING, or rather, it would be if only R00 were fixed.
That's why everything that should be possible with the lattice approach keeps coming back to the problem that R00 is not unique. If I were to define R00 in terms of absolute complement and/or attribute inversion and/or identity element of <OR>, still it wouldn't fix R00 in terms of lattice meet/join, therefore it wouldn't fix NOTMATCHING. I know, I've tried and tried.
(I've used Tutorial D style expressions in the above. Of course when running theorems in Prover9/Mace4 I use ^ v \ etc.
Quote from AntC on July 26, 2019, 7:20 amQuote from Vadim on July 25, 2019, 4:25 pmThere is no need for negation (aka NOT MATCHING). Lattice order (tuple subset) would suffice.
If "q=q1" is denoting a RENAME, you seem to have misunderstood the point: I'm aiming to express FDs without RENAME.
OK, confirmation on another thread that 'what's in a name' with an embedded '=' does represent an equi-relation, not a bijection.
b) where is all the machinery that expresses its properties as a bijection, or that gives its content as an example of a bijection?
Then Vadim's earlier demonstration in QBQL demonstrates nothing useful.
* We already know we can express FDs using RENAME.
* We already know (or strongly suspect) we can't axiomatise RENAME, that is can't axiomatise the definition for an equi-relation. Because the lattice algebra has no concept of attribute name nor of attribute value nor of equal values between different-named attributes.
* I think I can axiomatise bijections, that is the properties of a relation representing a bijection between distinct headings.
But I can't prove that to my own satisfaction in a Prover tool, because anything 'applying' the bijection relation needs to express conditions on headings of its 'arguments', and that needs R00 fixed.
Quote from AntC on July 27, 2019, 5:08 am...I define REMOVE as a relative complement of headings. I plain don't like your 'inversion' absolute complement. It seems to involve worse than domain-dependence, as I already said somewhere. I define REMOVE axiomatically in the algebra. Can't remember exactly how/I'm travelling so don't have that work with me, but to give a flavour:
* r1 REMOVE (r1 REMOVE r2) = r1 InnerUnion (r2 JOIN R00).
IOW double-REMOVE is the same as projection. Of course the axioms run smack into the indefiniteness of R00.
One axiom is not enough to unambiguously define an operation. As I emphasized before, from algebraic perspective having unsafe operations is not big deal. If the universe (that is the set of relations arranged into the lattice) is finite, then both the negation and inversion are well defined. And then we have a system where we can test if your two extra operations are unambiguos. Let use binary plus and minus as shorthand for the two versions of your REMOVE. Then:
x ^ y = y ^ x. (x ^ y) ^ z = x ^ (y ^ z). x ^ (x v y) = x. x v y = y v x. (x v y) v z = x v (y v z). x v (x ^ y) = x. % Litak et.al. x ^ (y v z) = (x ^ (z v (R00 ^ y))) v (x ^ (y v (R00 ^ z))). (x ^ y) v (x ^ z) = x ^ ( ((x v z) ^ y) v ((x v y) ^ z) ). (R00 ^ (x ^ (y v z))) v (y ^ z) = ((R00 ^ (x ^ y)) v z) ^ ((R00 ^ (x ^ z)) v y). % Unary postfix negation operation ' aka <NOT> x' ^ x = R00 ^ x. x' v x = R00'` v x. %R00' ^ x = x. % Unary postfix inversion operation ` aka <INV> x` ^ x = R00'` ^ x. x` v x = R00 v x. %R00` v x = x. % FDI x = (x ^ y') v (x ^ y`). % Distributivity of join over outer union aka <OR> x ^ (y' ^ z')' = ((x ^ y)' ^ (x ^ z)')'. % Anthony's axiom for REMOVE x * (x * y) = (x ^ (r2 ^ y)) v ((x v (y ^ R00)) ^ R00). x + (x + y) = (x ^ (r2 ^ y)) v ((x v (y ^ R00)) ^ R00).
With the goal:
x + y = x * y.
With such input the Mace4 exhibits 2 element counterexample.
Of course, the fact that I have attribute inversion would allow me to unambiguously define the binary REMOVE operation. This is besides the point, which is again is that your axiom is not completely defines REMOVE even with unambigous (fixed) R00.
Quote from Vadim on July 28, 2019, 6:12 pmQuote from AntC on July 27, 2019, 5:08 am...I define REMOVE as a relative complement of headings. I plain don't like your 'inversion' absolute complement. It seems to involve worse than domain-dependence, as I already said somewhere. I define REMOVE axiomatically in the algebra. Can't remember exactly how/I'm travelling so don't have that work with me, but to give a flavour:
* r1 REMOVE (r1 REMOVE r2) = r1 InnerUnion (r2 JOIN R00).
IOW double-REMOVE is the same as projection. Of course the axioms run smack into the indefiniteness of R00.
Vadim, please read my posts (and everybody's posts) more carefully; and stop posting pointless and unhelpful proofs of theorems that noboy's denying, nor disproofs of claims nobody's making.
One axiom is not enough to unambiguously define an operation.
I explicitly gave three reasons (at least) I was not claiming that's sufficient as an axiom:
* "I define ... Can't remember exactly how ..."
* "to give a flavour ..." is not claiming anything is sufficient.
* "... run smack into the indefiniteness of R00".
I would need at least:
* an axiom saying the heading of (r1 REMOVE r2) is disjoint from the headings of (r1 InnerUnion r2).
* and axiom saying the heading of ((r1 REMOVE r2) JOIN (r1 InnerUnion r2)) = heading of r1.
Those axioms rely on 'heading of', and that relies on definedeness of R00, that we don't have. Please don't post another useless (dis-)proof that those two axioms fail to fix REMOVE.
Quote from Vadim on July 28, 2019, 6:12 pmQuote from AntC on July 27, 2019, 5:08 am...I define REMOVE as a relative complement of headings. I plain don't like your 'inversion' absolute complement. It seems to involve worse than domain-dependence, as I already said somewhere. I define REMOVE axiomatically in the algebra. Can't remember exactly how/I'm travelling so don't have that work with me, but to give a flavour:
* r1 REMOVE (r1 REMOVE r2) = r1 InnerUnion (r2 JOIN R00).
IOW double-REMOVE is the same as projection. Of course the axioms run smack into the indefiniteness of R00.
As I emphasized before, from algebraic perspective having unsafe operations is not big deal.
But your 'inversion' is not merely an "unsafe" operation, as that term is defined in the literature. Frankly Vadim I am increasingly sure you do not know what you are talking about. As another example, what you've posted about Fagin's product is just gibberish; I didn't bother replying. As another example, you haven't yet posted an adequate proof that R00 is uniquely defined.
"unsafe operations" is to do with domain dependence. What is the 'domain' -- that is, the type of values, when it comes to attribute names?
If the universe (that is the set of relations arranged into the lattice) is finite,
You haven't proved that the lattice is finite. Therefore that must be an axiom. What axiom states finiteness of the lattices? There are at least two reasons to think the lattice is not finite:
* Nowhere is there a statement that the domain(s) of attribute values are finite.
* Nowhere is there a statement that the number of attribute names is finite.
* Furthermore, if you wish to include Relation-Valued-Attributes in your domains, then the lattice is beyond countably infinite. If you don't want to include RVA's, please explain how/where you exclude them.
... And then we have a system where we can test if your two extra operations are unambiguos.
With such input the Mace4 exhibits 2 element counterexample.
That sounds exactly like a proof that R00 is not adequately defined in terms of lattice meet/join.
First do this:
Provide a parallel set of axioms with R00 replaced by (say) R002.
Prove R00 = R002.
(The alleged proof you've provided so far for the uniqueness of R00 relies on the definedness of negation. You haven't proved that's defined uniquely, in fact you've conceded it isn't.)
Here is simplified argument, which settles the dispute. Assume there are the two binary operations - slash and back slash- satisfying the following axioms:
(y / x) ^ x = 0 ^ x. (y \ x) v x = 0 v x.
then the constant 0 is uniquely defined. In our standard relational lattice interpretation those are counterparts of NOT MATCHING and REMOVE. The proof:
1 0 = 1. [goal]. 2 x ^ y = y ^ x. [assumption]. 3 x ^ (x v y) = x. [assumption]. 4 x v y = y v x. [assumption]. 5 (x / y) ^ y = 0 ^ y. [assumption]. 6 x ^ (y / x) = 0 ^ x. [para(2(a,1),5(a,1))]. 7 (x \ y) v y = 0 v y. [assumption]. 8 x v (y \ x) = 0 v x. [para(4(a,1),7(a,1))]. 9 (x / y) ^ y = 1 ^ y. [assumption]. 10 y ^ (x / y) = 1 ^ y. [para(2(a,1),9(a,1))]. 11 0 ^ y = 1 ^ y. [para(6(a,1),10(a,1))]. 12 1 ^ x = 0 ^ x. [copy(11),flip(a)]. 13 (x \ y) v y = 1 v y. [assumption]. 14 y v (x \ y) = 1 v y. [para(4(a,1),13(a,1))]. 15 0 v y = 1 v y. [para(8(a,1),14(a,1))]. 16 1 v x = 0 v x. [copy(15),flip(a)]. 17 1 != 0. [deny(1)]. 18 0 ^ (1 v x) = 1. [para(12(a,1),3(a,1))]. 19 0 ^ (0 v x) = 1. [para(16(a,1),18(a,1,2))]. 20 0 = 1. [para(3(a,1),19(a,1))]. 21 1 = 0. [copy(20),flip(a)]. 22 $F. [resolve(21,a,17,a)].
Quote from Vadim on July 29, 2019, 6:48 pmHere is simplified argument, which settles the dispute. Assume there are the two binary operations - slash and back slash- satisfying the following axioms:
(y / x) ^ x = 0 ^ x. (y \ x) v x = 0 v x.then the constant 0 is uniquely defined. In our standard relational lattice interpretation those are counterparts of NOT MATCHING and REMOVE.
First equation, assuming / is intended as the counterpart of NOT MATCHING, and 0 as counterpart of DUM:
* heading of lhs is union of headings of y, x. heading of rhs is heading of x.
Those headings are not equal (in general). So you've started with a falsehood, given those assumptions are implicitly forall quantified. Then Prover9 has ended at $F. Falsehood implies anything. Not a proof.
Second equation, assuming \ is intended as counterpart of REMOVE:
* headings on both sides are empty OK
* lhs content is non-empty if either x is non-empty or y is non-empty. rhs content is non-empty just in case x is non-empty.
So you've started with another falsehood, etc, etc.
Also as you said earlier:
One axiom is not enough to unambiguously define an operation.
Then I'm not seeing that one axiom for NOT MATCHING and one for REMOVE fixes anything.