Re: armstrong's axioms: augmentation - help pls

"loveboat" <l0veb0at_at_gmx.de> wrote in message news:con0pi$c5c$1_at_svr7.m-online.net... > in armstrongs axioms, i don't get the augmentation, which is: > (X -> Y) => (XZ -> YZ)

Here is a proof of augmentation rule in XDB2.

...

Just kidding, I meant algebraic proof, of course. (Or as I use SQL syntax, should it be called "calculus-algebraic"?)

Given

A.x->A.y

By "->" definition

for any tuples a1,a2 from A
( a1.x=a2.x implies a1.y=a2.y )

which can be equivalently rewritten as

not exists a1,a2 ( a1.x=a2.x & a1.y!=a2.y )

which immediately gives view equation

(

select from A a1, A a2
where a1.x = a2.x and a1.y != a2.y
) = {}

We didn't started the proof yet: all we did is translating armstrong implication into a view equation written with SQL syntax. Please ignore this part when evaluating how verbose the proof is.

If we augment "where" clause of the empty view, we'd still have an empty view

(

select from A a1, A a2
where a1.x = a2.x and a1.y != a2.y
and a1.z = a2.z
) = {}

Next, consider view equation

(

select from A a1, A a2
where a1.x = a2.x and a1.z != a2.z
and a1.z = a2.z
) = {}

which is tautologically true because there are contradictory predicates. Union both views together

(

select from A a1, A a2
where a1.x=a2.x and a1.z=a2.z
and a1.y!=a2.y
 union
select from A a1, A a2
where a1.x=a2.x and a1.z=a2.z
and a1.z!=a2.z
) = {}

Combine the union operands

(select from A a1, A a2

where a1.x=a2.x and a1.z=a2.z
and (a1.y!=a2.y or a1.z!=a2.z)
) = {}

The formal proof stops there. Let's check if the last view equation is indeed the armstrong implication we are after. Transforming view equation into calculus expression

not exists a1,a2
( a1.x=a2.x & a1.z=a2.z & (a1.y!=a2.y \/ a1.z!=a2.z))

or, equivalently

for any tuples a1,a2
( a1.x=a2.x & a1.z=a2.z implies a1.y=a2.y & a1.y=a2.y )

which is indeed

A.xz->A.yz Received on Thu Dec 02 2004 - 19:55:26 CET