# 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 - 17:53:41 CEST