# The macro-level lattice structure of relations in the vicinity of `DEE`, `DUM`

Quote from AntC on May 22, 2021, 11:11 am

Quote from AntC on May 21, 2021, 11:37 pm [was: ANNOUNCE a relational algebra ...]... can't be

`DUM`

because it's not immediately adjacent to`DEE`

.Ok, trying an entirely different tack.

I'll presume for the time being all attribute types have cardinality at least 2. That is,

`Bool`

is amongst the smallest possible types. (I'll come back at the end to consider the consequences of a single-valued or zillary attribute type.)## Single-attribute relations

Say we have two relation values, one with single attribute

`A`

, one with single attribute`B`

, both type`Bool`

. Consider the fullest possible relation values with those headings, and the emptiest possible:

`RA1`

=df`REL{A Bool} {TUP{A True}, TUP{A False}}`

. (two tuples)`RB1`

=df likewise, for attribute`B`

.`RA0`

=df`REL{A Bool} {}`

. (no tuples)`RB0`

=df likewise, for attribute`B`

.Where do those sit in the lattice?

`RA1, RB1`

are immediately adjacent below`DEE`

.`RA0, RB0`

are immediately adjacent below`DUM`

. By 'immediately adjacent below' I mean lesser in the lattice ordering, but with no other relation value in between.

`RA0, RB0`

are below`RA1, RB1`

butnotimmediately adjacent: in between are the relations with a single tuple for that heading. Is there anything else immediately adjacent below`RA1, RB1`

? Yes:`RA1 NatJoin RB1`

-- that is, the Cartesian product, with heading`{A Bool, B Bool}`

and all possible tuples (4 of) for that heading. (And likewise all the pairings of single-attribute headings -- that is all the degree-two relations, maximum possible tuples.)## Finding

`DUM`

But hold!

`DUM`

is immediately adjacent below`DEE`

, and`RA0 = DUM NatJoin RA1, RB0 = DUM NatJoin RB1`

are immediately adjacent below`DUM`

. So to find`DUM`

in the lattice:

`DUM`

is immediately adjacent below`DEE`

;- and for all other relations immediately adjacent below
`DEE`

(say`RA1, RB1`

), pairwise`NatJoin`

ing them yields a relation immediately adjacent below each;- whereas
`DUM NatJoin RA1`

yields a relation immediately adjacent below`DUM`

;- but not immediately adjacent below
`RA1`

.- (This is not news. It's an example of the smallest non-distributive lattice
`N`

_{5}Pic 11, which appear all over relational lattice structures. What's new is me realising it appears in a very specific location in the vicinity of`DEE, DUM`

. In that Pic:`1`

corresponds to`DEE`

;`a`

corresponds to`DUM`

;`c`

corresponds to`RA1`

;`b`

corresponds to`RA½`

-- heading`A`

, body a single tuple;`0`

corresponds to`RA0 = DUM NatJoin RA1`

. In our example, there should be another relation`d`

corresponding to a different`RA?`

-- heading`A`

, body the single other possible tuple with that heading -- with route`c — RA? — 0`

bypassing the route through`b`

.)## Code/equations

The bonus here is I've described this location using only

`NatJoin`

(which gives the lattice ordering). To talk about it, some predicates/operators would be handy:

`r1 >= r2 ≡ r1 NatJoin r2 = r2.`

greater-or-equal in the lattice ordering.`between(r1, s, r2) ≡ r1 >= s & s >= r2.`

`apart(r1, r2) ≡ ∃ s. (r1 >= s & r1 ≠ s & s >= r2 & s ≠ r2).`

below, but not immediately adjacent`adj(r1, r2) ≡ (r1 >= r2 & r1 ≠ r2 & (∀ s (between(r1, s, r2) ≡ r1 = s | s = r2))).`

immediately adjacent below`DUM`

given by:`adj(DEE, DUM)`

`& ( ∀ r1. (adj(DEE, r1) & r1 ≠ DUM) → ( adj(DUM, DUM NatJoin r1) & apart(r1, DUM NatJoin r1) ) ).`

- Prover9 tells me this fixes
`DUM`

uniquely.- Also confirms this holds:
`r1 NatJoin DUM ≠ r1 ≡ r1 InnerUnion DUM = DEE`

. Two equivalent ways to tell if a relation is empty.- Sadly, that axiom/predicates are in 'non-positive' form: There's not-equals, existential quant, nested universal quant, nested disjunction. We can shuffle the equations around, but we'd still get a non-positive somewhere.
Now I can define those problematic operators (

`NotMatching, project, Remove`

) using`DUM`

, especially`... NatJoin DUM`

for`emptify( )`

. And some of the equations I expect to hold get proven; and none of them can Mace4 provide a counter-example.Butmost of them can't be proven -- even after several hours of running -- and that's because of the non-positive forms.## Degenerate attribute types

Coming back to the presumption about attribute types.

- Types with no possible values (
TTM`Omega`

?) are (surprisingly) not a difficulty.- Consider a Relation with attribute name
`E`

of that type, heading`{E T`

_{0}`}`

;- there's only on possible relation value
`RE0 = REL{E T`

_{0}`} {}`

.`RE0`

is immediately adjacent below`DUM`

, but not adjacent to`DEE`

-- precisely because`DUM`

intervenes.- So
`RE0`

won't be considered for its location in the vicinity of`DEE`

.- OTOH attribute types with exactly one possibly value are dodgy.
- Consider Relations with attribute name
`D`

of that unitype.- There's two possible relation values
`RD1 = REL{D T`

_{1}`} {D TheValue}; RD0 = REL{D T`

_{1}`} {}.`

`RD1`

is immediately adjacent below`DEE`

;`RD0 = DUM NatJoin RD1`

is immediately adjacent belowboth`DUM`

and`RD1`

.- So by the definition above, the appearance of
`RD1, RD0`

in the lattice would make it impossible to uniquely identify`DUM`

.- The definition requires
`Rx1`

to be apart from`Rx0 = DUM NatJoin Rx1`

for all attributes`x`

. This in effect rules out attribute types of cardinality 1. In the words of that acute observer of schoolroom algebra Lauren Cooper, "Am I bovvered?".

Quote from AntC on May 21, 2021, 11:37 pm [was: ANNOUNCE a relational algebra ...]... can't be

`DUM`

because it's not immediately adjacent to`DEE`

.

Ok, trying an entirely different tack.

I'll presume for the time being all attribute types have cardinality at least 2. That is, `Bool`

is amongst the smallest possible types. (I'll come back at the end to consider the consequences of a single-valued or zillary attribute type.)

#### Single-attribute relations

Say we have two relation values, one with single attribute `A`

, one with single attribute `B`

, both type `Bool`

. Consider the fullest possible relation values with those headings, and the emptiest possible:

`RA1`

=df`REL{A Bool} {TUP{A True}, TUP{A False}}`

. (two tuples)`RB1`

=df likewise, for attribute`B`

.`RA0`

=df`REL{A Bool} {}`

. (no tuples)`RB0`

=df likewise, for attribute`B`

.

Where do those sit in the lattice? `RA1, RB1`

are immediately adjacent below `DEE`

. `RA0, RB0`

are immediately adjacent below `DUM`

. By 'immediately adjacent below' I mean lesser in the lattice ordering, but with no other relation value in between.

`RA0, RB0`

are below `RA1, RB1`

but *not* immediately adjacent: in between are the relations with a single tuple for that heading. Is there anything else immediately adjacent below `RA1, RB1`

? Yes: `RA1 NatJoin RB1`

-- that is, the Cartesian product, with heading `{A Bool, B Bool}`

and all possible tuples (4 of) for that heading. (And likewise all the pairings of single-attribute headings -- that is all the degree-two relations, maximum possible tuples.)

#### Finding `DUM`

But hold! `DUM`

is immediately adjacent below `DEE`

, and `RA0 = DUM NatJoin RA1, RB0 = DUM NatJoin RB1`

are immediately adjacent below `DUM`

. So to find `DUM`

in the lattice:

`DUM`

is immediately adjacent below`DEE`

;- and for all other relations immediately adjacent below
`DEE`

(say`RA1, RB1`

), pairwise`NatJoin`

ing them yields a relation immediately adjacent below each; - whereas
`DUM NatJoin RA1`

yields a relation immediately adjacent below`DUM`

; - but not immediately adjacent below
`RA1`

. - (This is not news. It's an example of the smallest non-distributive lattice
`N`

_{5}Pic 11, which appear all over relational lattice structures. What's new is me realising it appears in a very specific location in the vicinity of`DEE, DUM`

. In that Pic:`1`

corresponds to`DEE`

;`a`

corresponds to`DUM`

;`c`

corresponds to`RA1`

;`b`

corresponds to`RA½`

-- heading`A`

, body a single tuple;`0`

corresponds to`RA0 = DUM NatJoin RA1`

. In our example, there should be another relation`d`

corresponding to a different`RA?`

-- heading`A`

, body the single other possible tuple with that heading -- with route`c — RA? — 0`

bypassing the route through`b`

.)

#### Code/equations

The bonus here is I've described this location using only `NatJoin`

(which gives the lattice ordering). To talk about it, some predicates/operators would be handy:

`r1 >= r2 ≡ r1 NatJoin r2 = r2.`

greater-or-equal in the lattice ordering.`between(r1, s, r2) ≡ r1 >= s & s >= r2.`

`apart(r1, r2) ≡ ∃ s. (r1 >= s & r1 ≠ s & s >= r2 & s ≠ r2).`

below, but not immediately adjacent`adj(r1, r2) ≡ (r1 >= r2 & r1 ≠ r2 & (∀ s (between(r1, s, r2) ≡ r1 = s | s = r2))).`

immediately adjacent below`DUM`

given by:`adj(DEE, DUM)`

`& ( ∀ r1. (adj(DEE, r1) & r1 ≠ DUM) → ( adj(DUM, DUM NatJoin r1) & apart(r1, DUM NatJoin r1) ) ).`

- Prover9 tells me this fixes
`DUM`

uniquely. - Also confirms this holds:
`r1 NatJoin DUM ≠ r1 ≡ r1 InnerUnion DUM = DEE`

. Two equivalent ways to tell if a relation is empty. - Sadly, that axiom/predicates are in 'non-positive' form: There's not-equals, existential quant, nested universal quant, nested disjunction. We can shuffle the equations around, but we'd still get a non-positive somewhere.

Now I can define those problematic operators (`NotMatching, project, Remove`

) using `DUM`

, especially `... NatJoin DUM`

for `emptify( )`

. And some of the equations I expect to hold get proven; and none of them can Mace4 provide a counter-example. **But** most of them can't be proven -- even after several hours of running -- and that's because of the non-positive forms.

#### Degenerate attribute types

Coming back to the presumption about attribute types.

- Types with no possible values (
*TTM*`Omega`

?) are (surprisingly) not a difficulty. - Consider a Relation with attribute name
`E`

of that type, heading`{E T`

_{0}`}`

; - there's only on possible relation value
`RE0 = REL{E T`

_{0}`} {}`

. `RE0`

is immediately adjacent below`DUM`

, but not adjacent to`DEE`

-- precisely because`DUM`

intervenes.- So
`RE0`

won't be considered for its location in the vicinity of`DEE`

. - OTOH attribute types with exactly one possibly value are dodgy.
- Consider Relations with attribute name
`D`

of that unitype. - There's two possible relation values
`RD1 = REL{D T`

_{1}`} {D TheValue}; RD0 = REL{D T`

_{1}`} {}.`

`RD1`

is immediately adjacent below`DEE`

;`RD0 = DUM NatJoin RD1`

is immediately adjacent below*both*`DUM`

and`RD1`

.- So by the definition above, the appearance of
`RD1, RD0`

in the lattice would make it impossible to uniquely identify`DUM`

. - The definition requires
`Rx1`

to be apart from`Rx0 = DUM NatJoin Rx1`

for all attributes`x`

. This in effect rules out attribute types of cardinality 1. In the words of that acute observer of schoolroom algebra Lauren Cooper, "Am I bovvered?".