## The Forum for Discussion about The Third Manifesto and Related Matters

Forum breadcrumbs - You are here:
Please or Register to create posts and topics.

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

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?".