Re: Date and McGoveran comments on view updating 'problem'
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.
>
I hope Vadim will answer these questions.
In the meantime, I'd like to point out that based on
http://arxiv.org/pdf/0807.3795,
SP v S = S can't be true given the usual attributes Date ascribes to SP
and S, for example Supplier_Name or somesuch is in S but not in SP. I
think it could be true for SP{S#, P#} V S{S#} = S{S#} with a further
proviso that S# is a foreign key. Vadim, can you cover this point in
Apart from the above, I'd also like to say that as far as my original question is concerned, I don't think key constraints need to be presumed in order to examine the algebraic possibilities. First, while it may well be that the dbms catalog reflects key constraints, Date's example is a "delete", so as long as it involves applying only <AND> <NOT> to S or SP, no new tuples that didn't satisfy the key constraint could be introduced. Foreign key constraints could be important if certain S tuples end up being deleted (this may contradict what I said in a previous post). Second, the TTM A-algebra includes no notion of a proper subset of attributes being "key" (or foreign "key" for that matter), only the notion of all attribute values in a tuple standing for a unique tuple within a relation. So it seems to me that any Prover9 demonstration ought to have a main example that ignores key constraints, not to say that couldn't be buttressed with examples that include keys.
Another question I have is whether anybody here knows whether Prover9 depends on a lattice formulation, or could it be applied using the TTM A-algebra instead? Received on Thu Dec 11 2008 - 14:37:26 CET