(Msg. 31) Posted: Mon Jun 25, 2007 2:19 pm
Post subject: Re: completeness of the relational lattice [Login to view extended thread Info.] Archived from groups: comp>databases>theory (more info?)

On Jun 24, 4:32 pm, Jan Hidders wrote:
> > Let R(u,w), S(u), Q(w), T(V), P(u,v), then we can't apply
> > distributivity to simplify
>
> > ( (R /\ (S \/ Q)) \/ T ) /\ P
>
> This is solved by the extra rules for [H]. These allow me to make the
> attributes of an expression explicit by rewriting it to r \/ [H] where
> H contains all attributes of r. That means that in the above you can
> rewrite S \/ Q to (S \/ [H1]) \/ (Q \/ [H2]) which in turn can be
> rewritten to (S \/ [H1*H2]) \/ (Q \/ [H1*H2]). By then distribtivity
> will apply.

OK, the nesting remains, although we have simpler conjunctive clauses.
For example, assuming
R(u,w), S(u,t), Q(w,t), T(v,t), P(u,v) the expression

( (R /\ (S \/ Q) ) \/ T ) /\ P

"simplifies" to a union normal form:

( ( (R /\ (S \/ [t])) \/ [t] ) /\ P ) \/
( ( (R /\ (Q \/ [t])) \/ [t] ) /\ P ) \/
( (T \/ [t]) /\ P )

This is indeed something new.

> What it should have said is that
> every expression r that returns always an empty result can be
> rewritten to [A(r)] where A is the function that give the attribute
> set of the result.

I assume you have to know if each relation in the expression is empty
or not. Then exvaluating the emptiness of the result is just a matter
of evaluating boolean expression. In the example above suppose
R - empty,
S - empty,
Q - non empty,
T - empty,
P - non empty

( (0 /\ (0 \/ 1) ) \/ 0 ) /\ 1 = 0

The issue becomes much less obvious when we introduce negation/
difference/division.

