 | |
#41
 
| ||||
| ||||
|
Re: Date and McGoveran comments on view updating 'problem' -
12-08-2008
, 06:13 PM
|
Thanks. *Although the relational lattice has seemed a fuzzy to me (no doubt that's my fault as usually takes me years before I feel confident in a mathematical topic), I gather that this example is about "insert" to JOIN. * |
mathematician would certainly label all these view update discussions
and ad-hock rules as "fuzzy". Since you are freely operating within
D&D system of <AND>, <OR>, <NOT> operations, it is not much of
difference to adopt RL; in fact join and negation are the same! The
difference between D&D system and RL is that the authors didn't really
reinforce their algebra with axioms to allow any manipulations.
(Sometime ago I mentioned how these both systems fit together).
As for deletion here is my worksheet. The first two assertions stay
the same:
(SP ^ S') v R00 = R00.
(SP ^ S) ^ R00 = D ^ R00.
Next, we delete one (or several) tuple(s) from S ^ SP, therefore the
delta relation D should be just a subset of the S ^ SP (because we
have already established that S ^ SP and D have the same headers):
D ^ (SP ^ S) = D.
Now, we are proving the following decomposition
(SP v D')^(S v D') = (SP ^ S) v D'.
(in the previous message I forgot to mention that the unary quote
operation is negation).
Again, in Prover9 the deduction is purely mechanical (it took 53 sec
on my machine).
Quote:
|
Just guessing but I gather that RL could be seen as a alternative way of understanding RM, maybe more fundamental in some ways and maybe has some more useful mechanical theoretical tools, so I wonder what happens with "delete" to JOIN (which I believe is the operation that many people find controversial)? |
corresponds to the deletions from the base relations. Therefore, there
is nothing controversial about deletion from join, unless my
assumptions (written formally as equations) are wrong.
Quote:
|
BTW, ever since I first read about it, I've tried to use the TTM algebra in my head because the small and tight definitions make it easier to check my thoughts by comparing results in terms of relations. *But I find most other people tune out when I use them to explain myself. * |
world who buy in this RL stuff:-)
Quote:
|
Also BTW, because I didn't think it affected the problem, I wasn't assuming any foreign key, but if I did I could express the one involving S and SP as: SP{S#} & S{S#} = SP{S#} (where & means <AND>). |
assumptions, and it still derives the deletion assertion! (Certainly,
if I remove one of the other two assertions, the Mace4 finds a
counterexample).
#42
| ||||
| ||||
|
|
Thanks. *Although the relational lattice has seemed a fuzzy to me (no doubt that's my fault as usually takes me years before I feel confident in a mathematical topic), I gather that this example is about "insert" to JOIN. * |
mathematician would certainly label all these view update discussions
and ad-hock rules as "fuzzy". Since you are freely operating within
D&D system of <AND>, <OR>, <NOT> operations, it is not much of
difference to adopt RL; in fact join and negation are the same! The
difference between D&D system and RL is that the authors didn't really
reinforce their algebra with axioms to allow any manipulations.
(Sometime ago I mentioned how these both systems fit together).
As for deletion here is my worksheet. The first two assertions stay
the same:
(SP ^ S') v R00 = R00.
(SP ^ S) ^ R00 = D ^ R00.
Next, we delete one (or several) tuple(s) from S ^ SP, therefore the
delta relation D should be just a subset of the S ^ SP (because we
have already established that S ^ SP and D have the same headers):
D ^ (SP ^ S) = D.
Now, we are proving the following decomposition
(SP v D')^(S v D') = (SP ^ S) v D'.
(in the previous message I forgot to mention that the unary quote
operation is negation).
Again, in Prover9 the deduction is purely mechanical (it took 53 sec
on my machine).
Quote:
|
Just guessing but I gather that RL could be seen as a alternative way of understanding RM, maybe more fundamental in some ways and maybe has some more useful mechanical theoretical tools, so I wonder what happens with "delete" to JOIN (which I believe is the operation that many people find controversial)? |
corresponds to the deletions from the base relations. Therefore, there
is nothing controversial about deletion from join, unless my
assumptions (written formally as equations) are wrong.
Quote:
|
BTW, ever since I first read about it, I've tried to use the TTM algebra in my head because the small and tight definitions make it easier to check my thoughts by comparing results in terms of relations. *But I find most other people tune out when I use them to explain myself. * |
world who buy in this RL stuff:-)
Quote:
|
Also BTW, because I didn't think it affected the problem, I wasn't assuming any foreign key, but if I did I could express the one involving S and SP as: SP{S#} & S{S#} = SP{S#} (where & means <AND>). |
assumptions, and it still derives the deletion assertion! (Certainly,
if I remove one of the other two assertions, the Mace4 finds a
counterexample).
#43
| ||||
| ||||
|
|
Thanks. *Although the relational lattice has seemed a fuzzy to me (no doubt that's my fault as usually takes me years before I feel confident in a mathematical topic), I gather that this example is about "insert" to JOIN. * |
mathematician would certainly label all these view update discussions
and ad-hock rules as "fuzzy". Since you are freely operating within
D&D system of <AND>, <OR>, <NOT> operations, it is not much of
difference to adopt RL; in fact join and negation are the same! The
difference between D&D system and RL is that the authors didn't really
reinforce their algebra with axioms to allow any manipulations.
(Sometime ago I mentioned how these both systems fit together).
As for deletion here is my worksheet. The first two assertions stay
the same:
(SP ^ S') v R00 = R00.
(SP ^ S) ^ R00 = D ^ R00.
Next, we delete one (or several) tuple(s) from S ^ SP, therefore the
delta relation D should be just a subset of the S ^ SP (because we
have already established that S ^ SP and D have the same headers):
D ^ (SP ^ S) = D.
Now, we are proving the following decomposition
(SP v D')^(S v D') = (SP ^ S) v D'.
(in the previous message I forgot to mention that the unary quote
operation is negation).
Again, in Prover9 the deduction is purely mechanical (it took 53 sec
on my machine).
Quote:
|
Just guessing but I gather that RL could be seen as a alternative way of understanding RM, maybe more fundamental in some ways and maybe has some more useful mechanical theoretical tools, so I wonder what happens with "delete" to JOIN (which I believe is the operation that many people find controversial)? |
corresponds to the deletions from the base relations. Therefore, there
is nothing controversial about deletion from join, unless my
assumptions (written formally as equations) are wrong.
Quote:
|
BTW, ever since I first read about it, I've tried to use the TTM algebra in my head because the small and tight definitions make it easier to check my thoughts by comparing results in terms of relations. *But I find most other people tune out when I use them to explain myself. * |
world who buy in this RL stuff:-)
Quote:
|
Also BTW, because I didn't think it affected the problem, I wasn't assuming any foreign key, but if I did I could express the one involving S and SP as: SP{S#} & S{S#} = SP{S#} (where & means <AND>). |
assumptions, and it still derives the deletion assertion! (Certainly,
if I remove one of the other two assertions, the Mace4 finds a
counterexample).
#44
| ||||
| ||||
|
|
Thanks. *Although the relational lattice has seemed a fuzzy to me (no doubt that's my fault as usually takes me years before I feel confident in a mathematical topic), I gather that this example is about "insert" to JOIN. * |
mathematician would certainly label all these view update discussions
and ad-hock rules as "fuzzy". Since you are freely operating within
D&D system of <AND>, <OR>, <NOT> operations, it is not much of
difference to adopt RL; in fact join and negation are the same! The
difference between D&D system and RL is that the authors didn't really
reinforce their algebra with axioms to allow any manipulations.
(Sometime ago I mentioned how these both systems fit together).
As for deletion here is my worksheet. The first two assertions stay
the same:
(SP ^ S') v R00 = R00.
(SP ^ S) ^ R00 = D ^ R00.
Next, we delete one (or several) tuple(s) from S ^ SP, therefore the
delta relation D should be just a subset of the S ^ SP (because we
have already established that S ^ SP and D have the same headers):
D ^ (SP ^ S) = D.
Now, we are proving the following decomposition
(SP v D')^(S v D') = (SP ^ S) v D'.
(in the previous message I forgot to mention that the unary quote
operation is negation).
Again, in Prover9 the deduction is purely mechanical (it took 53 sec
on my machine).
Quote:
|
Just guessing but I gather that RL could be seen as a alternative way of understanding RM, maybe more fundamental in some ways and maybe has some more useful mechanical theoretical tools, so I wonder what happens with "delete" to JOIN (which I believe is the operation that many people find controversial)? |
corresponds to the deletions from the base relations. Therefore, there
is nothing controversial about deletion from join, unless my
assumptions (written formally as equations) are wrong.
Quote:
|
BTW, ever since I first read about it, I've tried to use the TTM algebra in my head because the small and tight definitions make it easier to check my thoughts by comparing results in terms of relations. *But I find most other people tune out when I use them to explain myself. * |
world who buy in this RL stuff:-)
Quote:
|
Also BTW, because I didn't think it affected the problem, I wasn't assuming any foreign key, but if I did I could express the one involving S and SP as: SP{S#} & S{S#} = SP{S#} (where & means <AND>). |
assumptions, and it still derives the deletion assertion! (Certainly,
if I remove one of the other two assertions, the Mace4 finds a
counterexample).
#45
| ||||
| ||||
|
|
Thanks. *Although the relational lattice has seemed a fuzzy to me (no doubt that's my fault as usually takes me years before I feel confident in a mathematical topic), I gather that this example is about "insert" to JOIN. * |
mathematician would certainly label all these view update discussions
and ad-hock rules as "fuzzy". Since you are freely operating within
D&D system of <AND>, <OR>, <NOT> operations, it is not much of
difference to adopt RL; in fact join and negation are the same! The
difference between D&D system and RL is that the authors didn't really
reinforce their algebra with axioms to allow any manipulations.
(Sometime ago I mentioned how these both systems fit together).
As for deletion here is my worksheet. The first two assertions stay
the same:
(SP ^ S') v R00 = R00.
(SP ^ S) ^ R00 = D ^ R00.
Next, we delete one (or several) tuple(s) from S ^ SP, therefore the
delta relation D should be just a subset of the S ^ SP (because we
have already established that S ^ SP and D have the same headers):
D ^ (SP ^ S) = D.
Now, we are proving the following decomposition
(SP v D')^(S v D') = (SP ^ S) v D'.
(in the previous message I forgot to mention that the unary quote
operation is negation).
Again, in Prover9 the deduction is purely mechanical (it took 53 sec
on my machine).
Quote:
|
Just guessing but I gather that RL could be seen as a alternative way of understanding RM, maybe more fundamental in some ways and maybe has some more useful mechanical theoretical tools, so I wonder what happens with "delete" to JOIN (which I believe is the operation that many people find controversial)? |
corresponds to the deletions from the base relations. Therefore, there
is nothing controversial about deletion from join, unless my
assumptions (written formally as equations) are wrong.
Quote:
|
BTW, ever since I first read about it, I've tried to use the TTM algebra in my head because the small and tight definitions make it easier to check my thoughts by comparing results in terms of relations. *But I find most other people tune out when I use them to explain myself. * |
world who buy in this RL stuff:-)
Quote:
|
Also BTW, because I didn't think it affected the problem, I wasn't assuming any foreign key, but if I did I could express the one involving S and SP as: SP{S#} & S{S#} = SP{S#} (where & means <AND>). |
assumptions, and it still derives the deletion assertion! (Certainly,
if I remove one of the other two assertions, the Mace4 finds a
counterexample).
#46
| ||||
| ||||
|
|
Thanks. *Although the relational lattice has seemed a fuzzy to me (no doubt that's my fault as usually takes me years before I feel confident in a mathematical topic), I gather that this example is about "insert" to JOIN. * |
mathematician would certainly label all these view update discussions
and ad-hock rules as "fuzzy". Since you are freely operating within
D&D system of <AND>, <OR>, <NOT> operations, it is not much of
difference to adopt RL; in fact join and negation are the same! The
difference between D&D system and RL is that the authors didn't really
reinforce their algebra with axioms to allow any manipulations.
(Sometime ago I mentioned how these both systems fit together).
As for deletion here is my worksheet. The first two assertions stay
the same:
(SP ^ S') v R00 = R00.
(SP ^ S) ^ R00 = D ^ R00.
Next, we delete one (or several) tuple(s) from S ^ SP, therefore the
delta relation D should be just a subset of the S ^ SP (because we
have already established that S ^ SP and D have the same headers):
D ^ (SP ^ S) = D.
Now, we are proving the following decomposition
(SP v D')^(S v D') = (SP ^ S) v D'.
(in the previous message I forgot to mention that the unary quote
operation is negation).
Again, in Prover9 the deduction is purely mechanical (it took 53 sec
on my machine).
Quote:
|
Just guessing but I gather that RL could be seen as a alternative way of understanding RM, maybe more fundamental in some ways and maybe has some more useful mechanical theoretical tools, so I wonder what happens with "delete" to JOIN (which I believe is the operation that many people find controversial)? |
corresponds to the deletions from the base relations. Therefore, there
is nothing controversial about deletion from join, unless my
assumptions (written formally as equations) are wrong.
Quote:
|
BTW, ever since I first read about it, I've tried to use the TTM algebra in my head because the small and tight definitions make it easier to check my thoughts by comparing results in terms of relations. *But I find most other people tune out when I use them to explain myself. * |
world who buy in this RL stuff:-)
Quote:
|
Also BTW, because I didn't think it affected the problem, I wasn't assuming any foreign key, but if I did I could express the one involving S and SP as: SP{S#} & S{S#} = SP{S#} (where & means <AND>). |
assumptions, and it still derives the deletion assertion! (Certainly,
if I remove one of the other two assertions, the Mace4 finds a
counterexample).
#47
| |||
| |||
|
|
paul c wrote: ... so I wonder what happens with "delete" to JOIN (which I believe is the operation that many people find controversial)? ... Just as they find "insert" to UNION. *The main argument seems to be that the operation is not deterministic when trying to decide on a base table by base table basis what to change, ie., there are three combinations of base values that could produce the same tuple in a view. *McGoveran seemed to be saying that this argument is the wrong one, doesn't take in all available information because it manipulates extensions without concern as to the implications of the predicates and values involved before the insert or delete is tried. |
M - Males
F - Femails
D - Delta of M v F
The assertions:
1. M disjunct to F
(M ^ F) ^ R00 = R00.
This may be not necessary, although we'll demonstrate that we won't be
able to derive view update even under this additional assertion.
2. M and F having the same headers
M ^ R00 = F ^ R00.
3. D and F having the same headers
D ^ R00 = F ^ R00.
4. Added tuples (D) are disjoint with F
(D ^ F) ^ R00 = R00.
5. Added tuples are disjoint with M
(D ^ M) ^ R00 = R00.
It *doesn't* follow that we can insert D into M
M v D = (M v F) v D.
This is, again, established by Mace4 finding a two element
counterexample.
Quote:
|
It just seemed to me that if one started with the algebra and could somehow gauge all possible expressions as to what their resulting relations would be, one might find that McGoveran is right and if not, show that the problem is more complicated than he suggested. *It also seemed to me that for such an exercise, if one had the right mental machinery, one could ignore the practical restrictions that are usually followed, such as common headings for union and run-time exceptions that some think will confuse dumb users. |
#48
| |||
| |||
|
|
paul c wrote: ... so I wonder what happens with "delete" to JOIN (which I believe is the operation that many people find controversial)? ... Just as they find "insert" to UNION. *The main argument seems to be that the operation is not deterministic when trying to decide on a base table by base table basis what to change, ie., there are three combinations of base values that could produce the same tuple in a view. *McGoveran seemed to be saying that this argument is the wrong one, doesn't take in all available information because it manipulates extensions without concern as to the implications of the predicates and values involved before the insert or delete is tried. |
M - Males
F - Femails
D - Delta of M v F
The assertions:
1. M disjunct to F
(M ^ F) ^ R00 = R00.
This may be not necessary, although we'll demonstrate that we won't be
able to derive view update even under this additional assertion.
2. M and F having the same headers
M ^ R00 = F ^ R00.
3. D and F having the same headers
D ^ R00 = F ^ R00.
4. Added tuples (D) are disjoint with F
(D ^ F) ^ R00 = R00.
5. Added tuples are disjoint with M
(D ^ M) ^ R00 = R00.
It *doesn't* follow that we can insert D into M
M v D = (M v F) v D.
This is, again, established by Mace4 finding a two element
counterexample.
Quote:
|
It just seemed to me that if one started with the algebra and could somehow gauge all possible expressions as to what their resulting relations would be, one might find that McGoveran is right and if not, show that the problem is more complicated than he suggested. *It also seemed to me that for such an exercise, if one had the right mental machinery, one could ignore the practical restrictions that are usually followed, such as common headings for union and run-time exceptions that some think will confuse dumb users. |
#49
| |||
| |||
|
|
paul c wrote: ... so I wonder what happens with "delete" to JOIN (which I believe is the operation that many people find controversial)? ... Just as they find "insert" to UNION. *The main argument seems to be that the operation is not deterministic when trying to decide on a base table by base table basis what to change, ie., there are three combinations of base values that could produce the same tuple in a view. *McGoveran seemed to be saying that this argument is the wrong one, doesn't take in all available information because it manipulates extensions without concern as to the implications of the predicates and values involved before the insert or delete is tried. |
M - Males
F - Femails
D - Delta of M v F
The assertions:
1. M disjunct to F
(M ^ F) ^ R00 = R00.
This may be not necessary, although we'll demonstrate that we won't be
able to derive view update even under this additional assertion.
2. M and F having the same headers
M ^ R00 = F ^ R00.
3. D and F having the same headers
D ^ R00 = F ^ R00.
4. Added tuples (D) are disjoint with F
(D ^ F) ^ R00 = R00.
5. Added tuples are disjoint with M
(D ^ M) ^ R00 = R00.
It *doesn't* follow that we can insert D into M
M v D = (M v F) v D.
This is, again, established by Mace4 finding a two element
counterexample.
Quote:
|
It just seemed to me that if one started with the algebra and could somehow gauge all possible expressions as to what their resulting relations would be, one might find that McGoveran is right and if not, show that the problem is more complicated than he suggested. *It also seemed to me that for such an exercise, if one had the right mental machinery, one could ignore the practical restrictions that are usually followed, such as common headings for union and run-time exceptions that some think will confuse dumb users. |
#50
| |||
| |||
|
|
paul c wrote: ... so I wonder what happens with "delete" to JOIN (which I believe is the operation that many people find controversial)? ... Just as they find "insert" to UNION. *The main argument seems to be that the operation is not deterministic when trying to decide on a base table by base table basis what to change, ie., there are three combinations of base values that could produce the same tuple in a view. *McGoveran seemed to be saying that this argument is the wrong one, doesn't take in all available information because it manipulates extensions without concern as to the implications of the predicates and values involved before the insert or delete is tried. |
M - Males
F - Femails
D - Delta of M v F
The assertions:
1. M disjunct to F
(M ^ F) ^ R00 = R00.
This may be not necessary, although we'll demonstrate that we won't be
able to derive view update even under this additional assertion.
2. M and F having the same headers
M ^ R00 = F ^ R00.
3. D and F having the same headers
D ^ R00 = F ^ R00.
4. Added tuples (D) are disjoint with F
(D ^ F) ^ R00 = R00.
5. Added tuples are disjoint with M
(D ^ M) ^ R00 = R00.
It *doesn't* follow that we can insert D into M
M v D = (M v F) v D.
This is, again, established by Mace4 finding a two element
counterexample.
Quote:
|
It just seemed to me that if one started with the algebra and could somehow gauge all possible expressions as to what their resulting relations would be, one might find that McGoveran is right and if not, show that the problem is more complicated than he suggested. *It also seemed to me that for such an exercise, if one had the right mental machinery, one could ignore the practical restrictions that are usually followed, such as common headings for union and run-time exceptions that some think will confuse dumb users. |
 |
« Previous Thread
|
Next Thread »
| Thread Tools | |
| Display Modes | |
Linear Mode
| |
Powered by vBulletin Version 3.5.3
Copyright ©2000 - 2012, Jelsoft Enterprises Ltd.
Copyright ©2000 - 2012, Jelsoft Enterprises Ltd.