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

On Dec 11, 6:51 pm, vadim..._at_gmail.com wrote:
> On Dec 10, 5:25 pm, JOG <j..._at_cs.nott.ac.uk> wrote:
>
>
>
> > On Dec 8, 9:32 pm, vadim..._at_gmail.com wrote:
>
> > > I welcome the fact that you have switched from traditional RA
> > > operators to simpler set (D&Ds "A"lgebra: <AND>, <OR>, and <NOT>).
> > > Next, you seemed to approach view update problem algebraically, but
> > > stopped short of writing actual equations for base relations, views,
> > > their increments, and constraints. Here they are:
>
> > > The base relations:
>
> > > S - Suppliers
> > > SP - SuppliedParts
>
> > > Foreigh key constraint between S and SP is formally written as:
>
> > > (SP ^ S') v R00 = R00.
>
> > > where I leveraged standard relational lattice operators: "^" - join,
> > > "v" - generalized union, and R00 empty relation with empty header (aka
> > > D&D TABLE_DUM). Informally, foreign key constraint asserts that
> > > SuppliedParts antijoined with Suppliers produce an empty relation.
>
> > > Next, lets represent the insertion into the view, which is a join of S
> > > and SP, as a relation D (Delta). Therefore, D has the same header as
> > > SP ^ S, which is formally written as
>
> > > (SP ^ S) ^ R00 = D ^ R00.
>
> > > Our final assumption is that we insert new supplier data, therefore D
> > > should have no S# in common with the existing data:
>
> > > (D ^ (SP v S)) ^ R00 = R00.
>
> > Hi Vadim, this seems like an elegant approach but was hoping a quick
> > clarification concerning generalized union before I committed more
> > time to it. In your example would I be correct in thinking that: SP v
> > S = S
>
> > and hence your last statement above decomposes to:
> > (D ^ S) ^ R00 = R00
>
> > If so that would mean that tuples in D must feature a previously
> > unsees S# right? This confused me given the key to (SP ^ S) is {S#,
> > P#} not {S#}  (or it rather made me think I had perhaps missed
> > something along the line). Thanks in advance for any clarification you
> > can offer, Jim.
>
> You are correct, I made a typo. The assertion
> (D ^ (SP v S)) ^ R00 = R00.
> collapsed D to a nullary relation so the case becomes vacuous.
>
> Let be more careful. We have:
> 1. (SP ^ S) ^ R00 = D ^ R00
> "D and SP ^ S have the same header"
> 2.  (D ^ (SP ^ S)) v R00 = R00
> "D is addition of tuples to SP ^ S, therefore D is disjoint with SP ^
> S "
> We want to derive that insertion into SP ^ S is equivalent to
> inserting projections of D into base relations S and SP. Formally:
> (SP v D)^(S v D) = (SP ^ S) v D.
>
> Let's rename the variables as follows
> SP -> x
> S -> y
> D -> z
> and write what we want to prove as conditional assertion:
>
> (x ^ y) ^ R00 = z ^ R00 &
> (z ^ (x ^ y)) ^ R00 = R00
> -> (x v z) ^ (y v z) = (x ^ y) v z.
>
> Here as usual the "&" is Prover9 logical conjunction and the "->" is
> implication. It looks very similar to distributivity of union over
> join at page 5 ofhttp://arxiv.org/ftp/arxiv/papers/0807/0807.3795.pdf!
>
> Not surprisingly, it can be proved with the following assumptions:
> 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.
> (R00 ^ (x v y) = R00 ^ (x v z)) -> (x ^ (y v z) = (x ^ y) v (x ^ z)).
> where the first 6 are the standard lattice axioms, and the last one is
> the familiar SDC.

Unfortunately the familiar SDC is not so familar to me ;) I've had a look through your and marshall's papers but was still not clear on its derivation. Again, perhaps you could point me down the right track. The SDC states that (R00 ^ (x v y) = R00 ^ (x v z)) implies distributivity of joins over unions. But R00 joined with anything results in R00 right? Hence, while the LHS of the SDC seems universally true I am not clear how the implication is consequently reached. Received on Fri Dec 12 2008 - 02:20:14 CET