Re: TRUE and FALSE values in the relational lattice

On Jun 19, 10:51 am, Vadim Tropashko <vadimtro_inva..._at_yahoo.com> 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 Received on Tue Jun 19 2007 - 22:32:14 CEST