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

From: paul c <toledobythesea_at_oohay.ac>
Date: Thu, 11 Dec 2008 13:37:26 GMT
Message-ID: <qI80l.4098\$yK5.2013_at_edtnps82>

JOG 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.
>

>> 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.
>