Re: constraints in algebra instead of calculus

On Jun 15, 10:24 am, Vadim Tropashko <vadimtro_inva..._at_yahoo.com> wrote:
> On Jun 15, 9:23 am, Vadim Tropashko <vadimtro_inva..._at_yahoo.com>
> wrote:
>
> > Remarkably, it is shaped very similarly to FK constraint
>
> > A \/ X B \/ X

Apparently, the inequality symbol "less (or equal) than" didn't render making the whole post unreadable so I'll use the '<' instead:

A \/ X < B \/ X

>
> > that was mentioned earlier in the thread.
>
> > This is fine, but what are the implications? Can it be demonstrated
> > that Armstrong axioms easily follow from this formulation?
>
> BTW, transitivity of FK is easy. Consider 3 relations
>
> A(x,u), B(x,y,v), C(x,y,w)
>
> where x,y,u,v,w individual attributes or sets of attributes. Again,
> let X(x) be the empty relation with attribute x, and Y(x,y) be the the
> empty relation with attributes x and y. Then,
>
> table B foreign key (x) references A(x)
>
> (what a syntax!) is formally an inequality
>
> B \/ X A \/ X

B \/ X < A \/ X

> (As a reminder, the partial order " " that is "less (or equal) than"

the partial order "<" that is "less (or equal) than"

> in the relational lattice has the two special cases:
> 1. when both relations have the same set of attributes and the first
> relation has a superset of rows of the second one, and
> 2 The empty relation has sbset of attributes of the other empty
> relation
> The partial order, therefore, generalizes the set theory subset
> relation).
>
> Likewise,
>
> C \/ Y B \/ Y

C \/ Y < B \/ Y

> or in conventional language
>
> table C foreign key (x,y) references B(x,y)
>
> Note that also X Y as the set of attributes of the empty relation X

X < Y

> is a subset of that of Y.
>
> It follows that
>
> C \/ X B \/ X

C \/ X < B \/ X

> The proof is somewhat tedious (and I wonder if a quicker method or
> just a reference to LT would suffice):
>
> By inequality definition we have:
> B \/ Y \/ C \/ Y = C \/ Y
> X \/ Y = X
> Prove:
> B \/ X \/ C \/ X = C \/ X
>
> Proof:
> B \/ X \/ C \/ X = B \/ X \/ C = B \/ X \/ Y \/ C =
> = B \/ X \/ Y \/ C = X \/ B \/ Y \/ C = X \/ C \/ Y =
> = X \/ C
>
> Now that we proved C \/ X B \/ X we derive by transitivity

C \/ X < B \/ X

>
> C \/ X A \/ X

C \/ X < A \/ X

>
> That was quite a long way to establish the obvious:
>
> table C foreign key (x) references A(x)
>
> !
Received on Fri Jun 15 2007 - 19:29:40 CEST