Oracle FAQ Your Portal to the Oracle Knowledge Grid
 HOME | ASK QUESTION | ADD INFO | SEARCH | E-MAIL US

Home -> Community -> Usenet -> comp.databases.theory -> Vadim Tropashko = Aloha Kakuikanu?

# Vadim Tropashko = Aloha Kakuikanu?

From: Brian Selzer <brian_at_selzer-software.com>
Date: Mon, 25 Jun 2007 23:24:43 GMT
Message-ID: <%8Yfi.2333\$K44.10@newssvr13.news.prodigy.net>

Strange that this text is almost identical to the previous one posted under a different name.

> On Jun 25, 12:56 pm, Jan Hidders <hidd..._at_gmail.com> wrote:

```>> > >  (7)     r * {()} = r
>> > >  (13)   {()} = {()} + []
>>
>> > >  Special distribution equalities:
>>
>> > >  (8)   r * (s + t) = (r * s) + (r * t)
>> > >         if  A(r) * A(s) <= A(t)  or A(r) * A(t) <= A(s)
>> > >  (9)   r + (s * t) = (r + s) * (r + t)
>> > >         if  A(s) * A(t) <= A(r)
>>
>> > >  Absorption:
>>
>> > >  (20)   r + (r * s) = r
>> > >  (21)   r * (r + s) = r
>>
>> > >  Empty relations:
>>
>> > >  (10)   R = R + [H]
>> > >          if H is the header of R
>> > >  (11)   [H] * [S] = [H + S]
>> > >  (12)   [H] + [S] = [H * S]
>> > >  (22)   R * [] = [H]
>> > >          if H is the header of R
>>
>> > You have informal "H is the header of R" in many places. Why don't we
>> > use this axiom as a definition of [H]? Then, we just substitute [H]
>> > with R * [].
>>
>> Well, I would not say it is informal. It has a precise meaning since
>> we can assume that we know the database schema, and given that schema
>> you can see which axioms are generated by the axiom schemas.
>
```

> So you have axiom schemas, instead of a single axiom system? I don't
> challenge this approach, but think that a single axiom system is
> workable as well (see below).
```>
>> Your suggestion might work, but you would have to first formalize what
>> your inference mechanism is before we can start thinking about it.
>> Right now my formalism is quite simple. It derives r = s iff it can
>> rewrite r to s with the given axioms. Yours would probably be much
>> more complicated than that. Can you give a formal definition of yours?
>
```

> OK, I have relation variables, 5 constants 00, 01, 10, 11, 1E, and two
> binary operations \/, /\, and the inequlity Y <= X abbreviation for X /
> \ Y = X. Axioms:
```>
```

> 1-8. Lattice axioms
> 9. Spight criteria:
> (R/\00) \/ (S/\00) <= Q/\00 and (R/\00) \/ (Q/\00) <= S/\00 implies
> (R /\ S) \/ (R /\ Q) = R /\ (S \/ Q)
> 10. (R/\00) \/ (Q/\00) <= R/\00 implies
> (R /\ S) /\ (R \/ Q) = R \/ (S /\ Q)
> 11. 01 <= R <= 10
> 12. R = (00 /\ R) \/ (11 /\ R)
> 13. Universal equality relation 1E axioms.
```>
```

> Do you imply that I can't reduce both sides of the expression R = S to
> the Union Normal Form in this system?
```>
>> > Also given that we agreed not to introduce operator precedence, the RL
>> > expressions contain a lot of parenthesis. Therefore, introducing
>> > constants which include brackets is not the best choice.
>>
>> They are sets, so I need to put something around them. :-) Seriously,
>> I don't see what else I could do. Note that in a real expression there
>> would be things like <a,b,c> and [b,c,e]. How do you want me to write
>> that without brackets?
>
```

> [b,c,e] = B /\ C /\ E /\ 00
```>
```

> <a,b,c> = 1E \/ (B /\ C /\ E /\ 00)
```>
```

> where 1E is the universal equality relation. Once again your brakets
> are clever abbreviations, but they are not fundamental.
```>
>> > The [] brakets are very convenient when we want to specify relation
>> > arguments explicitly, e.g [x,y]. In the algebraic context relation
>> > header is just  R * 00
>>
>> .. under the assumption that the header of R is {x,y}, and such
>> assumptions we cannot use in our inference mechanism. Again, we could
>> move to such an inference mechanism but we would have to formalize it.
>
```

> ?? When we write R /\ 00, there is no x and y mentioned anywhere.
```>
>> > >   Equalities
>>
>> > >   (27)  <H> * <S> = <H + S>
>> > >   (28)  R * <x> = R
>> > >          if x in header H (NOTE x is a single attribute)
>>
>> > I don't see why it is an equality axiom. The <x> is unary relation
>> > which is domain x.
>>
>> Yes, it corresponds to the equation x=x, but the grouping of the
>> axioms is just to give it some structure.
>> > And also you have informal note. Once again you can express the
>> > condition that the relation R is a single attribute relation as
>>
>> > 00 <= X <= R /\ 00    implies   X = 00 or X = R /\ 00
>>
>> Yes, but again this means that you extend your inference mechanism,
>> namely with first order logic inference.
>
```

> OK, if this is a critical showstopper, then I would have to introduce
> single attribute relations, conveniently designated with small letters
> r,s,t etc. Your rule #28, for example becomes
```>
```

> 28. x /\ 00 <= R /\ 00 implies
> R /\ ((x /\ 00) \/ 1E) = R
```>
```

> The (informal) implication is there in both systems yours and mine,
> there is no way around it.
```>
>> Again, this requires that you
>> first define this formally, and even then I would still be inclined to
>> come up with a proof for the simpeler inference mechanisme first. Note
>> that once you have that, you can probably from that derive proofs for
>> more complicated inference mechanisms.
>>
>> > >   (30)  <> = {()}
>
```

> This is a theorem, not axiom.
```>
```

> <> = 00 \/ 1E = 01 = {()}
```>
```

> It follows from the 1E being non empty. 1E is not empty because if it
> is empty then for non empty R the left side of
```>
```

> R /\ ((x /\ 00) \/ 1E) = R
```>
```

> evaluates to empty relation.
```>
```

> Oh, yeah, the empty relation is formalized as follows
```>
```

> R \/ 00 = 00 iff R empty
> R \/ 00 = 01 iff R nonempty
```>
>> > >  Miscellaneous
>>
>> > >   (26)  <H> + [S] = <H * S>
>> > >   (29)  [H] * <S> = [H + S]
>> > >   (31)  ((r * <S>) + [H]) * <S> = ((r * <S>) + [H'])
>> > >          if S * H nonempty and H + S = H'
>>
>> > You have to specify that headers of <S> and r overlap on no more than
>> > a single attribute -- and I don't see this condition here.
>>
>> Why do you think that condition is necessary?
>
```

> OK, I see that you slightly modified the equality axiom. Can you
```>
```

> (((R(x,y) * <yz>) + [xz]) * <yz>) + [xy] = R(x,y)
```>
```