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

From: paul c <>
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, 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,

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 your answer to JOG?

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

Original text of this message