> We consider the following algebra:
>
> E ::= R | E * E | E + E | {()} | [H] | 'x=y'
>
> Where:
> - R : a relation with name R (and known header)
> - E * E : natural join
> - E + E : generalized union
> - {()} : the relation with empty header and a single empty tuple
> - [H] : the empty relation with header H (possibly empty)
> - 'x=y' : the relation { (x=a, y=b) | a in D, b in D, a=b }
>
> The * and + will also be used as intersection and union on sets of
> attributes.
>
> We define a function A that computes the header of the result:
> - A(R) = H where H is the header of R
> - A(r * s) = A(r) + A(s)
> - A(r + s) = A(r) * A(s)
> - A({()}) = {}
> - A([H]) = H
> - A('x=y') = {x,y}
>
> Standard equalities:
>
> (1) r * r = r
> (2) r * s = s * r
> (3) r * (s * t) = (r * s) * t
>
> (4) r + r = r
> (5) r + s = s + r
> (6) r + (s + t) = (r + s) + t
>
> (7) r * {()} = r
> (13) {()} = {()} + []
>
> Special distribution equalities:
>
> ( r * (s + t) = (r * s) + (r * t) if A(r) * A(s) <= A(t) or
> A(r) * A(t) <= A(s)

"and", not "or". I like the distributivity critera in this form!

> (9) r + (s * t) = (r + s) * (r + t) if A(s) * A(t) <= A(r)

Even more so...

> Absorption:
>
> (20) r + (r * s) = r
> (21) r * (r + s) = r
>
> Empty relations:
>
> (14) 'x=y' = 'x=y' + [x,y]
> (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
>
> Equalities
>
> (15) 'x=y' = 'x=y' * 'x=x'
> (16) 'x=y' = 'x=y' * 'y=x'
> (17) 'x=y' * 'y=z' = 'x=y' * 'y=z' * 'x=z'
> (18a) R * 'x=x' = R if x in header R
>
> Miscellaneous
>
> (18b) [] * 'x=y' = [x,y]
> (18c) 'x=y' + [H] = 'x=x' if x in H and y not in H
> (19) 'x=y' + [] = {()}
> (24) ((r * 'x=y') + [H]) * 'x=y' = ((r * 'x=y') + [H + {y}]) if x
> in H

(Msg. 32) Posted: Mon Jun 25, 2007 3:04 pm
Post subject: Re: completeness of the relational lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

On Jun 25, 5:34 am, Jan Hidders wrote:
> Hello Marshall and Vadim,
>
> The axioms for equality axioms looked a bit ugly, so I wondered if
> that could be improved. I think we can if we introduce in analogy to
> [H] the operation <H> which denotes the relation with header H that
> contains all tuples of the form (x,x,..,x).
>
> The syntax:
>
> E ::= R | E * E | E + E | {()} | [H] | <H>
>
> If we adapt the equations we get:
>
> Standard equalities:
>
> (1) r * r = r
> (2) r * s = s * r
> (3) r * (s * t) = (r * s) * t
>
> (4) r + r = r
> (5) r + s = s + r
> (6) r + (s + t) = (r + s) + t
>
> (7) r * {()} = r
> (13) {()} = {()} + []
>
> Special distribution equalities:
>
> ( 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 * [].

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.

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.

> Equalities
>
> (27) <H> * <S> = <H + S>
> (2 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.

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

> (30) <> = {()}
>
> 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.

(Msg. 33) Posted: Mon Jun 25, 2007 4:34 pm
Post subject: Re: completeness of the relational lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

Hello Marshall and Vadim,

The axioms for equality axioms looked a bit ugly, so I wondered if
that could be improved. I think we can if we introduce in analogy to
[H] the operation <H> which denotes the relation with header H that
contains all tuples of the form (x,x,..,x).

The syntax:

E ::= R | E * E | E + E | {()} | [H] | <H>

If we adapt the equations we get:

Standard equalities:

(1) r * r = r
(2) r * s = s * r
(3) r * (s * t) = (r * s) * t

(4) r + r = r
(5) r + s = s + r
(6) r + (s + t) = (r + s) + t

(7) r * {()} = r
(13) {()} = {()} + []

Special distribution equalities:

( 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

Equalities

(27) <H> * <S> = <H + S>
(2 R * <x> = R
if x in header H (NOTE x is a single attribute)
(30) <> = {()}

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'

(Msg. 34) Posted: Mon Jun 25, 2007 7:17 pm
Post subject: Re: completeness of the relational lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

On Jun 25, 12:56 pm, Jan Hidders wrote:
> > > (7) r * {()} = r
> > > (13) {()} = {()} + []
>
> > > Special distribution equalities:
>
> > > ( 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 ont
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
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. Equality 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>
> > > (2 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
please derive

(Msg. 35) Posted: Mon Jun 25, 2007 7:29 pm
Post subject: Re: completeness of the relational lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

On Jun 25, 12:56 pm, Jan Hidders wrote:
> > > (7) r * {()} = r
> > > (13) {()} = {()} + []
>
> > > Special distribution equalities:
>
> > > ( 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>
> > > (2 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
please derive

(Msg. 36) Posted: Tue Jun 26, 2007 12:56 am
Post subject: Re: completeness of the relational lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

On 25 jun, 20:04, Vadim Tropashko wrote:
> On Jun 25, 5:34 am, Jan Hidders wrote:
>
>
>
> > Hello Marshall and Vadim,
>
> > The axioms for equality axioms looked a bit ugly, so I wondered if
> > that could be improved. I think we can if we introduce in analogy to
> > [H] the operation <H> which denotes the relation with header H that
> > contains all tuples of the form (x,x,..,x).
>
> > The syntax:
>
> > E ::= R | E * E | E + E | {()} | [H] | <H>
>
> > If we adapt the equations we get:
>
> > Standard equalities:
>
> > (1) r * r = r
> > (2) r * s = s * r
> > (3) r * (s * t) = (r * s) * t
>
> > (4) r + r = r
> > (5) r + s = s + r
> > (6) r + (s + t) = (r + s) + t
>
> > (7) r * {()} = r
> > (13) {()} = {()} + []
>
> > Special distribution equalities:
>
> > ( 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.

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?

> 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?

> 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.

> > Equalities
>
> > (27) <H> * <S> = <H + S>
> > (2 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. 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) <> = {()}
>
> > 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?

By the way, I may also some other good news. I looked briefly at the
problem of the infinitely wide relations, and it seems that is not so
difficult to solve. The reason is that any expression r that returns
an infinitely wide result can be rewritten to r' * W where W is my
version of 11, (W as in "wide" and omega) with r' an expression
without W. Since for such expressions s' * W and r' * W it holds that
they are equivalent iff s' and r' are equivalent, this means that we
can reduce this problem to deciding equivalence for the finitely wide
expressions. I actually only needed one extra axiom for this:

(32) W + [x] = <x> with x a single attribute

With things seeming to go relatively well I also became a bit more
interested in the next step. Could we for example also axiomatize
complement (and thereby the whole of first order logic)?

I came up with a few axioms, but have no idea if they are complete:

(34) ~R + R = W + [H] if H header of R
(35) ~R * R = [H] if H header of R

These axioms seem complete in the sense that the only possible
interpretatoin is the complement operator, but that doesn't prove that
as inference rules they are complete.

(Msg. 37) Posted: Tue Jun 26, 2007 3:24 am
Post subject: Vadim Tropashko = Aloha Kakuikanu? [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

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

"Vadim Tropashko" wrote in message

> On Jun 25, 12:56 pm, Jan Hidders wrote:
>> > > (7) r * {()} = r
>> > > (13) {()} = {()} + []
>>
>> > > Special distribution equalities:
>>
>> > > ( 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>
>> > > (2 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
> please derive
>
> (((R(x,y) * <yz>) + [xz]) * <yz>) + [xy] = R(x,y)
>
> in your system?
>
> >> Stay informed about: completeness of the relational lattice

(Msg. 38) Posted: Tue Jun 26, 2007 4:53 am
Post subject: Re: completeness of the relational lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

On Jun 26, 12:29 am, Vadim Tropashko
wrote:
> On Jun 25, 12:56 pm, Jan Hidders wrote:
>
>
>
> > > > (7) r * {()} = r
> > > > (13) {()} = {()} + []
>
> > > > Special distribution equalities:
>
> > > > ( 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).

It's a schema anyway because you still have relation variables.
Although I agree that I need two types of variables, or three if you
count the singleton attributes, and you have one (or two if you have
special ones for singleton sets, as you suggest later). On the other
hand, I only have equations, and you need propositional formulas over
equation.

> > 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.

You found those already?

> Do you imply that I can't reduce both sides of the expression R = S to
> the Union Normal Form in this system?

I don't know, you've onlly given axioms and not the inference
mechanism. Since they are propositional formulas I assume you want to
use propositional calculus. If you add this you can no longer claim
that you have a pure algebraic axiomatization, which makes the
completeness claim less interesting. But is propositional calculus all
you allow, or are you also allowing reasoning by rewriting? The latter
can be captured in either your inference mechanism or by adding adding
extra axioms (e.g. the rules "if R = R' and S = S' then R /\ S = R' /\
S'" and "if R = S and S= T then S = T" and ... ). There is the usual
trade off between putting your inference in the axioms or in the
inference mechanism. So how do you want do that? And yes, I want a
full formal specification of that. You cannot write a paper on the
completeness of some reasoning system and not specify formally its
inference mechanism. Note by the way that this changes the notion of
"complete" because it then not only means that you can derive all
equations that hold, but in fact that you can derive all propositional
formulas (including negations) over equations that hold. I have no
idea how to prove that. Do you?

Btw. what I did wonder about is how you would derive "if R1(x,y) /\ 00
= R1(x,y) and R2(x,y) /\ 00 = R2(x,y) then R1(x,y) /\ [] = R2(x,y) /\
[]".

> > 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

Ok. I think that would work. But also here you have to say how the
inference deals with this. How does it know what and what not to match
x with when it rewrites? This is solvable, but again it adds
complexity to the inference mechanism.

> The (informal) implication is there in both systems yours and mine,
> there is no way around it.

Of course. But the difference is that I have fully formally specified
what my system is (the axioms *and* the inference mechanism) and you
have not. Moreover it seems that you want to push a lot of the
complexity into the inference mechanism in order to keep you set of
axioms simple. As I already said, that makes the completeness claim at
the same time harder to prove, and less interesting.

> > > > (30) <> = {()}
>
> This is a theorem, not axiom.

Yes, in your inference mechanism, but not in mine. So I need it.

> > > > 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
> please derive
>
> (((R(x,y) * <yz>) + [xz]) * <yz>) + [xy] = R(x,y)
>
> in your system?

(Msg. 39) Posted: Tue Jun 26, 2007 2:55 pm
Post subject: Re: completeness of the relational lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

On Jun 26, 12:53 am, Jan Hidders wrote:
> On Jun 26, 12:29 am, Vadim Tropashko
> > 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).
>
> It's a schema anyway because you still have relation variables.
> Although I agree that I need two types of variables, or three if you
> count the singleton attributes, and you have one (or two if you have
> special ones for singleton sets, as you suggest later). On the other
> hand, I only have equations, and you need propositional formulas over
> equation.

I'm not sure I understand. I see "if" all over the place in your axiom
system -- you must have propositions there as well. I had a quantifier
in one place where I wanted to introduce atomic attribute, but this
can be avoided (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.
>
> You found those already?

Let's translate your axioms 26-31 in terms of 1E (no special meaning
of square brackets in my notation other than easy reading):

[H] * <S> = (def)
[H /\ 00] /\ (1E \/ [S /\ 00]) = (idemp, assoc)
H /\ 00 /\ (00 /\ (1E \/ [S /\ 00])) = ( A -> 00 /\ A homomorhism )
[H /\ 00] /\ [00 /\ 1E] \/ [S /\ 00])) = ( A -> 00 /\ A homomorhism,
again )
00 /\ (H \/ 1E \/ S) = (axiom 13a see below)
00 /\ (H /\ S)] = (def)
[H + S]

Axiom 13a: 1E /\ 00 = 10

Axiom #31 is the only fundamental property of equality, which
translated in my notation becomes (no special meaning for angled
brackets either!)

13b: S /\ 00 = S and H /\ 00 = H and S \/ H != 00 and S /\ H = H'
imply
((R /\ <S \/ 1E>) \/ H) /\ <S \/ 1E> = (R /\ <S \/ 1E>) \/ H'

> > Do you imply that I can't reduce both sides of the expression R = S to
> > the Union Normal Form in this system?
>
> I don't know, you've onlly given axioms and not the inference
> mechanism. Since they are propositional formulas I assume you want to
> use propositional calculus.

What is the inference mechanism? I thought that we prove equalities by
writing down a chain of equations where each step is supported by some
axiom.

I'm not sure I understand your comment about propositional calculus --
sure your system have implications and therefore derives equalities by
rules of propositional calculus as well.

> If you add this you can no longer claim
> that you have a pure algebraic axiomatization, which makes the
> completeness claim less interesting. But is propositional calculus all
> you allow, or are you also allowing reasoning by rewriting? The latter
> can be captured in either your inference mechanism or by adding adding
> extra axioms (e.g. the rules "if R = R' and S = S' then R /\ S = R' /\
> S'" and "if R = S and S= T then S = T" and ... ). There is the usual
> trade off between putting your inference in the axioms or in the
> inference mechanism.

Again as soon as propositional claculus is used implicitly I don't see
the difference between your and my systems. Perhaps you can reveal
inference rules of your system so that I can see the difference?

> Btw. what I did wonder about is how you would derive "if R1(x,y) /\ 00
> = R1(x,y) and R2(x,y) /\ 00 = R2(x,y) then R1(x,y) /\ [] = R2(x,y) /\
> []".

R1 /\ 00 = X /\ Y /\ 00 (R1 has a set of attributes X and Y)
R2 /\ 00 = X /\ Y /\ 00 (R2 has a set of attributes X and Y as
well)

therefore

R1 /\ 00 = R2 /\ 00

The fact that R1 /\ 00 = R1 is irrelevant, although can be leveraged
to further derive R1 = R2.

> > > 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
>
> Ok. I think that would work. But also here you have to say how the
> inference deals with this. How does it know what and what not to match
> x with when it rewrites? This is solvable, but again it adds
> complexity to the inference mechanism.

Actually, there is no need for explicit single attribute relations
(see below).

OK now you earned your notation. If you also derive (R /\ 00) \/ (R /\
11) = R, I would be totally sold out.

I admit that generalizing your axiom #31 getting rid of the single
attribute condition is quite clever. Leveraging on this idea a little
bit more, can we just define single attribute relation "x" as the one
satisfying the following constraint:

(Msg. 40) Posted: Tue Jun 26, 2007 5:29 pm
Post subject: Re: completeness of the relational lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

On Jun 26, 10:55 am, Vadim Tropashko
wrote:
> 13b: S /\ 00 = S and H /\ 00 = H and S \/ H != 00 and S /\ H = H'
> imply
> ((R /\ <S \/ 1E>) \/ H) /\ <S \/ 1E> = (R /\ <S \/ 1E>) \/ H'

Hmm, the S \/ H != 00 condition doesn't seem to be required. So
rewritten a little the axiom

(Msg. 41) Posted: Tue Jun 26, 2007 6:31 pm
Post subject: Re: completeness of the relational lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

I don't think the axiom #9 (as written in one of your previous posts)
is correct. First, it should be more restrictive than #8 and it looks
less restrictive. Anyway, the first application of distributivity is
correct. I doubt the second one. In the distributive law:

(Msg. 42) Posted: Tue Jun 26, 2007 7:17 pm
Post subject: Re: completeness of the relational lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

On Jun 26, 2:31 pm, Vadim Tropashko
wrote:
> On Jun 26, 1:48 pm, Jan Hidders wrote:
>
> > (R(x,y) * []) + (R(x,y) * W)
> > (22) = [x,y] + (R(x,y) * W)
> > (9) = ([x,y] + R(x,y)) * ([x,y] + W)
> > (10) = R(x,y) * ([x,y] + W)
> > (11) = R(x,y) * (([x] * [y]) + W)
> > (9) = R(x,y) * (([x] + W) * ([y] + W))
> > (32b) = R(x,y) * <x> * <y>
> > (2 = R(x,y)
>
> I don't think the axiom #9 (as written in one of your previous posts)
> is correct. First, it should be more restrictive than #8 and it looks
> less restrictive. Anyway, the first application of distributivity is
> correct. I doubt the second one. In the distributive law:
>
> A + (B*C) = (A+B) * (A+C)
>
> the attributes of B are required to be a superset of A, not subset.

Speaking of axom #9, I only now nocied that you applied earlier when
proving the equality property:

(Msg. 43) Posted: Tue Jun 26, 2007 7:21 pm
Post subject: Re: completeness of the relational lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

On 25 jun, 22:56, Jan Hidders wrote:
>
>
> By the way, I may also some other good news. I looked briefly at the
> problem of the infinitely wide relations, and it seems that is not so
> difficult to solve. The reason is that any expression r that returns
> an infinitely wide result can be rewritten to r' * W where W is my
> version of 11, (W as in "wide" and omega) with r' an expression
> without W. Since for such expressions s' * W and r' * W it holds that
> they are equivalent iff s' and r' are equivalent, this means that we
> can reduce this problem to deciding equivalence for the finitely wide
> expressions. I actually only needed one extra axiom for this:
>
> (32) W + [x] = <x> with x a single attribute

A small correction here. After checking the completeness proof I
noticed it was not completely correct. In fact I had needed the
following axioms:

(32a) W + [] = {()}
(32b) W + [x] = <x> with x a single attribute
(32c) [H] * W = [] * W

(Msg. 44) Posted: Wed Jun 27, 2007 12:48 am
Post subject: Re: completeness of the relational lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

On 26 jun, 19:55, Vadim Tropashko wrote:
>
>
> OK now you earned your notation. If you also derive (R /\ 00) \/ (R /\
> 11) = R, I would be totally sold out.

I hope you'll forgive me if I'm slightly skeptical about that.
Anyway, such a challenge I cannot refuse, of course. To be clear, I
will answer the points you raised, but that requires some more
thinking, because there are some deep and fundamental issues there,
and that requires some more thought.

(Msg. 45) Posted: Wed Jun 27, 2007 1:07 am
Post subject: Re: completeness of the relational lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

On 26 jun, 22:29, Vadim Tropashko wrote:
> On Jun 26, 10:55 am, Vadim Tropashko
> wrote:
>
> > 13b: S /\ 00 = S and H /\ 00 = H and S \/ H != 00 and S /\ H = H'
> > imply
> > ((R /\ <S \/ 1E>) \/ H) /\ <S \/ 1E> = (R /\ <S \/ 1E>) \/ H'
>
> Hmm, the S \/ H != 00 condition doesn't seem to be required. So
> rewritten a little the axiom
>
> S /\ 00 = S and H /\ 00 = H imply
>
> ((R /\ <S \/ 1E>) \/ H) /\ <S \/ 1E> = (R /\ <S \/ 1E>) \/ (H /\ <S \/ 1E>)

which cannot be correct if H and S have no common columns. If you are
projecting all the columns away that are involved in the equalities
and afterwards add them back then that is not the same as not removing
them.

And, yes, having a negative premisse is a very big problem.

Relational Lattice, what is it good for? - Let's begin with an anonymous review of the earlier iteration of the paper ("Dualities among Relational Algebra Operators"): <review> While the paper does have an intriguing premise, it is inappropriate for inclusion in a refereed academ...

Relational lattice completeness - Mikito Harakiri wrote: > Jan Hidders wrote: > > I'm asking the question for a specific model, not in general as you > > did. For example, boolean algebra for boolean value *is* complete. > > According to Matt all that I have to do to...

Complement in Relational Lattice - RL complement is well-defined. It is roughly the complement of the rows and the complement of the columns. 1. !A has all the columns that aren't in A In other words: A \/ !A \/ 10 = 00 Equivalently: A \/ !A >= 00 2a. If A is nonempt...

TRUE and FALSE values in the relational lattice - Given a relation R(x,y) with domains x={0,1,2}, y={'a','b'} we know from classic predicate theory that the expression R(x=0, y='a') evaluates to true or false. Here is how we establish this siumple fact in the relational lattice. First, lets substitut...

Proof of Completeness of Algebraic Properties of Relationa.. - The Relational Lattice algebra ("RL") consists of two generic operations on relations: natural join, written "&&", and inner union, written "||". It has been shown that the RL operations possess the followi...

All times are: Pacific Time (US & Canada) Goto page Previous1, 2, 3, 4, 5

Page 3 of 5

You can post new topics in this forum You can reply to topics in this forum You can edit your posts in this forum You can delete your posts in this forum You can vote in polls in this forum

Warning: fopen(/home/adsense_reject.txt) [function.fopen]: failed to open stream: Permission denied in /home/autoforu/public_html/Giga/GigaFunctions.php on line 1142

Warning: fwrite(): supplied argument is not a valid stream resource in /home/autoforu/public_html/Giga/GigaFunctions.php on line 1143

Warning: fclose(): supplied argument is not a valid stream resource in /home/autoforu/public_html/Giga/GigaFunctions.php on line 1144