Re: more on delete from join

From: Vadim Tropashko <vadimtro_at_gmail.com>
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