(Msg. 1) Posted: Sat May 20, 2006 8:56 pm
Post subject: Proof of Completeness of Algebraic Properties of Relational Lattice Archived from groups: comp>databases>theory (more info?)

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 following
properties:

commutative: A && B = B && A
A || B = B || A

associative: A && (B && C) = (A && B) && C
A || (B || C) = (A || B) || C

idempotent: A && A = A
A || A = A

absorbtive: (A && B) || B = B
(A || B) && B = B

Furthermore, the algebra is quasi-distributive:

A && (B || C) = (A && B) || (A && C) ||
empty(a,abc,b,bc,c)

(The empty term contains all attributes that are not common to both A
and B,
nor common to both A and C.)

Given commutativity, associativity, and the above quasi-distributivity,
we can
rewrite any RL expression into a disjunctive normal form, which
consists of a
collection of minterms connected by ||. Some of the minterms might be
"empty"
terms, created by the application of quasi-distributivity. If there are
more than
one "empty" minterm, they can be coalesced into a single one,
containing only
those attributes that are common to all of the empty minterms. If the
result
contains any attributes that are not part of the result of the
expression,
those attributes can be dropped from the empty minterm as well.

If no applications of distributivity are required, there will be no
empty term,
but we can manufacture one, again by inspecting the attributes of the
result
and creating an empty minterm that corresponds. Thus all DNF
expressions have
exactly one empty term, and if two expressions have the same type, they
will
have the same empty term.

The minterms other than the empty term can be viewed as a set of sets
of relation
variables. For example, (v1 || (v2 && v3)) || ((v2 && v4) && v5) ||
empty(...)
can be thought of as { {v1}, {v2, v3}, {v2, v4, v5} } || empty(...).
Let us call
this the set representation.

Applications of the idemponent and absorbtive property can convert any
set
representation into a set representation that is subset-free. That is,
for
{ C1, C2, ... Cn }, there does not exist Ci, Cj such that Ci is a
subset of Cj.
Let us call this subset-free disjunctive normal form, or SF-DNF.

Consider two expressions e1 and e2, each written in terms of a set of
relation
variables v1 .. vn. If, for all possible values of v1 .. vn, e1 = e2,
we say
e1 and e2 are semantically equivalent.

Now to address the main question. We wish to prove that if two
expressions
e1 and e2 can be rewritten to SF-DNF form s1 and s2, and e1 and e2 are
semantically equivalent, then s1 = s2.

Proof is by contradiction.

Given two semantically equivalent expressions e1 and e2 with SF-DNF
form s1 and s2 respectively. ASSUME s1 != s2.

Let s1 = {B1, ..., Bn} || empty and s2 = {C1, ..., C2} || empty

Because e1 and e2 are semantically equivalent, they have the same set
of attributes, so the two empty terms will be identical.

s1 and s2 are different, finite, and subset-free. Therefore,
either there exists some Bi that is not a superset of any of C1, ...,
Cn,
or there exists some Cj that is not a superset of any of B1, ... , Bn.
(If there were no such term, it would mean s1 and s2 were identical.)

We can assume without loss of generality that Bi is the not-superset
term. (The proof is the same if we assume it is Cj.)

For each attribute of each variable in Bi, choose an arbitrary value
from the type of that attribute. (The specific value is irrelevant.
Note that this introduces the requirement into the proof that all types
of all attributes contain at least one value.) For each variable in Bi,
assign a value to the variable that consists of a single element, where
each attribute has the chosen value from that type. For each variable
not
in Bi, assign a value that is empty (that is, has no element.) Because
each variable in the Bi minterm contains one element, and the
attributes
in common with each variable are equal (because we chose the same value
for each attribute), the result of the && operations on all the
variables
in the Bi minterm will have a single element. Because all the other
variables in all the minterms in s1 are empty, the minterms will be
empty as well. The result of the || of each minterm will have exactly
one row, from the Bi minterm. So s1 will have exactly one element.

In s2, every minterm will evaluate to an empty result, because we
assigned to each variable an empty value, except for those in Bi,
and no C1 .. Cn is a subset of Bi. Therefore, s2 will have exactly
zero element.

This contradicts our assumption that s1 != s2. Therefore by RAA,
if e1 and e2 are semantically equivalent, the SF-DNF form of e1
and e2 are equal. Since we can apply the equalities to rewrite
e1 to s1, (and vice versa) and e2 to s2, and since s1 = s2, we
can rewrite any two semantically equivalent e1 and e2 into
each other.

