# Re: more on delete from join

Date: Tue, 1 Sep 2009 08:53:41 -0700 (PDT)

Message-ID: <91644b56-ebc6-4939-bcd5-fe17a4e0ef50_at_q40g2000prh.googlegroups.com>

On Sep 1, 8:29 am, Tegiri Nenashi <tegirinena..._at_gmail.com> wrote:

*> On Sep 1, 8:03 am, Kevin Kirkpatrick <kvnkrkpt..._at_gmail.com> wrote:*

*>*

*> > Looking at an even simpler example, we encounter the same problem:*

*> > VIEW F := 'E';*

*> > DELETE FROM F {{C2='B'}}**>*

*> > This yields the system of equations*

*> > E = E MINUS {{C2='B'}}**> > which is solved by any of these assignments:*

*> > E := {{}}*

*> > E := {{C2='A'}}*

*> > E := {{C2='A'}, {C2='Q'}}*

*> > ...*

*>*

*> You are correct: the approach should handle at least trivial view*

*> updates. The system of equation is:*

*>*

*> F = E*

*> F minus deltaF = E minus {{C2='B'}}*

*> "deltaF and F have the same set of attributes" -- (that is a*

*> constraint as well!)*

*>*

*> The system is still underspecified for E and F -- the question is if*

*> it is underspecified for deltaF!*

It is nearly to impossible even to express a system of equations in relational algebra or/and set notation. Here is QBQL assertion

x ^ [] = dx ^ [] & -- x and dx have the same header y ^ [] = dy ^ [] & -- y and dy have the same header x = y & -- trivial view definition dx < x & -- try running it without these two dy < y & -- set containment assertions x ^ dx' = x ^ dy' -- the view definition after update-> dx = dy.

If running against Figure1.db it finds no counterexamples. (It finds the system underspecified without set containment assertions!) Next step is proving it with prover9. Here is the RL system of axioms

x ^ y = y ^ x.

(x ^ y) ^ z = x ^ (y ^ z).

x ^ (x v y) = x.

x v y = y v x.

(x v y) v z = x v (y v z).

x v (x ^ y) = x.

x = (x ^ R00) v (x ^ R11).

(x v (y ^ R00)) ^ (y v (x ^ R00))=(x ^ y) v ((x v y) ^ R00).
x ^ (y' ^ z')' = ((x ^ y)' ^ (x ^ z)')'.
R00 ^ (x ^ (y v z)) = R00 ^ ((x ^ y) v (x ^ z)).
x' ^ x = x ^ R00.

x' v x = x v R11.

x < y <-> x ^ y = x.

and the theorem

x ^ R00 = dx ^ R00 &

y ^ R00 = dy ^ R00 &

x = y & dx < x & dy < y &

x ^ dx' = x ^ dy'

-> dx = dy.

proven in 2 sec! Received on Tue Sep 01 2009 - 10:53:41 CDT