Quote from AntC on October 29, 2019, 12:01 am

Quote from Vadim on October 28, 2019, 6:43 pm

...

Surprisingly, the problem is still under specified as evidenced by Mace4 counterexample of cardinality 10. What other possible condition is missing?

Vadim, you're attempting (rather clumsily) the Constant Complement approach. A couple of pertinent quotes from Bancilhon & Spyratos:

"We show that a view can have more than one complement and that the choice of a complement determines an update policy. "

"... computational algorithms (if they exist) implementing steps (1) and (2) must be sought in specific problems:
for example, schemata defined by functional dependencies and views derived by projections. "

A "possible condition" is that you've under-specified what must be constant (persistent) through an update via that view. A "possible condition" is you've not recognised any key/Functional Dependency in either the base relvar or the view.

In general, B&S are quite pessimistic about 'solutions' to the update-via-views problem. Furthermore, as I pointed out on the older forum, their approach doesn't even work for the update-base 'problem'.

We've spilled more than enough ink here on update-via-view. I. can't. even.

Quote from AntC on October 29, 2019, 5:33 am

Quote from AntC on October 29, 2019, 12:01 am

Quote from Vadim on October 28, 2019, 6:43 pm

...

Surprisingly, the problem is still under specified as evidenced by Mace4 counterexample of cardinality 10. What other possible condition is missing?

Vadim, you're attempting (rather clumsily) the Constant Complement approach.

To explain a bit about constant complements:

• Start with the 'leftovers' of the base relvar(s) that are excluded from the view. (That'll be attribute p in your X1.)
• Can you reconstitute X1 from the view content with the 'leftovers'? You can use any known constraints to help.
  • In your example, you can't: the only option would be Cartesian product X1{ p } x Y1;, which'll give 4 tuples with your example, not the 2 original.
  • If not, augment the 'leftovers' with more attributes and/or tuples from the base relvar(s) until you can reconstitute.
    (Then being able to reconstitute should be an axiom in your approach.)
  • In general, there's many ways to augment: we want the augmented complement to be constant in face of updates through the view.
    (You do have an axiom for that.)
  • In your case, the only way to augment is by making the 'complement' the whole original base table.
  • That's not constant in face of updates through the view.

So what you're trying can't be done. (And I'm not surprised; and I don't understand why you say "surprisingly".)

Since UPDATE-through-projection and DELETE-through-projection are forms of update-through-view that are supported in many versions of SQL, that's a poor show for the axiomatic method.

Quote from Vadim on October 29, 2019, 8:23 pm

I agree, since SQL can handle UPDATE-through-projection, certainly, you will have no trouble writing down all the assumptions made in the OP example. To be more concrete, consider for example oracle RDBMS where any join-project view is updateable as soon as the view is key-preserving.

Unfortunately, in relational algebra perspective, we don't have axioms for functional dependency. In our earlier email exchange you attempted to introduce axioms for binary equivalence relation, but felt short of exhibiting the complete system. It looks like we have no option other than switching perspective to relational calculus. Here is the translated OP example:

%X1 v Q = Y1.
exists p X1(p,q) <-> Y1(q).

%X2 v Q = Y2.
exists p X2(p,q) <-> Y2(q).

%X1 v Q` = X2 v Q`.
exists p X1(p,q) <-> X2(p,q).

%((Y1 ^ Y2') ^ X1) v Q = ((Y2 ^ Y1') ^ X2) v Q.
exists q (Y1(q) & -Y2(q)) & X1(p,q) <-> (Y2(q) & -Y1(q)) & X2(p,q).

%X1(p,q1) & X1(p,q2) -> q1=q2.
%X2(p,q1) & X2(p,q2) -> q1=q2.

X1(p1,q) & X1(p2,q) -> p1=p2.
X2(p1,q) & X2(p2,q) -> p1=p2.

The last two lines express functional dependency q->p as required by the key-preserve condition; the prior commented out portion declared the opposite functional dependency.

Still, the system is under specified as witnessed by the following model:

X1:

p	q
1	0

X2:

p	q
0	0

Y1:

q

0

Y2:

q

0

What formal condition of key-preserved view update rule am I missing?

BTW, the 10-element model I mentioned in the original post turned out to be quite helpful, because it doesn't represent any lattice of database relations. Which hints that my 2x2 axiom system is incomplete.

Quote from AntC on October 29, 2019, 9:23 pm

Quote from Vadim on October 29, 2019, 8:23 pm

I agree, since SQL can handle UPDATE-through-projection, certainly, you will have no trouble writing down all the assumptions made in the OP example. To be more concrete, consider for example oracle RDBMS where any join-project view is updateable as soon as the view is key-preserving.

Consider how very different to TTM is SQL wrt update-through-view. SQL doesn't treat views as relvars/not as first-class (contra RM Pre 14). Neither does SQL treat update as a form of assignment (contra RM Pre 21). SQL is all very ad-hoc and unprincipled, but it works (up to a point, Lord Copper). SQL is also very different to the approach in Bancilhon & Spyratos, who assume you're replacing some view content with the update holus bolus/much more like RM Pre 21.

So SQL translates an update statement targetting a view into an update statement targetting the base table(s). In your example we might put it

UPDATE (SELECT q FROM X1) SET q = 'c' WHERE q = 'b';   // translated to

UPDATE X1 SET q = 'c' WHERE q = 'b';

DELETE (SELECT q FROM X1) WHERE q = 'b';                    // likewise translated

DELETE X1 WHERE q = 'b';

INSERT-through-projection not possible, because you can't translate it into INSERT-to-base. (Well, unless you put Nulls in column p. We won't go there.)