(Msg. 2) Posted: Sat May 20, 2006 9:05 pm
Post subject: Re: Proof of Completeness of Algebraic Properties of Relational Lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

Marshall wrote:
> The Relational Lattice algebra ("RL") consists of two
> generic operations on relations: natural join, written
> "&&", and inner union, written "||".

Thanks as always to Vadim Tropashko, for his work on the
relational lattice, and particularly to Jan Hidders, whose
demonstration of a comparable proof for the booleans made
this possible. Curses to the Google Groups team for
reformatting my text. Darn them to heck!

Any errors or omissions are my own.

As always, any comments, complaints, criticisms, corrections,
or other things starting with 'c' welcome.

(Msg. 3) Posted: Sun May 21, 2006 2:57 pm
Post subject: Re: Proof of Completeness of Algebraic Properties of Relational Lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

(Msg. 4) Posted: Sun May 21, 2006 3:03 pm
Post subject: Re: Proof of Completeness of Algebraic Properties of Relational Lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

(Msg. 5) Posted: Sun May 21, 2006 4:21 pm
Post subject: Re: Proof of Completeness of Algebraic Properties of Relational Lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

Neo wrote:
> Or more accurately/practically, how does one verify that a proof is
> correct?

Absolute knowledge of truth is not part of the human condition.
However, we have many things we can do to increase our
confidence of a particular idea. A proof is a good first step.
The more formal the proof, the better our confidence.
(My proof here is not particularly formal.) Also good is
publishing a proof so that it's in front of many eyes; the
more people that see it, the more chances there are that
flaws will be spotted. A single flaw is enough to invalidate
a proof.

Other good things to do: publication in a peer-reviewed journal.
Also, use of a proof assistant, such as Coq, is an excellent,
formal way of reinforcing proofs. But then we can ask,
how do we verify the proof assistant is sound? This leads
to infinite regress, which is part of why absolute knowledge
of truth is impossible.

In practical terms, if, say, VC, Jan Hidders, and Vadim Tropashko
don't find anything wrong with it, it's probably right.

(Msg. 6) Posted: Sun May 21, 2006 4:41 pm
Post subject: Re: Proof of Completeness of Algebraic Properties of Relational Lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

Marshall wrote:
>The algebra is quasi-distributive:
>A && (B || C) = (A && B) || (A && C) || empty(a,abc,b,bc,c)

This is an interesting attempt to formulate distributivity criteria. I
interpret your identity as a formal algebraic equality in the lattice
algebra

A /\ (B \/ C) = (A /\ B) \/ (A /\ C) \/ D

where the additional term D vanishes whenever Spight distributivity
criteria is met. The analogy is with Lie algebras, which are not
commutative ab != ba so that a special construction -- the commutator
[a,b]=ab-bc -- is introduced. In this case the additional disjunct D
can be called a "distributor term".

First of all, how can we be sure that there always exists a
"distributor term"? The equation that defines distributor term D can
have no solutions! Existence of distributor hinges on the following
inequality:

A /\ (B \/ C) >= (A /\ B) \/ (A /\ C)

proof:

A /\ (B \/ C) /\ ((A /\ B) \/ (A /\ C)) = #
distributivity by Spight criteria

A /\ ((A /\ B /\ (B \/ C)) \/ (A /\ C /\ (B \/C ))) = # absorption

A /\ ((A /\ B) \/ (A /\ C)) = #
distributivity by Spight criteria

((A /\ B /\ A) \/ (A /\ C /\ A)) = # idempotence

(A /\ B) \/ (A /\ C)

So far so good. There are two problems, however.

Distributor term defined equationally as above is not unique, however.
There has to be an extra condition.

Second, the distributor term can't be expressed as a closed form
expression of the relations A, B, and C. You can witness this in a
simple lattice generated by all the unions and joins of the following
relations

Q = {x=1}
R = {x=1}\/{x=2}
S = {y=a}
T = {y=a}\/{y=b}

Take

A = R /\ T
B = Q
C = S

then

A /\ (B \/ C) = {(x=1,y=a),(x=1,y=b),(x=2,y=a),(x=2,y=b)}

(A /\ B) \/ (A /\ C) = {(x=1,y=a),(x=1,y=b),(x=2,y=a)}

