Re: more on delete from join
From: Vadim Tropashko <vadimtro_at_gmail.com>
Date: Tue, 1 Sep 2009 10:31:10 -0700 (PDT)
Message-ID: <702ac6ee-38bb-4a08-ae71-d4cfb30d5cc7_at_d15g2000prc.googlegroups.com>
(x ^ y) ^ dz' = (x ^ dx') ^ (y ^ dy') -- View definition after update
-> dx = dz v (x^[]) | dy = dz v (y^[]).
Note: I didn't introduce the relvar z for the view z = x ^ y because one extra variable would cause slower assertion evaluation: QBQL substitutes all the variables with tables from the database definition file).
Date: Tue, 1 Sep 2009 10:31:10 -0700 (PDT)
Message-ID: <702ac6ee-38bb-4a08-ae71-d4cfb30d5cc7_at_d15g2000prc.googlegroups.com>
Returning to the main theme of the thread here is delete from join system of equations:
x ^ [] = dx ^ [] & -- x and dx have the same header y ^ [] = dy ^ [] & -- y and dy have the same header x ^ y ^ [] = dz ^ [] & -- y ^ x and dz have the same header dx < x & -- Try running it without these 3 dy < y & -- set containment assertions dz < (x ^ y) & --
(x ^ y) ^ dz' = (x ^ dx') ^ (y ^ dy') -- View definition after update
-> dx = dz v (x^[]) | dy = dz v (y^[]).
Legend:
x ^ y -- join of x and y
x v (y ^ []) -- projection of x onto the set of attributes of the
relvar y
x' -- complement of x
x < y -- (generalized) set containment
& -- logical AND (as in Prover9) | -- logical OR (as in Prover9) -> -- implication (as in Prover9)
Note: I didn't introduce the relvar z for the view z = x ^ y because one extra variable would cause slower assertion evaluation: QBQL substitutes all the variables with tables from the database definition file).
Here is the counterexample produced by QBQL:
dx = [p]
1
;
dy = [p]
0
;
dz = [p]
;
y = [p]
0
;
x = [p]
1
;
Therefore, unless we add more constraints the join view is not updatable. Received on Tue Sep 01 2009 - 19:31:10 CEST