Re: Date and McGoveran comments on view updating 'problem'

From: <vadimtro_at_gmail.com>
Date: Mon, 8 Dec 2008 16:13:42 -0800 (PST)
Message-ID: <081b1071-3a78-46a7-b6fe-a6f142329c1f_at_b38g2000prf.googlegroups.com>


On Dec 8, 2:59 pm, paul c <toledobythe..._at_oohay.ac> wrote:
> Thanks.  Although the relational lattice has seemed a fuzzy to me (no
> doubt that's my fault as usually takes me years before I feel confident
> in a mathematical topic), I gather that this example is about "insert"
> to JOIN.  

By "fuzzy" you certainly have meant "too formal"? Because, a mathematician would certainly label all these view update discussions and ad-hock rules as "fuzzy". Since you are freely operating within D&D system of <AND>, <OR>, <NOT> operations, it is not much of difference to adopt RL; in fact join and negation are the same! The difference between D&D system and RL is that the authors didn't really reinforce their algebra with axioms to allow any manipulations. (Sometime ago I mentioned how these both systems fit together).

As for deletion here is my worksheet. The first two assertions stay the same:

(SP ^ S') v R00 = R00.
(SP ^ S) ^ R00 = D ^ R00.

Next, we delete one (or several) tuple(s) from S ^ SP, therefore the delta relation D should be just a subset of the S ^ SP (because we have already established that S ^ SP and D have the same headers):

D ^ (SP ^ S) = D.

Now, we are proving the following decomposition

(SP v D')^(S v D') = (SP ^ S) v D'.

(in the previous message I forgot to mention that the unary quote operation is negation).

Again, in Prover9 the deduction is purely mechanical (it took 53 sec on my machine).

> Just guessing but I gather that RL could be seen as a
> alternative way of understanding RM, maybe more fundamental in some ways
> and maybe has some more useful mechanical theoretical tools, so I wonder
> what happens with "delete" to JOIN (which I believe is the operation
> that many people find controversial)?

We are able to formally deduce that deletion in the base realtion corresponds to the deletions from the base relations. Therefore, there is nothing controversial about deletion from join, unless my assumptions (written formally as equations) are wrong.

> BTW, ever since I first read about it, I've tried to use the TTM algebra
> in my head because the small and tight definitions make it easier to
> check my thoughts by comparing results in terms of relations.  But I
> find most other people tune out when I use them to explain myself.  

Tell me about people tuning out... There are perhaps 5 people in the world who buy in this RL stuff:-)

> Also BTW, because I didn't think it affected the problem, I wasn't
> assuming any foreign key, but if I did I could express the one involving
> S and SP as: SP{S#} & S{S#} = SP{S#} (where & means <AND>).

Actually, you are right. I removed the foreign key constraint from assumptions, and it still derives the deletion assertion! (Certainly, if I remove one of the other two assertions, the Mace4 finds a counterexample). Received on Tue Dec 09 2008 - 01:13:42 CET

Original text of this message