(Msg. 7) Posted: Sun May 21, 2006 8:57 pm
Post subject: Re: Proof of Completeness of Algebraic Properties of Relational Lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

> > Or more accurately/practically, how does one verify that a proof is correct?
>
> Absolute knowledge of truth is not part of the human condition.

So, are you saying we have no reference to judge by, whether a proof is
correct?

> However, we have many things we can do to increase our confidence of a particular idea. A proof is a good first step. The more formal the proof, the better our confidence. (My proof here is not particularly formal.) Also good is publishing a proof so that it's in front of many eyes; the more people that see it, the more chances there are that flaws will be spotted. A single flaw is enough to invalidate a proof.

But what good is the definition of define, if it uses define to define
it? Proofs that God exist are flaw-less (according to those providing
the proof). The bible is published for many eyes and many can't find a
flaw in it.

> Other good things to do: publication in a peer-reviewed journal. Also, use of a proof assistant, such as Coq, is an excellent, formal way of reinforcing proofs. But then we can ask, how do we verify the proof assistant is sound? This leads to infinite regress, which is part of why absolute knowledge of truth is impossible.

(Msg. 8) Posted: Sun May 21, 2006 9:38 pm
Post subject: Re: Proof of Completeness of Algebraic Properties of Relational Lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

Tonight, the part of Philip J. Fry will be played by Neo, and the part
of Professor Farnsworth will be played by Marshall.

Neo wrote:
> > > Or more accurately/practically, how does one verify that a proof is correct?
> >
> > Absolute knowledge of truth is not part of the human condition.
>
> So, are you saying we have no reference to judge by, whether a proof is
> correct?

No, I am not saying anything remotely like that. In fact, the very next
sentence made that abundantly clear.

> > However, we have many things we can do to increase our confidence of a particular idea. A proof is a good first step. The more formal the proof, the better our confidence. (My proof here is not particularly formal.) Also good is publishing a proof so that it's in front of many eyes; the more people that see it, the more chances there are that flaws will be spotted. A single flaw is enough to invalidate a proof.
>
> But what good is the definition of define, if it uses define to define
> it? Proofs that God exist are flaw-less (according to those providing
> the proof). The bible is published for many eyes and many can't find a
> flaw in it.

Farnsworth: "We're not watching it again, ask something less stupid!"

> > Other good things to do: publication in a peer-reviewed journal. Also, use of a proof assistant, such as Coq, is an excellent, formal way of reinforcing proofs. But then we can ask, how do we verify the proof assistant is sound? This leads to infinite regress, which is part of why absolute knowledge of truth is impossible.
>
> Are they really proofs or just self-consistent, self-supporting,
> self-confirming systems?

Farnsworth: "That question is less stupid, though you asked it in a
profoundly stupid way."

"Self-consistent" is a necessity. "Self-supporting" doesn't mean
anything.
"Self-confirming" is an impossibility, so the answer is no.

(Msg. 9) Posted: Sun May 21, 2006 11:16 pm
Post subject: Re: Proof of Completeness of Algebraic Properties of Relational Lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

Vadim Tropashko wrote:
> Marshall wrote:
> >The algebra is quasi-distributive:
> >A && (B || C) = (A && B) || (A && C) || empty(a,abc,b,bc,c)
>
> This is an interesting attempt to formulate distributivity criteria.

After looking at your objections, and with further analysis on
my end, it appears that my restatement of the distributivity
criteria is bogus. Since that's approximately step one of the
proof, I think we can safely ignore the rest unless this
breach can be repaired.

I'll try to come up with a restatement of the distributivity that
isn't bogus. The goal is to be able to use the quasi-distributivity
to generate a normal form for expressions.

(Msg. 10) Posted: Mon May 22, 2006 4:54 am
Post subject: Re: Proof of Completeness of Algebraic Properties of Relational Lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

Marshall wrote:

> Tonight, the part of Philip J. Fry will be played by Neo, and the part
> of Professor Farnsworth will be played by Marshall.
>
> Neo wrote:
>
>>>>Or more accurately/practically, how does one verify that a proof is correct?
>>>
>>>Absolute knowledge of truth is not part of the human condition.
>>
>>So, are you saying we have no reference to judge by, whether a proof is
>>correct?
>
> No, I am not saying anything remotely like that. In fact, the very next
> sentence made that abundantly clear.
>
>>>However, we have many things we can do to increase our confidence of a particular idea. A proof is a good first step. The more formal the proof, the better our confidence. (My proof here is not particularly formal.) Also good is publishing a proof so that it's in front of many eyes; the more people that see it, the more chances there are that flaws will be spotted. A single flaw is enough to invalidate a proof.
>>
>>But what good is the definition of define, if it uses define to define
>>it? Proofs that God exist are flaw-less (according to those providing
>>the proof). The bible is published for many eyes and many can't find a
>>flaw in it.
>
> Farnsworth: "We're not watching it again, ask something less stupid!"
>
>>>Other good things to do: publication in a peer-reviewed journal. Also, use of a proof assistant, such as Coq, is an excellent, formal way of reinforcing proofs. But then we can ask, how do we verify the proof assistant is sound? This leads to infinite regress, which is part of why absolute knowledge of truth is impossible.
>>
>>Are they really proofs or just self-consistent, self-supporting,
>>self-confirming systems?
>
> Farnsworth: "That question is less stupid, though you asked it in a
> profoundly stupid way."
>
> "Self-consistent" is a necessity. "Self-supporting" doesn't mean
> anything.
> "Self-confirming" is an impossibility, so the answer is no.
>
> And yes, they are really proofs.
>
> Marshall
>
> PS. Futurama quotes are from the episode "Anthology of Interest."

(Msg. 11) Posted: Mon May 22, 2006 6:06 pm
Post subject: Re: Proof of Completeness of Algebraic Properties of Relational Lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

> ... A single flaw is enough to invalidate a proof.

(Msg. 12) Posted: Wed May 24, 2006 2:00 pm
Post subject: Re: Proof of Completeness of Algebraic Properties of Relational Lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

Vadim Tropashko wrote:
> Existence of distributor hinges on the following
> inequality:
>
>
> A /\ (B \/ C) >= (A /\ B) \/ (A /\ C)

This identity is true in any lattice, not only relational one. Hence it
can be proved witut need to invoke distributivity criteria.

1. A /\ (B \/ C) >= (A /\ B)

Proof: A /\ (B \/ C) /\ (A /\ B) = A /\ B /\ (B \/ C) = A /\ B

(Msg. 13) Posted: Tue May 30, 2006 12:33 am
Post subject: Re: Proof of Completeness of Algebraic Properties of Relational Lattice [Login to view extended thread Info.] Archived from groups: per prev. post (more info?)

Mikito Harakiri wrote:
> Vadim Tropashko wrote:
> >
> > A /\ (B \/ C) >= (A /\ B) \/ (A /\ C)
>
> This identity is true in any lattice, not only relational one. Hence it
> can be proved witut need to invoke distributivity criteria.

Upon further investigation, it appears impossible to create
a form of the distributive equation such that the distributor
appears on the right/undistributed side. If that is in fact
the case, then it appears further impossible to transform
any equation into either conjunctive or disjunctive normal
form. Which pretty much cuts off the entire line of reasoning
I was using.

Jan has stated that semantic equivalence is undecidable
in the RA. I strongly suspect that there is a simple
procedure to transform the classical RA into the RL, in
which case we would expect that this would also be
undecidable for the RL.

(All the above is merely informed conjecture.)

At this point I see no further reason to pursue this line
of inquiry.

A new proof of the superiority of set oriented approaches:.. - Among the least explored opportunities RM has to offer comes the issue of numerical / time series linear interpolation of values. Recently, I have solved the following problem on a community board which I encountered this problem a few years ago with..

Verify Basic Algebra Properties - Apparently the following four algebraic properties (or something similar) are considered important, possibly showing an approach is well-grounded in mathematics. Commutative: A and B = B and A A or B = B or A Associative: A and...

Modelling objects with variable number of properties in an.. - i've apparently hit a brick wall in my understanding of table relationships. Say I have the following: widgets: id widget ---------------------- 1 sprocket 2 cog 3 hammer 4 thingamajig qualifiers: id qualifier..

Valentina 3.5 Now Offers Custom Server Properties - Valentina Office Server, Valentina Embedded Server and the free Valentina Community Server for Linux now support custom database properties, some of which include both read and write properties. This treats databases on servers as objects, much as modern...

Non Sequitur - <satire> Meteorologists have noted that there is an unusually high number of hurricanes in the Caribbean this year. Experts are in disagreement as to what the fundamental cause is. However, one frequent observer has conjectured that, "this...

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