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 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 NatJoining 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 N5 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 T0};
• there's only on possible relation value RE0 = REL{E T0} {}.
• 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 T1} {D TheValue}; RD0 = REL{D T1} {}.
• 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?".