Re: TRUE and FALSE values in the relational lattice

On Jun 19, 10:51 am, Vadim Tropashko <vadimtro_inva...@xxxxxxxxx>
wrote:
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 substitute x -> x=0 into R(x,y) and get unary relation
R'(y). The formula for such substitution is

R'(y) = R(0,y) = (R /\ `x=0`) \/ `y`

where `x=0' is unary relation with one tuple {0} and attribute x, and
`y` is the unary empty relation with attribute y. Informally, we
select all the tuples in R such that x=0 and project the result to
column y.

Next, we substitute y -> y=a into R'(y) and obtain "emptiary"
relation R":

R"({}) = R(0,'a') = ( ( (R /\ `x=0`) \/ `y` ) /\ `y=a` ) \/ 00

It is instructive to apply the distributivity criteria (I lost count
how many times I leveraged it!) and simplify the expression to

R(0,'a') = ( R /\ `x=0` /\ `y=a` ) \/ 00

As expected this expression is valued to 00 or 01, so Marshall was
eventually right when interpreting those relations as TRUE and FALSE.

Not to be contrary, but I've revised my thinking in that area.
I now equate 10 as false rather than 00. Any other relation
equates to true, especially, of course, 01.

The relevance that 00 plays is in relation to existential
quantification.
I interpret existential quantification as meaning a relation is not
empty.

We can define exists(X) as:

X | 00 = 01

Where = is a primitive that returns either 10 or 01 according
the usual meaning.

As far as lattice order goes, it is usually written , meaning

A B iff (A & B = A)

(In case that character doesn't display correctly, it's the usual
single character version of <=.)

However this relations closely corresponds to logical implication,
which is often written =>. It almost looks like a comparison
operator, coincidentally. Since there is some value in writing
the relational operators differently than the scalar ones, it
might make sense to use => as the way to write this relation.
Thus:

10 => A
A => 01

etc.

I know Vadim is not thrilled with my notation, however
we are thinking of different audiences. He is more concerned
with maintaining fidelity with mathematical notation, and I'm
interested in a notation that will be palatable to programmers.
So we naturally reach different results.

I am thinking about formalizing the lattice logic. That would
involve a formal statement of the axioms and the rules of
inference. We would then want a soundness proof, and
a proof of consistency. We would also want to understand
how complete such a logic would be, and how strong it
was relative to FOL. And how decidable. My hope is
that it is decidable even if that means it is weaker than
FOL. We also have to think about what else besides
& and | we're putting in to it. Clearly 00 is a strong
candidate. I'm currently thinking that the negation
operator I defined a week or two ago is *not* a good idea.
The scary one is division/group by.

All this requires a better understanding of logic and proof
theory than I currently possess. So I have some trepidation,
along with a lot of required reading.

It turns out a lot of this work has already been done for
complete lattices, and this work will just be an extension
of that.

It is interesting to consider the question of whether to take
equality or the order relation as primitive. Each can be
defined in terms of the other. However I am finding it
easier to write inference rules against the order than
against equality.


Marshall

.

Relevant Pages

  • complement in relational bi-lattice
    ... Classic Relational Algebra employs six basic operations: ... natural join and inner union. ... Algebra, didn't fit into any lattice ... We keep a very succinct algebraic notation, ...
    (comp.databases.theory)
  • Re: Lattices--the distributive inequality
    ... the same in simpler Boolean algebra like notation ... Also the lattice of topologies for a set with more than three points isn't ... requirement that lub x,y and glb x,y exist for all x,y. ...
    (sci.math)
Loading