Re: Sixth normal form
Date: Fri, 10 Aug 2007 11:55:03 -0000
Message-ID: <1186746903.126913.321140_at_z24g2000prh.googlegroups.com>
On 10 aug, 13:08, Jan Hidders <hidd..._at_gmail.com> wrote:
> On 9 aug, 20:53, vldm10 <vld..._at_yahoo.com> wrote:
>
>
>
> > Although your comments in this thread are knowledgeable and useful I
> > have a few remarks here.
>
> > On Aug 7, 3:30 pm, Jan Hidders <hidd..._at_gmail.com> wrote:
>
> > > On 7 aug, 20:36, vldm10 <vld..._at_yahoo.com> wrote:
>
> > > > On Aug 1, 7:36 am, Jan Hidders <hidd..._at_gmail.com> wrote:
>
> > > > > Any attempt to reformulate it to something easier or more intuitive in
> > > > > my experience almost always ends up with something that is either
> > > > > wrong or actually harder to understand.
>
> > > > > The only somewhat mysterious part may be the "JD is implied by the
> > > > > CKs" but this can be tested by the following simple procedure:
>
> > > > > 1. Let jd be the join dependency we want to test
> > > > > 2. While jd has two elements (being sets of attributes) Si and Sj such
> > > > > that the intersection of Si and Sj contains a candidate key do:
> > > > > 2.1 replace Si and Sj with the union of Si and Sj
> > > > > 3. If jd contains the header of the relation (which is also a set of
> > > > > attributes) then return "yes" else "false"
> > > > > -- Jan Hidders
>
> > > > You gave here the procedure which is more on intuitive level than
> > > > based on some formal system.
>
> > > Although somewhat informally described by me, it is a proper algorithm
> > > and as such *is* a formal system that has been proven both sound and
> > > complete.
>
> > I have a feeling that you didn't pay enough attention to make a
> > distinction between a constructioun (construct) and a formal axiomatic
> > system (FAS). I mean here on construction for 5NF and 6NF, that put
> > "things" in 5NF, 6NF.
>
> Indeed, the algorithm is not a formal axiomatic system, but it is a
> formal system in the broader sense of the word. And if you look
> closely you will see that it is in fact based on a very simple
> axiomatic system whose propositions are JDs and CKs and has one
> inference rule that allows you to derive JDs.
In case anyone's interested:
For a relation with header H (a set of attrbiutes) this formal system
starts with the following axioms:
- JD{H}
- any CKs that hold
Next to the trivial inference rule that says that all axioms are derived there is the following inference rule : (+ denotes set union, * denotes set intersection, <= denotes set inclusion)
IF
1. we derive JD{C_1, ..., C_i, ..., C_m}
2. C_i = D_1 + D_2
3. we derive CK(E)
4. D_1 * D_2 <= E
THEN
we derive JD{C_1, ..., D_1, D_2, ..., C_m}
- Jan Hidders