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

From: <vadimtro_at_gmail.com>
Date: Mon, 8 Dec 2008 13:32:35 -0800 (PST)
Message-ID: <2ac2d60f-c6fe-41df-be7f-0af7e756f9a9_at_x8g2000yqk.googlegroups.com>


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.

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 Mon Dec 08 2008 - 22:32:35 CET

Original text of this message