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

Date: Thu, 11 Dec 2008 10:51:54 -0800 (PST)

Message-ID: <67b08aa0-8c23-482c-9f3a-c7c85bbb5ad4_at_d36g2000prf.googlegroups.com>

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