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

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 of http://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. Received on Thu Dec 11 2008 - 19:51:54 CET