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

From: JOG <jog_at_cs.nott.ac.uk>
Date: Fri, 12 Dec 2008 03:34:25 -0800 (PST)
Message-ID: <f55871dc-ad7a-44fc-98ec-017af751e032_at_k1g2000prb.googlegroups.com>


On Dec 12, 1:49 am, vadim..._at_gmail.com wrote:
> On Dec 11, 5:20 pm, JOG <j..._at_cs.nott.ac.uk> wrote:
>
>
>
> > 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?
>
> Nope. R00 is nullary empty relation. Joining it with nonnullary
> relation results in some nonnullary empty relation, which is different
> from R00. The only relation invariant to joining with the other
> relations is the lattice supremum R10.

Ah, of course, the header. Now it makes sense - distributivity requires correspondence in header unions. It might be worth noting that I did not make the assumption that headers intersect when the two components of a join are disjunct (and on a quick reglance of your work could see no mention of this). In "First Steps in Relational Lattice" you very neatly define a natural join over two binary relations as:

A(x,y) ^ B(y,z) = {(x,y,z) | (x,y)EA & (y,z)EB }

However, this makes no mention of headers at all, leaving ambiguity that might be worth just rectifying in future papers (to avoid any confusion in those like me who don't assume a theoretical requirement for header constructs).

Nevertheless all very interesting stuff Vadim! Have you formally published your work in this area?

>
> Perhaps the original Marshall's messagehttp://newsgroups.derkeiler.com/Archive/Comp/comp.databases.theory/20...
> is better for informal exposure.
Received on Fri Dec 12 2008 - 12:34:25 CET

Original text of this message