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

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.

>
> These three equations are all our knowlwedge about SP ^ S view
> updates. Now we plug them (together with RL axiom system) into
> Prover9, and derive
>
> (SP v D) ^ (S v D) = (SP ^ S) v D.
>
> with a single press of a button! Informally, under some very natural
> conditions (the 3 assertions that I described early) an increment to
> the view SP ^ S can be decomposed into independent increments of the
> base relations S and D.
Received on Thu Dec 11 2008 - 02:25:52 CET