So SQL has a notion of tuples having identity, and that you're changing the content of a tuple(s) identified via the WHERE condition as a means to grab the identity. In Oracle, that identity can be made explicit: there's a rowid.

Unfortunately, in relational algebra perspective, we don't have axioms for functional dependency. In our earlier email exchange you attempted to introduce axioms for binary equivalence relation, but felt short of exhibiting the complete system.

I did some further work after that thread fell quiet. I think I can express a FD, but it relies on fixing R00 as DUM. Without that, anything else is going to be unprovable. And that's where I'm still stuck (after much trying).

It looks like we have no option other than switching perspective to relational calculus. Here is the translated OP example:

%X1 v Q = Y1.
exists p X1(p,q) <-> Y1(q).

%X2 v Q = Y2.
exists p X2(p,q) <-> Y2(q).

%X1 v Q` = X2 v Q`.
exists p X1(p,q) <-> X2(p,q).

%((Y1 ^ Y2') ^ X1) v Q = ((Y2 ^ Y1') ^ X2) v Q.
exists q (Y1(q) & -Y2(q)) & X1(p,q) <-> (Y2(q) & -Y1(q)) & X2(p,q).

%X1(p,q1) & X1(p,q2) -> q1=q2.
%X2(p,q1) & X2(p,q2) -> q1=q2.

X1(p1,q) & X1(p2,q) -> p1=p2.
X2(p1,q) & X2(p2,q) -> p1=p2.

The last two lines express functional dependency q->p as required by the key-preserve condition; the prior commented out portion declared the opposite functional dependency.

Still, the system is under specified ...

Vadim stop churning out code and think what you're trying to do: Do the tuples have identity/something that uniquely identifies them other than their content? In your example, you have four possibilities:

• The key is {p}, the attribute projected away from the view. Then changing the content of the view has no way to connect back to the key.
• The key is {q}, the attribute projected-in to the view. Then the 'leftovers' (attribute p) have no way to connect back to the key.
• The key is both {p, q}, so the projection view potentially has different cardinality to base. Then no way to connect back the broken halves of the key.
• There are two keys {{p}, {q}}, so either project identifies a tuple. But you're then updating q so destroying the key/no way to connect them back.
• So there's good sense in Oracle's rule that everything must be key-preserving. (BTW it's not just that the view must preserve keys: the update can't change the key content either. One of Codd's 12 rules is to that effect.)

What formal condition of key-preserved view update rule am I missing?

There's nothing you could add. Simply, you can't achieve update-through-view by this holus-bolus replacing content.

BTW, the 10-element model I mentioned in the original post turned out to be quite helpful, because it doesn't represent any lattice of database relations. Which hints that my 2x2 axiom system is incomplete.

Your axiom system used R00 to obtain headings. R00 is under-specified. Everything using R00 is incomplete.

Quote from p c on October 30, 2019, 7:44 am

The comments are not quite right. You can make a logically valid proof that applies whether or not keys are preserved. Propositional logic is enough to prove that.

It's known that if you have an operator such as rename then you can express an FD but it appears that complete and consistent systems don't have such an operator.

 

 

 

 

Quote from p c on October 30, 2019, 10:17 am

When a proof argument says nothing else about r{q} it can't conclude r{p,q}.

However it can assume that in a premise.

It can prove r{p,q}  from r{q} when p is known, such as when Forall q((r(q) = 'c' ) -> ((r(p) = 2 )). Of course this is known by the dbms when it derives the projection r{q}.

That predicate describes a set, not a tuple. But it is obviously a singleton set, so several FD's could apply.

So long as an argument doesn't assume the truth of both of that predicate and of another predicate that is identical except that r{q} = 'b', it can be a logically valid argument.

Plus, if r obeys some FD before the argument is applied it will still obey after. Such a proof argument doesn't even need to explicitly assume an FD, it only needs to be written such that the desired FD is not contradicted.

Quote from Vadim on October 30, 2019, 4:56 pm

Quote from AntC on October 29, 2019, 9:23 pm

I think I can express a FD, but it relies on fixing R00 as DUM. Without that, anything else is going to be unprovable. And that's where I'm still stuck (after much trying).

This is recurring theme of yours, but again, I'm more confused about uniqueness now, than in the past (before you raised the issue). What is uniqueness of constants and operations in Universal Algebra? I don't see it covered anywhere, except perhaps couple of exercises in undergraduate algebra textbooks asking to prove uniqueness of 0 in a group or ring. Once again, there is nothing special about constants compared to operations, so why are the book authors compelled to prove uniqueness of 0? And if we start questioning uniqueness of other operations, then we get nowhere in any algebra.

Look at the issue from the model theory perspective. As long as your axiom system outputs models which you can interpret as database relations, where exactly is the problem of the uniqueness of R00? How does the alleged nonuniqueness affect the theorems that you can formally deduce in your system?

When you are saying that an axiom system has to associate R00 with Dum unambiguously, you mean something else. There is a concept of representative relation algebras, that is when formal elements of algebra can be interpreted as binary relations and operations in both systems match. I think you are after analogous concept in the area of relational lattices. Given a model satisfying a formal system of relational lattice axioms, would we always be able to interpret the elements of the model as database relations? I didn't encounter such "abnormal" models in either LMH or 2x2 axiom system, but the question is open.

 

BTW, the 10-element model I mentioned in the original post turned out to be quite helpful, because it doesn't represent any lattice of database relations. Which hints that my 2x2 axiom system is incomplete.

Your axiom system used R00 to obtain headings. R00 is under-specified. Everything using R00 is incomplete.

The axiom system is a system of requirements to which operations should comply. All operations are introduced at once, and there is no intrinsic order among them.

I made mistake claiming that the 10-element model is not representable by database of relations. Here is the counterexample translated into database terms:

X1:

p	q
1	a
2	b

X2:

p	q
1	a
1	b
2	a
2	b

Y1:

q

a

b

Y2:

q

a

b

In both this counter example, and the one from predicate calculus perspective the view Y didn't change at all! So it is neither insert, nor update, nor delete, and I agree with your comment that the additional information whether we are deleting, updating, or inserting tuples is important -- as I just found out the hard way.

The 2x2 axiom system lives.

 

Quote from AntC on November 5, 2019, 2:10 am

(Apologies to everybody other than Vadim for burdening the forum with double-dutch.)

Quote from Vadim on October 30, 2019, 4:56 pm

Quote from AntC on October 29, 2019, 9:23 pm

I think I can express a FD, but it relies on fixing R00 as DUM. Without that, anything else is going to be unprovable. And that's where I'm still stuck (after much trying).

This is recurring theme of yours, but again, I'm more confused about uniqueness now, than in the past (before you raised the issue). What is uniqueness of constants and operations in Universal Algebra? I don't see it covered anywhere, except perhaps couple of exercises in undergraduate algebra textbooks asking to prove uniqueness of 0 in a group or ring.

When a Universal Algebra text says "An n-ary operation on A is a function ", it means the operation " takes n elements of A and returns a single element of A." Not only returns a single element but that provably it returns a single element for all possible combos of n elements as operands.

Once again, there is nothing special about constants compared to operations, so why are the book authors compelled to prove uniqueness of 0?

Yes a constant is just a nullary operation. All operations are defined by axioms (including for 0). We have to prove those axioms are sufficient to fix 0 otherwise any axiom that uses 0 to define some operation fails to define that operation as a function. (i.e. it might just define a 'relation' in the algebraic sense.)

So for example we have to prove that a definition for R01 aka DEE fixes it uniquely. (That's trivial, a blink of an eye in Prover9.)

And if we start questioning uniqueness of other operations, then we get nowhere in any algebra.

Certainly it's tedious to prove uniqueness for every constant/operation introduced. So I guess textbook authors don't trouble the reader with it. If you're breaking new algebraic ground, you must prove uniqueness. So Principia Mathematica is full of tedious proofs (and when mechanised theorem provers became available, they showed that some of Russell & Whitehead's proofs are not complete.)

Look at the issue from the model theory perspective. As long as your axiom system outputs models which you can interpret as database relations, where exactly is the problem of the uniqueness of R00?

But so far I can't interpret the models as database relations. Mace4 keeps throwing up models where R00 might be DUM, or might be some relation with a single attribute and all possible tuples for that heading. By "might be" I mean is consistent with.

How does the alleged nonuniqueness affect the theorems that you can formally deduce in your system?

Mostly by failing to prove that what I want to be functions are in fact functions (including for the dratted nullary function R00).

When you are saying that an axiom system has to associate R00 with Dum unambiguously, you mean something else.

I mean something like the following, since you only seem to understand talking in code.

Take generalised difference aka NOT MATCHING. You have equations characterising that in one of your papers: (I won't say axioms defining or proving it; but having stared long and hard at these following equations, I'm sure they fix / -- if only I could fix R00.)

(x ^ y) v (x \ y) = x.
(x ^ y) ^ (x \ y) = (x ^ y) ^ R00.

(x ^ y) v d2(x, y) = x.                    % duplicate def'n, changing the name
(x ^ y) ^ d2(x, y) = (x ^ y) ^ R00.        %

% x \ y = d2(x, y).                        % [goal]

% (x \ (x \ y)) = (x ^ y) v (x ^ R00).     % [goal] MATCHING equiv double-NOT MATCHING

Note \ is defined in terms of only ^, v, R00.

Mace4 finds a counter-example for that first goal in no time. To give my axioms in full:

x ^ x = x.
x ^ y = y ^ x.
x ^ (y ^ z) = (x ^ y) ^ z.

R01 ^ x = x.                               % R01 provably unique
R10 ^ x = R10.                             % R10 provably unique

x ^ z = x & y ^ z = y <-> z ^ (x v y) = (x v y).    % distributivity axiom
%                                % that (non-standard) def'n for v is provably unique.

R00 ^ x != x <-> x v R00 = R01.            % R00 not provably unique

By all means supply your own definitions/axioms for R00. (I can offer you heaps.) What you can't do in this 'game' is supply definitions for \ in terms of other operators -- unless those are defined in terms of ^, v. Because then you're potentially talking about some other operation.

 

There is a concept of representative relation algebras,

I have no idea what that is, do you? Or is this more cargo-cult algebra from you? The very first thing that wikipedia page says (in effect) is that this has nothing to do with relational algebra in the database sense.

that is when formal elements of algebra can be interpreted as binary relations and operations in both systems match. I think you are after analogous concept in the area of relational lattices.

I have no idea what you're talking about. I suspect you have no idea either.

Given a model satisfying a formal system of relational lattice axioms, would we always be able to interpret the elements of the model as database relations? I didn't encounter such "abnormal" models in either LMH or 2x2 axiom system, but the question is open.

Tadeus conceded [private email with you] that the LMH system doesn't fix R00 (their H).

 

BTW, the 10-element model I mentioned in the original post turned out to be quite helpful, because it doesn't represent any lattice of database relations. Which hints that my 2x2 axiom system is incomplete.

Your axiom system used R00 to obtain headings. R00 is under-specified. Everything using R00 is incomplete.

The axiom system is a system of requirements to which operations should comply.

There is an overarching requirement (I've already quoted the very first sentence of the wiki on UA) that operations must be functions.

All operations are introduced at once, and there is no intrinsic order among them.

Sure. So what? For my sanity, since v is supposed to be the dual of ^, I'd rather work with a definition that specifies v as the dual of ^. It's a perfectly valid way to define a bi-lattice, by which I mean you can prove all the same theorems.