# ANNOUNCE: a relational algebra with only one primitive operator (tentative) (please check/critique)

Quote from dandl on May 16, 2021, 3:01 pmQuote from AntC on May 16, 2021, 9:47 amQuote from dandl on May 16, 2021, 7:28 amQuote from AntC on May 16, 2021, 2:53 amQuote from dandl on May 16, 2021, 12:30 amWould it be helpful to start a new thread and set out what you are trying to achieve? Rather than this quibbling over mathematical nuances that may not even matter, and a heading that no longer seems relevant?

A reasonable question @dandl. I've just re-read the o.p. I think 'Motivation' still stands. I think '(Empty) Relations denoting headings' still stands.

I don't find Motivation helpful in understanding where you want to get to. It's just a list of issues.

Headings: who needs them? This is an algebra closed over relations, but the behaviour of operators is dictated by the headings of their arguments, and using relations to stand in for their headings doesn't really change anything.

Headings? I don't have them. The algebra is single-sorted. It's just that in

TTM-land it's easier to talk in terms of headings and bodies. Instead of 'heading' you can put 'type of relation value'.I thought that's what I said. Just because it's only about relations doesn't stop you talking about properties of relations.

Only one operator? I think you've abandoned that. So a new thread might be overdue.

It's "only one primitive operator". I've defined

`NotMatching`

in terms of it; I've defined`DUM = DEE NotMatching DEE`

.If you were going to pick a single primitive, that's the one to go for, but I still don't think it works. And you can't define

`DEE`

and also claim that every possible relation already exists.The rest of your comment betrays that you still think this is something 'executable'. Then the third section of the o.p. still stands.

The algebra allows you to write WFFs. When variables in the WFF are bound to values it can be evaluated to yield a result (like Pythagoras). What other purpose did you have in mind?

Showing that two queries are equivalent. Also expressing side-conditions on that equivalence -- such as the participant relations must have disjoint headings. Note I haven't

in the algebraspecified what is a heading, what is a tuple, what is a`<A, v>`

pair. I've given no specification of a value. So good luck with trying to evaluate non-values -- or perhaps I should say "ghost" values.`r1, r2, s ...`

are variables for/range over values.There are no queries. An algebra lets you write WFFs with free variables, and I think that's what you're doing. Queries are explicit requests for evaluating an expression with values bound to its free variables.

Addit:You're very welcome to assume relations are as specified in Appendix A 'FORMAL DEFINITIONS'; you won't mis-understand. But I haven't assumed or specified anything about relations being sets or pairs of sets or pairs of a set-of-pairs with a set-of-sets-of-pairs. There's no set operations in the algebra. There's only operators and variables embedded in FOPL-with-equality.All the algebra can do is inspect its argument. If it's

`DUM`

then ... If it's the identity for`NatJoin`

then ... How do I tell if some value is the identity for`NatJoin`

? I apply`DEE NatJoin r`

to all`r`

in my infinity of values; if each application returns`r`

(and no other candidate returns`r`

for all`r`

), then I have`DEE`

.I'm fine with that. Kind of like zero and one in arithmetic.

For example: if I can talk about headings, I can characterise what it is for a relation (value) to have exactly one more attribute than another; I can characterise what it is for a relation to have exactly one more tuple than another with the same heading. I can say that characterising one more attribute on top of one more tuple achieves the same properties as characterising one more tuple on top of one more attribute. I can characterise starting from

`DUM`

and building up.Which I think is the correct approach. But you are going to have to address the problem of creating new values. IMO once you have relcons restriction is just a semijoin and new value is just a join: it's relations all the way down. Lovely!

So arguably you can construct an algebra of dyadic functions that is closed over relations. Given the starting point of

`NotMatching`

it's at least possible you can cover all the joins and set operations. That just leaves Coss's Restrict and Project, plus TD's Extend and Rename. About halfway.

Quote from AntC on May 16, 2021, 9:47 amQuote from dandl on May 16, 2021, 7:28 amQuote from AntC on May 16, 2021, 2:53 amQuote from dandl on May 16, 2021, 12:30 amWould it be helpful to start a new thread and set out what you are trying to achieve? Rather than this quibbling over mathematical nuances that may not even matter, and a heading that no longer seems relevant?

A reasonable question @dandl. I've just re-read the o.p. I think 'Motivation' still stands. I think '(Empty) Relations denoting headings' still stands.

I don't find Motivation helpful in understanding where you want to get to. It's just a list of issues.

Headings: who needs them? This is an algebra closed over relations, but the behaviour of operators is dictated by the headings of their arguments, and using relations to stand in for their headings doesn't really change anything.

Headings? I don't have them. The algebra is single-sorted. It's just that in

TTM-land it's easier to talk in terms of headings and bodies. Instead of 'heading' you can put 'type of relation value'.

I thought that's what I said. Just because it's only about relations doesn't stop you talking about properties of relations.

Only one operator? I think you've abandoned that. So a new thread might be overdue.

It's "only one primitive operator". I've defined

`NotMatching`

in terms of it; I've defined`DUM = DEE NotMatching DEE`

.

If you were going to pick a single primitive, that's the one to go for, but I still don't think it works. And you can't define `DEE`

and also claim that every possible relation already exists.

The rest of your comment betrays that you still think this is something 'executable'. Then the third section of the o.p. still stands.

The algebra allows you to write WFFs. When variables in the WFF are bound to values it can be evaluated to yield a result (like Pythagoras). What other purpose did you have in mind?

Showing that two queries are equivalent. Also expressing side-conditions on that equivalence -- such as the participant relations must have disjoint headings. Note I haven't

in the algebraspecified what is a heading, what is a tuple, what is a`<A, v>`

pair. I've given no specification of a value. So good luck with trying to evaluate non-values -- or perhaps I should say "ghost" values.`r1, r2, s ...`

are variables for/range over values.

There are no queries. An algebra lets you write WFFs with free variables, and I think that's what you're doing. Queries are explicit requests for evaluating an expression with values bound to its free variables.

Addit:You're very welcome to assume relations are as specified in Appendix A 'FORMAL DEFINITIONS'; you won't mis-understand. But I haven't assumed or specified anything about relations being sets or pairs of sets or pairs of a set-of-pairs with a set-of-sets-of-pairs. There's no set operations in the algebra. There's only operators and variables embedded in FOPL-with-equality.

All the algebra can do is inspect its argument. If it's

`DUM`

then ... If it's the identity for`NatJoin`

then ... How do I tell if some value is the identity for`NatJoin`

? I apply`DEE NatJoin r`

to all`r`

in my infinity of values; if each application returns`r`

(and no other candidate returns`r`

for all`r`

), then I have`DEE`

.

I'm fine with that. Kind of like zero and one in arithmetic.

For example: if I can talk about headings, I can characterise what it is for a relation (value) to have exactly one more attribute than another; I can characterise what it is for a relation to have exactly one more tuple than another with the same heading. I can say that characterising one more attribute on top of one more tuple achieves the same properties as characterising one more tuple on top of one more attribute. I can characterise starting from

`DUM`

and building up.Which I think is the correct approach. But you are going to have to address the problem of creating new values. IMO once you have relcons restriction is just a semijoin and new value is just a join: it's relations all the way down. Lovely!

So arguably you can construct an algebra of dyadic functions that is closed over relations. Given the starting point of `NotMatching`

it's at least possible you can cover all the joins and set operations. That just leaves Coss's Restrict and Project, plus TD's Extend and Rename. About halfway.

Quote from AntC on May 20, 2021, 8:00 amQuote from tobega on May 16, 2021, 8:41 amI'll give a second reply, as a hook to report on further research (which has only elaborated the ineffability) ...

IIUC, Dee is the identity for natural join, but Dum would be the zero. Also, it seems Dum might be the identity for inner union, and Dee would be the zero. Or is it? Does the identity for inner union need to be the empty relation with maximum heading? Could/should Dum have the maximum heading (oh, that's Dumpty)? Yes, I think so, Dumpty is also the true zero for natural join, not Dum.

The closest (simplish) analogue I can think of is the role of zero in multiplication of Naturals:

`1 × x = x`

, for all`x`

, so`1`

is the identity for`×`

, as`DEE`

is the identity for`NatJoin`

.`0 × x = 0`

, for all`x`

, so`0`

is the absorbing element for`×`

. So its effect is 'sideways' relative to`1`

.`DUM`

's effect is sideways in the sense:`DUM InnerUnion x`

yields`DUM`

if`x`

is empty, otherwise`DEE`

. (Compare a sign function`signum`

on Naturals that returns`0`

or`1`

.)- There's a handy corollary:
`DUM NatJoin x`

yields`x`

if`x`

is empty, otherwise something not equal`x`

. (Unfortunately, stipulating that corollary as an equivalence is not sufficient to 'fix'`DUM`

. I can't say the 'something not equal`x`

' is`emptify(x)`

, because I haven't independently defined what is an empty relation.)- But the analogue breaks down fairly quickly: there's a minimal Natural, but not a maximal; and
- we can build the Naturals by starting at
`0`

and applying a`successor`

function; similarly we can 'unbuild' the Naturals by applying a`predecessor`

that's the inverse of`successor`

.- There's no 'definite procedure' to build all relation values starting from some seed: we could start from
`DUM`

and add a tuple, =`DEE`

, but we can't add any more tuples with that heading; we could start from`DUM`

and add an attribute (the choice of attribute is not definite, I suppose we could apply some ordering to attribute names and pick the least); perhaps we take next the empty relation at that heading; but now we need to add a tuple (at least one), and what attribute value do we pick -- again the choice is not definite.- Equally there's no definite procedure to 'unbuild' relations: remove some tuple arbitrarily? remove some attribute arbitrarily? We want that we could do those in either order and arrive at the same answer -- but in what sense are we removing the 'same' tuple if we first remove some attribute: projecting the attribute away might have reduced cardinality by more than one, IOW squished several tuples into one.
So that's why I'm taking the 'Universe' of relation values as given -- as lattice theory takes its set, and it's entirely happy if the set is infinite, providing we can identify the minimal and maximal.

`DEE`

(maximal/top),`Dumpty`

(minimal/lowest),`DUM`

('leftmost' ?) are in there somewhere, I just have to specify how to find them, and in sufficient detail that's unique.If we start with Dee and Dumpty (it perhaps remains to be proven that the algebra from that is sane), ...

Yes it's sane that far. Because all we need to identify them uniquely is a single operation

`NaturalJoin`

, acting as lattice`meet`

, with a (provably unique) identity value and a (provably unique) absorbing value.we can never create Dum by natural join and inner union.

Correct. But my hope was to introduce additional operations that were well-behaved (

`NotMatching, Project, Remove`

,`emptify( )`

) then fix`DUM`

in terms of them -- it's variously the identity or absorbing or idempotent (kinda) element for those -- but be careful they're not commutative. That approach presumed those other operations could be 'fixed' in terms of`NatJoin, InnerUnion`

. And/or I could specify a bunch of properties about those operations, and a bunch of properties of`DUM`

, then 'nail' all of them together with

`DUM = emptify(DEE)`

`emptify(x) = x NatJoin DUM`

- As I have it, either of those as axioms implies the other; but neither is sufficient to 'fix' enough.
- The handy corollary I mentioned above:
`x NatJoin DUM ≠ x ≡ x InnerUnion DUM = DEE`

does greatly limit what`DUM`

could be, but not sufficient to 'fix' it.It's not as if counter-examples need be anything very weird or degenerate. So if Vadim is still listening ... There's a counter-example with just 4 elements: suppose in this Universe there's only one attribute, and its type has only value, then there's a single relation with non-empty heading (degree 1) and non-empty body (cardinality 1), call it

`R11`

; the 4 elements`DEE, DUM, Dumpty, R11`

. The axioms and operators all work if we take`R11`

as a false`DUM`

, and leave the true`DUM`

as just some other element.It's not that I've introduced a contradiction. There's no counter-examples to the properties I expect for

`DUM`

and the operators. It's just that neither are those properties inferable. Or at least inferable in any reasonable timescale -- if we had all of mathematical time ... maybe. If I (for example) had a proof of the Collatz Conjecture, I could plug that in and derive stuff effortlessly. (This position is not unprecedented: PLT higher-order type inference for possibly-non-terminating function definitions needs the same trick.)I could write those expected properties as axioms. (That wouldn't be wrong, provided I didn't introduce contradictions.) But still it doesn't derive equivalences between what should be equivalent queries. These theorems aren't provable:

`r1 project r2 = r1 Remove (r1 Remove r2)`

`r1 Remove (s1 NatJoin s2) = (r1 Remove s1) Remove s2`

-- required by Appendix A: I can`<REMOVE>`

a bunch of attributes by successively removing each one, IOW`<REMOVE> attribute-comma-list`

must be equivalent to a nesting of`((r <REMOVE> A1) <REMOVE> A2 ...)`

. I'm taking`s1`

as a relation with attribute`A1`

only;`s2`

as the relation with all other attributes that'll be successively unpeeled as`A2, ...`

;`s1 NatJoin s2`

is Cartesian product, where we're only interested in the resulting heading.I haven't yet gone as far as running inference over a set-up with all four operators defined along with

`DUM`

; perhaps that'll magically fix it all together. To solve a set of simultaneous equations in 5 variables, how many equations does it take? And what if 4 of the 'variables' are functions that must be defined for all elements in the 'Universe'? Note that`project, NotMatching`

(say) must be defined even if the headings of the operands are disjoint -- just as`NatJoin`

degnerates to Cartesian product, or if an operand is`DUM`

-- which is kinda disjoint (no attributes in common) but actually a subset.

Quote from tobega on May 16, 2021, 8:41 am

I'll give a second reply, as a hook to report on further research (which has only elaborated the ineffability) ...

IIUC, Dee is the identity for natural join, but Dum would be the zero. Also, it seems Dum might be the identity for inner union, and Dee would be the zero. Or is it? Does the identity for inner union need to be the empty relation with maximum heading? Could/should Dum have the maximum heading (oh, that's Dumpty)? Yes, I think so, Dumpty is also the true zero for natural join, not Dum.

The closest (simplish) analogue I can think of is the role of zero in multiplication of Naturals:

`1 × x = x`

, for all`x`

, so`1`

is the identity for`×`

, as`DEE`

is the identity for`NatJoin`

.`0 × x = 0`

, for all`x`

, so`0`

is the absorbing element for`×`

. So its effect is 'sideways' relative to`1`

.`DUM`

's effect is sideways in the sense:`DUM InnerUnion x`

yields`DUM`

if`x`

is empty, otherwise`DEE`

. (Compare a sign function`signum`

on Naturals that returns`0`

or`1`

.)- There's a handy corollary:
`DUM NatJoin x`

yields`x`

if`x`

is empty, otherwise something not equal`x`

. (Unfortunately, stipulating that corollary as an equivalence is not sufficient to 'fix'`DUM`

. I can't say the 'something not equal`x`

' is`emptify(x)`

, because I haven't independently defined what is an empty relation.) - But the analogue breaks down fairly quickly: there's a minimal Natural, but not a maximal; and
- we can build the Naturals by starting at
`0`

and applying a`successor`

function; similarly we can 'unbuild' the Naturals by applying a`predecessor`

that's the inverse of`successor`

. - There's no 'definite procedure' to build all relation values starting from some seed: we could start from
`DUM`

and add a tuple, =`DEE`

, but we can't add any more tuples with that heading; we could start from`DUM`

and add an attribute (the choice of attribute is not definite, I suppose we could apply some ordering to attribute names and pick the least); perhaps we take next the empty relation at that heading; but now we need to add a tuple (at least one), and what attribute value do we pick -- again the choice is not definite. - Equally there's no definite procedure to 'unbuild' relations: remove some tuple arbitrarily? remove some attribute arbitrarily? We want that we could do those in either order and arrive at the same answer -- but in what sense are we removing the 'same' tuple if we first remove some attribute: projecting the attribute away might have reduced cardinality by more than one, IOW squished several tuples into one.

So that's why I'm taking the 'Universe' of relation values as given -- as lattice theory takes its set, and it's entirely happy if the set is infinite, providing we can identify the minimal and maximal. `DEE`

(maximal/top), `Dumpty`

(minimal/lowest), `DUM`

('leftmost' ?) are in there somewhere, I just have to specify how to find them, and in sufficient detail that's unique.

If we start with Dee and Dumpty (it perhaps remains to be proven that the algebra from that is sane), ...

Yes it's sane that far. Because all we need to identify them uniquely is a single operation `NaturalJoin`

, acting as lattice `meet`

, with a (provably unique) identity value and a (provably unique) absorbing value.

we can never create Dum by natural join and inner union.

Correct. But my hope was to introduce additional operations that were well-behaved (`NotMatching, Project, Remove`

, `emptify( )`

) then fix `DUM`

in terms of them -- it's variously the identity or absorbing or idempotent (kinda) element for those -- but be careful they're not commutative. That approach presumed those other operations could be 'fixed' in terms of `NatJoin, InnerUnion`

. And/or I could specify a bunch of properties about those operations, and a bunch of properties of `DUM`

, then 'nail' all of them together with

`DUM = emptify(DEE)`

`emptify(x) = x NatJoin DUM`

- As I have it, either of those as axioms implies the other; but neither is sufficient to 'fix' enough.
- The handy corollary I mentioned above:
`x NatJoin DUM ≠ x ≡ x InnerUnion DUM = DEE`

does greatly limit what`DUM`

could be, but not sufficient to 'fix' it.

It's not as if counter-examples need be anything very weird or degenerate. So if Vadim is still listening ... There's a counter-example with just 4 elements: suppose in this Universe there's only one attribute, and its type has only value, then there's a single relation with non-empty heading (degree 1) and non-empty body (cardinality 1), call it `R11`

; the 4 elements `DEE, DUM, Dumpty, R11`

. The axioms and operators all work if we take `R11`

as a false `DUM`

, and leave the true `DUM`

as just some other element.

It's not that I've introduced a contradiction. There's no counter-examples to the properties I expect for `DUM`

and the operators. It's just that neither are those properties inferable. Or at least inferable in any reasonable timescale -- if we had all of mathematical time ... maybe. If I (for example) had a proof of the Collatz Conjecture, I could plug that in and derive stuff effortlessly. (This position is not unprecedented: PLT higher-order type inference for possibly-non-terminating function definitions needs the same trick.)

I could write those expected properties as axioms. (That wouldn't be wrong, provided I didn't introduce contradictions.) But still it doesn't derive equivalences between what should be equivalent queries. These theorems aren't provable:

`r1 project r2 = r1 Remove (r1 Remove r2)`

`r1 Remove (s1 NatJoin s2) = (r1 Remove s1) Remove s2`

-- required by Appendix A: I can`<REMOVE>`

a bunch of attributes by successively removing each one, IOW`<REMOVE> attribute-comma-list`

must be equivalent to a nesting of`((r <REMOVE> A1) <REMOVE> A2 ...)`

. I'm taking`s1`

as a relation with attribute`A1`

only;`s2`

as the relation with all other attributes that'll be successively unpeeled as`A2, ...`

;`s1 NatJoin s2`

is Cartesian product, where we're only interested in the resulting heading.

I haven't yet gone as far as running inference over a set-up with all four operators defined along with `DUM`

; perhaps that'll magically fix it all together. To solve a set of simultaneous equations in 5 variables, how many equations does it take? And what if 4 of the 'variables' are functions that must be defined for all elements in the 'Universe'? Note that `project, NotMatching`

(say) must be defined even if the headings of the operands are disjoint -- just as `NatJoin`

degnerates to Cartesian product, or if an operand is `DUM`

-- which is kinda disjoint (no attributes in common) but actually a subset.

Quote from Vadim on May 20, 2021, 3:08 pmQuote from AntC on May 20, 2021, 8:00 am

There's a counter-example with just 4 elements: suppose in this Universe there's only one attribute, and its type has only value, then there's a single relation with non-empty heading (degree 1) and non-empty body (cardinality 1), call it

`R11`

; the 4 elements`DEE, DUM, Dumpty, R11`

. The axioms and operators all work if we take`R11`

as a false`DUM`

, and leave the true`DUM`

as just some other element.Another example: take the universe inhabited by 4 unary relations [latex] X = \langle \{ p \}, \{ \langle 0 \rangle \}\rangle [/latex], [latex] Y = \langle \{ p \}, \{ \langle 1 \rangle \}\rangle [/latex], [latex] X \wedge Y [/latex], [latex] X \vee Y [/latex]. Some may argue that there are "genuine" DUM and DEE hidden somewhere in that universe, but I'd think their roles can perfectly be played by unary relations, so that those 4 relations is all that you will ever see.

Again, there is "definition" of

`DEE`

and`DUM`

in set theoretic terms, but my faith in the curly brackets and the membership symbol has been compromized lately. Perhaps, the best way to proceed is, as you have mentioned before, not to pretend that [latex]R_{00} = DUM[/latex], [latex]R_{01} = DEE[/latex] .I could write those expected properties as axioms. (That wouldn't be wrong, provided I didn't introduce contradictions.) But still it doesn't derive equivalences between what should be equivalent queries. These theorems aren't provable:

`r1 project r2 = r1 Remove (r1 Remove r2)`

`r1 Remove (s1 NatJoin s2) = (r1 Remove s1) Remove s2`

-- required by Appendix A: I can`<REMOVE>`

a bunch of attributes by successively removing each one, IOW`<REMOVE> attribute-comma-list`

must be equivalent to a nesting of`((r <REMOVE> A1) <REMOVE> A2 ...)`

. I'm taking`s1`

as a relation with attribute`A1`

only;`s2`

as the relation with all other attributes that'll be successively unpeeled as`A2, ...`

;`s1 NatJoin s2`

is Cartesian product, where we're only interested in the resulting heading.I haven't yet gone as far as running inference over a set-up with all four operators defined along with

`DUM`

; perhaps that'll magically fix it all together. To solve a set of simultaneous equations in 5 variables, how many equations does it take? And what if 4 of the 'variables' are functions that must be defined for all elements in the 'Universe'? Note that`project, NotMatching`

(say) must be defined even if the headings of the operands are disjoint -- just as`NatJoin`

degnerates to Cartesian product, or if an operand is`DUM`

-- which is kinda disjoint (no attributes in common) but actually a subset.Is your version of

`<REMOVE>`

total? Also, by`project`

do you mean classic project, or inner union?P.S. I'm using the total unary version of

`<REMOVE>`

called`<INVERSE>`

. The axioms for`<INVERSE>`

are the dual versions of the axioms for the`<NOT>`

. I agree that perhaps a binary incarnation of the`<INVERSE>`

operation, which would be domain and attribute set independent, might have its merits, but it would certainly make the axiom system more complex.

Quote from AntC on May 20, 2021, 8:00 am

There's a counter-example with just 4 elements: suppose in this Universe there's only one attribute, and its type has only value, then there's a single relation with non-empty heading (degree 1) and non-empty body (cardinality 1), call it

`R11`

; the 4 elements`DEE, DUM, Dumpty, R11`

. The axioms and operators all work if we take`R11`

as a false`DUM`

, and leave the true`DUM`

as just some other element.

Another example: take the universe inhabited by 4 unary relations X = \langle \{ p \}, \{ \langle 0 \rangle \}\rangle , Y = \langle \{ p \}, \{ \langle 1 \rangle \}\rangle , X \wedge Y , X \vee Y . Some may argue that there are "genuine" DUM and DEE hidden somewhere in that universe, but I'd think their roles can perfectly be played by unary relations, so that those 4 relations is all that you will ever see.

Again, there is "definition" of `DEE`

and `DUM`

in set theoretic terms, but my faith in the curly brackets and the membership symbol has been compromized lately. Perhaps, the best way to proceed is, as you have mentioned before, not to pretend that R_{00} = DUM, R_{01} = DEE .

`r1 project r2 = r1 Remove (r1 Remove r2)`

`r1 Remove (s1 NatJoin s2) = (r1 Remove s1) Remove s2`

-- required by Appendix A: I can`<REMOVE>`

a bunch of attributes by successively removing each one, IOW`<REMOVE> attribute-comma-list`

must be equivalent to a nesting of`((r <REMOVE> A1) <REMOVE> A2 ...)`

. I'm taking`s1`

as a relation with attribute`A1`

only;`s2`

as the relation with all other attributes that'll be successively unpeeled as`A2, ...`

;`s1 NatJoin s2`

is Cartesian product, where we're only interested in the resulting heading.`DUM`

; perhaps that'll magically fix it all together. To solve a set of simultaneous equations in 5 variables, how many equations does it take? And what if 4 of the 'variables' are functions that must be defined for all elements in the 'Universe'? Note that`project, NotMatching`

(say) must be defined even if the headings of the operands are disjoint -- just as`NatJoin`

degnerates to Cartesian product, or if an operand is`DUM`

-- which is kinda disjoint (no attributes in common) but actually a subset.

Is your version of `<REMOVE>`

total? Also, by `project`

do you mean classic project, or inner union?

P.S. I'm using the total unary version of `<REMOVE>`

called `<INVERSE>`

. The axioms for `<INVERSE>`

are the dual versions of the axioms for the `<NOT>`

. I agree that perhaps a binary incarnation of the `<INVERSE>`

operation, which would be domain and attribute set independent, might have its merits, but it would certainly make the axiom system more complex.

Quote from AntC on May 21, 2021, 12:44 amQuote from Vadim on May 20, 2021, 3:08 pmQuote from AntC on May 20, 2021, 8:00 am

There's a counter-example with just 4 elements: suppose in this Universe there's only one attribute, and its type has only value, then there's a single relation with non-empty heading (degree 1) and non-empty body (cardinality 1), call it

`R11`

; the 4 elements`DEE, DUM, Dumpty, R11`

. The axioms and operators all work if we take`R11`

as a false`DUM`

, and leave the true`DUM`

as just some other element.Another example: take the universe inhabited by 4 unary relations [latex] X = \langle \{ p \}, \{ \langle 0 \rangle \}\rangle [/latex], [latex] Y = \langle \{ p \}, \{ \langle 1 \rangle \}\rangle [/latex], [latex] X \wedge Y [/latex], [latex] X \vee Y [/latex]. Some may argue that there are "genuine" DUM and DEE hidden somewhere in that universe, but I'd think their roles can perfectly be played by unary relations, so that those 4 relations is all that you will ever see.

Edit:some mistakes here, I'll expand more in my reply to Vadim's reply:There is a

`DEE`

-- that is, a relation whose heading is a subset of every other relation (not necessarily proper), and content a~~subset~~superset of every other relation projected on that heading. That is`X ^ Y`

.There isn't a

`DUM`

-- that is a relation whose headings is the subset of every other relation, and content a subset of every other relation projected on that heading. (Neither`X`

's nor`Y`

's body are a subset of the other.) [Correction:there is a relation like that subset, subset -- but that one is`Dumpty`

= lattice bottom. But it's not`DUM`

because it isn't immediately adjacent to`DEE`

. ] But I suspect my definitions would work 'fine' (as well/badly as I'm currently experiencing) by interpreting`DUM = X`

. But equally well/badly by interpreting`DUM = Y`

. The choice is arbitrary -- which is the problem.Again, there is "definition" of

`DEE`

and`DUM`

in set theoretic terms, but my faith in the curly brackets and the membership symbol has been compromized lately. Perhaps, the best way to proceed is, as you have mentioned before, not to pretend that [latex]R_{00} = DUM[/latex], [latex]R_{01} = DEE[/latex] .Lattice definitions don't know anything about set contents nor headings. We're given a universe of elements (i.e. relation values -- we assume all possible values for some set of `<attribute name, type>` pairs). Our problem is to identify certain critical elements amongst them.

For comparison: If we start with an unbounded lattice (set of elements), we can always 'invent' a supremum/infimum. If we start with a set of relations without an equivalent to

`DUM`

, we can always 'invent' it. Just define it into existence -- if only there were precise enough definitions.Taking lattice top as

`DEE`

is I think fine. D&D don't have a cute name for lattice bottom, but I don't think there's much need to mention it. We take`DEE`

equivalent to`TRUE`

where we have projected away all attributes/obtained a proposition rather than a predicate. (Are there any Suppliers in Leeds? Yes or No.) Then we do need an equivalent to`FALSE`

and it must have as few attributes as`TRUE`

. This is quite apart from the role of`DUM`

in being the possible result of`r1 Project r2`

(where they have no attributes in common,`r1`

empty)`r1 Remove r1`

(where`r1`

is empty).

`r1 project r2 = r1 Remove (r1 Remove r2)`

`r1 Remove (s1 NatJoin s2) = (r1 Remove s1) Remove s2`

-- required by Appendix A: I can`<REMOVE>`

a bunch of attributes by successively removing each one, IOW`<REMOVE> attribute-comma-list`

must be equivalent to a nesting of`((r <REMOVE> A1) <REMOVE> A2 ...)`

. I'm taking`s1`

as a relation with attribute`A1`

only;`s2`

as the relation with all other attributes that'll be successively unpeeled as`A2, ...`

;`s1 NatJoin s2`

is Cartesian product, where we're only interested in the resulting heading.`DUM`

; perhaps that'll magically fix it all together. To solve a set of simultaneous equations in 5 variables, how many equations does it take? And what if 4 of the 'variables' are functions that must be defined for all elements in the 'Universe'? Note that`project, NotMatching`

(say) must be defined even if the headings of the operands are disjoint -- just as`NatJoin`

degnerates to Cartesian product, or if an operand is`DUM`

-- which is kinda disjoint (no attributes in common) but actually a subset.Is your version of

`<REMOVE>`

total? Also, by`project`

do you mean classic project, or inner union?

`r1 project r2`

=df`r1 InnerUnion emptify(r2)`

(many possible definitions for`emptify( )`

, which ought to be equivalent but aren't provably so.)`r1 Remove r2 = r1 project s ≡ emptify(r1 InnerUnion s) NatJoin emptify(r1 InnerUnion r2) = emptify(r1) & emptify((s InnerUnion r1) InnerUnion r2) = emptify(DEE).`

That is,`Remove`

is equivalent to`project`

on any`s`

such that`s`

has at least the attributes of`r1`

not in`r2`

.So yes I'm aiming to make

`project, Remove`

total (defined for all possible operands). I've added several further axioms for`Remove`

which ought to be implied by that (and aren't countered by Mace4), but aren't provable, it seems.Why is there that 'at least the attributes' business for

`s`

? Because I want an equivalence in the definition, to strengthen inference. See below about headings for the attributes to project/remove.P.S. I'm using the total unary version of

`<REMOVE>`

called`<INVERSE>`

. The axioms for`<INVERSE>`

are the dual versions of the axioms for the`<NOT>`

. I agree that perhaps a binary incarnation of the`<INVERSE>`

operation, which would be domain and attribute set independent, might have its merits, but it would certainly make the axiom system more complex.I'm pretty sure using

`<NOT>, <INVERSE>`

run into the same problems of non-provability. I think the difficulty is this:

`NatJoin, InnerUnion`

are well-defined no matter what the headings of their operands. Indeed we deliberately exploit unequal headings for`NatJoin`

: if they're the same, thats`INTERSECT`

; if they don't overlap, that's Cartesian product; if one is a subset, that's`WHERE`

; if there's a partial overlap, that's`EXTEND`

. (To be more precise, the axiom system takes`NatJoin`

to be well-defined; then it follows from the absorption laws that`InnerUnion`

is well-defined. For the other operators, we don't have definitions as strong as the absorption laws.- We want
`Matching, NotMatching, project, Remove`

to be well-defined no matter what the headings of operands. And for`Matching, NotMatching`

that's not too bad, because the heading of the result is to be the heading of the left operand. But the heading of the r.h. operand to`project, Remove`

could include any rubbishy attributes that don't appear in the l.h. operand, they're just ignored/they don't have any influence on the result.- For
`Matching, NotMatching, project, Remove`

the bodies of the r.h. operand could include any rubbishy tuples that don't appear in the l.h. operand, again they're just ignored.- So you want
`r1 Remove r2`

=`r1 project (<INVERSE> r2)`

=`r1 InnerUnion emptify?(<INVERSE> r2)`

. Again that must be well defined if`r2`

has attributes outside`r1`

, and/or`<INVERSE> r2`

has attributes outside`r1`

. For`emptify?( )`

you still need to fix something -- perhaps`emptify?(r) = r NatJoin DUM; DUM = <NOT> DEE`

?- You can define
`<INVERSE> (<INVERSE> r) = r; <NOT> (<NOT> r) = r`

. I think that won't fix either operation to what you want. For example, those are 'solved' if`<INVERSE>, <NOT>`

are merely identity. I've added stupid/ugly axioms like`emptify(DEE) ≠ DEE`

;`DUM`

must be adjacent to`DEE`

. That's not enough to fix anything. (So in your 4-element model, it merely fixes that`R00`

is the element 'opposite'`R11`

-- either could be`X, Y`

, the choice is arbitrary.)

Quote from Vadim on May 20, 2021, 3:08 pmQuote from AntC on May 20, 2021, 8:00 am

`R11`

; the 4 elements`DEE, DUM, Dumpty, R11`

. The axioms and operators all work if we take`R11`

as a false`DUM`

, and leave the true`DUM`

as just some other element.Another example: take the universe inhabited by 4 unary relations X = \langle \{ p \}, \{ \langle 0 \rangle \}\rangle , Y = \langle \{ p \}, \{ \langle 1 \rangle \}\rangle , X \wedge Y , X \vee Y . Some may argue that there are "genuine" DUM and DEE hidden somewhere in that universe, but I'd think their roles can perfectly be played by unary relations, so that those 4 relations is all that you will ever see.

**Edit:** some mistakes here, I'll expand more in my reply to Vadim's reply:

There is a `DEE`

-- that is, a relation whose heading is a subset of every other relation (not necessarily proper), and content a ~~subset~~ superset of every other relation projected on that heading. That is `X ^ Y`

.

There isn't a `DUM`

-- that is a relation whose headings is the subset of every other relation, and content a subset of every other relation projected on that heading. (Neither `X`

's nor `Y`

's body are a subset of the other.) [**Correction:** there is a relation like that subset, subset -- but that one is `Dumpty`

= lattice bottom. But it's not `DUM`

because it isn't immediately adjacent to `DEE`

. ] But I suspect my definitions would work 'fine' (as well/badly as I'm currently experiencing) by interpreting `DUM = X`

. But equally well/badly by interpreting `DUM = Y`

. The choice is arbitrary -- which is the problem.

Again, there is "definition" of

`DEE`

and`DUM`

in set theoretic terms, but my faith in the curly brackets and the membership symbol has been compromized lately. Perhaps, the best way to proceed is, as you have mentioned before, not to pretend that R_{00} = DUM, R_{01} = DEE .

Lattice definitions don't know anything about set contents nor headings. We're given a universe of elements (i.e. relation values -- we assume all possible values for some set of `<attribute name, type>` pairs). Our problem is to identify certain critical elements amongst them.

For comparison: If we start with an unbounded lattice (set of elements), we can always 'invent' a supremum/infimum. If we start with a set of relations without an equivalent to `DUM`

, we can always 'invent' it. Just define it into existence -- if only there were precise enough definitions.

Taking lattice top as `DEE`

is I think fine. D&D don't have a cute name for lattice bottom, but I don't think there's much need to mention it. We take `DEE`

equivalent to `TRUE`

where we have projected away all attributes/obtained a proposition rather than a predicate. (Are there any Suppliers in Leeds? Yes or No.) Then we do need an equivalent to `FALSE`

and it must have as few attributes as `TRUE`

. This is quite apart from the role of `DUM`

in being the possible result of `r1 Project r2`

(where they have no attributes in common, `r1`

empty) `r1 Remove r1`

(where `r1`

is empty).

`r1 project r2 = r1 Remove (r1 Remove r2)`

`r1 Remove (s1 NatJoin s2) = (r1 Remove s1) Remove s2`

-- required by Appendix A: I can`<REMOVE>`

a bunch of attributes by successively removing each one, IOW`<REMOVE> attribute-comma-list`

must be equivalent to a nesting of`((r <REMOVE> A1) <REMOVE> A2 ...)`

. I'm taking`s1`

as a relation with attribute`A1`

only;`s2`

as the relation with all other attributes that'll be successively unpeeled as`A2, ...`

;`s1 NatJoin s2`

is Cartesian product, where we're only interested in the resulting heading.`DUM`

; perhaps that'll magically fix it all together. To solve a set of simultaneous equations in 5 variables, how many equations does it take? And what if 4 of the 'variables' are functions that must be defined for all elements in the 'Universe'? Note that`project, NotMatching`

(say) must be defined even if the headings of the operands are disjoint -- just as`NatJoin`

degnerates to Cartesian product, or if an operand is`DUM`

-- which is kinda disjoint (no attributes in common) but actually a subset.Is your version of

`<REMOVE>`

total? Also, by`project`

do you mean classic project, or inner union?

`r1 project r2`

=df`r1 InnerUnion emptify(r2)`

(many possible definitions for`emptify( )`

, which ought to be equivalent but aren't provably so.)`r1 Remove r2 = r1 project s ≡ emptify(r1 InnerUnion s) NatJoin emptify(r1 InnerUnion r2) = emptify(r1) & emptify((s InnerUnion r1) InnerUnion r2) = emptify(DEE).`

That is,`Remove`

is equivalent to`project`

on any`s`

such that`s`

has at least the attributes of`r1`

not in`r2`

.

So yes I'm aiming to make `project, Remove`

total (defined for all possible operands). I've added several further axioms for `Remove`

which ought to be implied by that (and aren't countered by Mace4), but aren't provable, it seems.

Why is there that 'at least the attributes' business for `s`

? Because I want an equivalence in the definition, to strengthen inference. See below about headings for the attributes to project/remove.

`<REMOVE>`

called`<INVERSE>`

. The axioms for`<INVERSE>`

are the dual versions of the axioms for the`<NOT>`

. I agree that perhaps a binary incarnation of the`<INVERSE>`

operation, which would be domain and attribute set independent, might have its merits, but it would certainly make the axiom system more complex.

I'm pretty sure using `<NOT>, <INVERSE>`

run into the same problems of non-provability. I think the difficulty is this:

`NatJoin, InnerUnion`

are well-defined no matter what the headings of their operands. Indeed we deliberately exploit unequal headings for`NatJoin`

: if they're the same, thats`INTERSECT`

; if they don't overlap, that's Cartesian product; if one is a subset, that's`WHERE`

; if there's a partial overlap, that's`EXTEND`

. (To be more precise, the axiom system takes`NatJoin`

to be well-defined; then it follows from the absorption laws that`InnerUnion`

is well-defined. For the other operators, we don't have definitions as strong as the absorption laws.- We want
`Matching, NotMatching, project, Remove`

to be well-defined no matter what the headings of operands. And for`Matching, NotMatching`

that's not too bad, because the heading of the result is to be the heading of the left operand. But the heading of the r.h. operand to`project, Remove`

could include any rubbishy attributes that don't appear in the l.h. operand, they're just ignored/they don't have any influence on the result. - For
`Matching, NotMatching, project, Remove`

the bodies of the r.h. operand could include any rubbishy tuples that don't appear in the l.h. operand, again they're just ignored. - So you want
`r1 Remove r2`

=`r1 project (<INVERSE> r2)`

=`r1 InnerUnion emptify?(<INVERSE> r2)`

. Again that must be well defined if`r2`

has attributes outside`r1`

, and/or`<INVERSE> r2`

has attributes outside`r1`

. For`emptify?( )`

you still need to fix something -- perhaps`emptify?(r) = r NatJoin DUM; DUM = <NOT> DEE`

? - You can define
`<INVERSE> (<INVERSE> r) = r; <NOT> (<NOT> r) = r`

. I think that won't fix either operation to what you want. For example, those are 'solved' if`<INVERSE>, <NOT>`

are merely identity. I've added stupid/ugly axioms like`emptify(DEE) ≠ DEE`

;`DUM`

must be adjacent to`DEE`

. That's not enough to fix anything. (So in your 4-element model, it merely fixes that`R00`

is the element 'opposite'`R11`

-- either could be`X, Y`

, the choice is arbitrary.)

Quote from AntC on May 21, 2021, 4:54 amQuote from AntC on May 21, 2021, 12:44 amQuote from Vadim on May 20, 2021, 3:08 pmQuote from AntC on May 20, 2021, 8:00 am

`R11`

; the 4 elements`DEE, DUM, Dumpty, R11`

. The axioms and operators all work if we take`R11`

as a false`DUM`

, and leave the true`DUM`

as just some other element.

Is your version of

`<REMOVE>`

total? Also, by`project`

do you mean classic project, or inner union?

`r1 project r2`

=df`r1 InnerUnion emptify(r2)`

(many possible definitions for`emptify( )`

, which ought to be equivalent but aren't provably so.)`r1 Remove r2 = r1 project s ≡ emptify(r1 InnerUnion s) NatJoin emptify(r1 InnerUnion r2) = emptify(r1) & emptify((s InnerUnion r1) InnerUnion r2) = emptify(DEE).`

That is,`Remove`

is equivalent to`project`

on any`s`

such that`s`

has at least the attributes of`r1`

not in`r2`

.So yes I'm aiming to make

`project, Remove`

total (defined for all possible operands). I've added several further axioms for`Remove`

which ought to be implied by that (and aren't countered by Mace4), but aren't provable, it seems.Why is there that 'at least the attributes' business for

`s`

? Because I want an equivalence in the definition, to strengthen inference. See below about headings for the attributes to project/remove.`<REMOVE>`

called`<INVERSE>`

. The axioms for`<INVERSE>`

are the dual versions of the axioms for the`<NOT>`

. I agree that perhaps a binary incarnation of the`<INVERSE>`

operation, which would be domain and attribute set independent, might have its merits, but it would certainly make the axiom system more complex.I'm pretty sure using

`<NOT>, <INVERSE>`

run into the same problems of non-provability. I think the difficulty is this:

`NatJoin, InnerUnion`

are well-defined no matter what the headings of their operands. Indeed we deliberately exploit unequal headings for`NatJoin`

: if they're the same, thats`INTERSECT`

; if they don't overlap, that's Cartesian product; if one is a subset, that's`WHERE`

; if there's a partial overlap, that's`EXTEND`

. (To be more precise, the axiom system takes`NatJoin`

to be well-defined; then it follows from the absorption laws that`InnerUnion`

is well-defined. For the other operators, we don't have definitions as strong as the absorption laws.- We want
`Matching, NotMatching, project, Remove`

to be well-defined no matter what the headings of operands. And for`Matching, NotMatching`

that's not too bad, because the heading of the result is to be the heading of the left operand. But the heading of the r.h. operand to`project, Remove`

could include any rubbishy attributes that don't appear in the l.h. operand, they're just ignored/they don't have any influence on the result.- For
`Matching, NotMatching, project, Remove`

the bodies of the r.h. operand could include any rubbishy tuples that don't appear in the l.h. operand, again they're just ignored.- So you want
`r1 Remove r2`

=`r1 project (<INVERSE> r2)`

=`r1 InnerUnion emptify?(<INVERSE> r2)`

. Again that must be well defined if`r2`

has attributes outside`r1`

, and/or`<INVERSE> r2`

has attributes outside`r1`

. For`emptify?( )`

you still need to fix something -- perhaps`emptify?(r) = r NatJoin DUM; DUM = <NOT> DEE`

?- You can define
`<INVERSE> (<INVERSE> r) = r; <NOT> (<NOT> r) = r`

. I think that won't fix either operation to what you want. For example, those are 'solved' if`<INVERSE>, <NOT>`

are merely identity. I've added stupid/ugly axioms like`emptify(DEE) ≠ DEE`

;`DUM`

must be adjacent to`DEE`

. That's not enough to fix anything. (So in your 4-element model, it merely fixes that`R00`

is the element 'opposite'`R11`

-- either could be`X, Y`

, the choice is arbitrary.)Ah, that was easy to prove. Or are there some extra axioms I need? My definition above for

`<INVERSE>`

is wrong, a better guess below.

`<NOT>(<NOT> r1)) = r1.`

`r1 ≠ <NOT> r1.`

- Does not fix
`<NOT>`

. I can see this is pointless anyway, because there's no mention of`NatJoin, InnerUnion`

that are really what defines the lattice. Try that ...`emptify(r1) = r1 NatJoin (<NOT> r1).`

`emptify(DEE) = <NOT>(DEE).`

i.e. two definitions for`DUM`

not proven equal, neither is there a counter-model; so this has rapidly reached the position I'm in. (For full disclosure, Prover9 gives a strange message: 'not all the required proofs were found' -- even though I'm asking for only one proof. I don't think it's this problem. And that's weird because expanding the emptify ⇒`DEE NatJoin (<NOT> DEE)`

and`DEE NatJoin r = r`

, then lhs reduces to same as rhs.Well perhaps it'll all fix itself if I go on to

`<INVERSE>`

. My guess`<INVERSE> (<INVERSE> r) = r`

must be wrong, because the heading of`<INVERSE>`

's result must be the absolute complement of the heading of`r`

; which throws away the content of`r`

; so double-inverting can't restore it. I'll better-guess that`<INVERSE>`

returns the maximum content for that complemented heading. That'll give an opportunity to introduce the lattice operators into the equations.

`<INVERSE>(<INVERSE)(r1)) = r1 InnerUnion <NOT> r1.`

`<INVERSE> r1 ≠ r1.`

`<INVERSE>(<NOT> r1) = <INVERSE> r1.`

`<INVERSE> Dumpty = DEE.`

(`Dumpty`

=df the identity for`InnerUnion`

aka lattice bottom aka Tropashko's`R10`

.)- Those definitions don't fix
`<INVERSE>`

unique.- I don't see a definition for
`DUM`

that would use`<INVERSE>`

without also using`<NOT>`

to emptify.Perhaps it'll magically come together if we tie the loose ends with

`NotMatching`

?

`r1 NotMatching r2 = (r1 NatJoin <NOT> r2) InnerUnion (r1 NatJoin <NOT> DEE).`

-- writing out emptify in full -- no, not unique`(r1 NatJoin r2) InnerUnion (r1 NotMatching r2) = r1.`

`(r1 NatJoin r2) NatJoin (r1 NotMatching r2) = (r1 NatJoin r2) ^ <NOT> DEE.`

Adding both those doesn't make`NotMatching`

unique.So this approach ('total unary'/absolute complements) is just as ineffable as my avoiding domain-dependent operators.

Quote from AntC on May 21, 2021, 12:44 amQuote from Vadim on May 20, 2021, 3:08 pmQuote from AntC on May 20, 2021, 8:00 am

`R11`

; the 4 elements`DEE, DUM, Dumpty, R11`

. The axioms and operators all work if we take`R11`

as a false`DUM`

, and leave the true`DUM`

as just some other element.

Is your version of

`<REMOVE>`

total? Also, by`project`

do you mean classic project, or inner union?

`r1 project r2`

=df`r1 InnerUnion emptify(r2)`

(many possible definitions for`emptify( )`

, which ought to be equivalent but aren't provably so.)`Remove`

is equivalent to`project`

on any`s`

such that`s`

has at least the attributes of`r1`

not in`r2`

.`project, Remove`

total (defined for all possible operands). I've added several further axioms for`Remove`

which ought to be implied by that (and aren't countered by Mace4), but aren't provable, it seems.`s`

? Because I want an equivalence in the definition, to strengthen inference. See below about headings for the attributes to project/remove.`<REMOVE>`

called`<INVERSE>`

. The axioms for`<INVERSE>`

are the dual versions of the axioms for the`<NOT>`

. I agree that perhaps a binary incarnation of the`<INVERSE>`

operation, which would be domain and attribute set independent, might have its merits, but it would certainly make the axiom system more complex.`<NOT>, <INVERSE>`

run into the same problems of non-provability. I think the difficulty is this:

`NatJoin, InnerUnion`

are well-defined no matter what the headings of their operands. Indeed we deliberately exploit unequal headings for`NatJoin`

: if they're the same, thats`INTERSECT`

; if they don't overlap, that's Cartesian product; if one is a subset, that's`WHERE`

; if there's a partial overlap, that's`EXTEND`

. (To be more precise, the axiom system takes`NatJoin`

to be well-defined; then it follows from the absorption laws that`InnerUnion`

is well-defined. For the other operators, we don't have definitions as strong as the absorption laws.- We want
`Matching, NotMatching, project, Remove`

to be well-defined no matter what the headings of operands. And for`Matching, NotMatching`

that's not too bad, because the heading of the result is to be the heading of the left operand. But the heading of the r.h. operand to`project, Remove`

could include any rubbishy attributes that don't appear in the l.h. operand, they're just ignored/they don't have any influence on the result.- For
`Matching, NotMatching, project, Remove`

the bodies of the r.h. operand could include any rubbishy tuples that don't appear in the l.h. operand, again they're just ignored.- So you want
`r1 Remove r2`

=`r1 project (<INVERSE> r2)`

=`r1 InnerUnion emptify?(<INVERSE> r2)`

. Again that must be well defined if`r2`

has attributes outside`r1`

, and/or`<INVERSE> r2`

has attributes outside`r1`

. For`emptify?( )`

you still need to fix something -- perhaps`emptify?(r) = r NatJoin DUM; DUM = <NOT> DEE`

?- You can define
`<INVERSE> (<INVERSE> r) = r; <NOT> (<NOT> r) = r`

. I think that won't fix either operation to what you want. For example, those are 'solved' if`<INVERSE>, <NOT>`

are merely identity. I've added stupid/ugly axioms like`emptify(DEE) ≠ DEE`

;`DUM`

must be adjacent to`DEE`

. That's not enough to fix anything. (So in your 4-element model, it merely fixes that`R00`

is the element 'opposite'`R11`

-- either could be`X, Y`

, the choice is arbitrary.)

Ah, that was easy to prove. Or are there some extra axioms I need? My definition above for `<INVERSE>`

is wrong, a better guess below.

`<NOT>(<NOT> r1)) = r1.`

`r1 ≠ <NOT> r1.`

- Does not fix
`<NOT>`

. I can see this is pointless anyway, because there's no mention of`NatJoin, InnerUnion`

that are really what defines the lattice. Try that ... `emptify(r1) = r1 NatJoin (<NOT> r1).`

`emptify(DEE) = <NOT>(DEE).`

i.e. two definitions for`DUM`

not proven equal, neither is there a counter-model; so this has rapidly reached the position I'm in. (For full disclosure, Prover9 gives a strange message: 'not all the required proofs were found' -- even though I'm asking for only one proof. I don't think it's this problem. And that's weird because expanding the emptify ⇒`DEE NatJoin (<NOT> DEE)`

and`DEE NatJoin r = r`

, then lhs reduces to same as rhs.

Well perhaps it'll all fix itself if I go on to `<INVERSE>`

. My guess `<INVERSE> (<INVERSE> r) = r`

must be wrong, because the heading of `<INVERSE>`

's result must be the absolute complement of the heading of `r`

; which throws away the content of `r`

; so double-inverting can't restore it. I'll better-guess that `<INVERSE>`

returns the maximum content for that complemented heading. That'll give an opportunity to introduce the lattice operators into the equations.

`<INVERSE>(<INVERSE)(r1)) = r1 InnerUnion <NOT> r1.`

`<INVERSE> r1 ≠ r1.`

`<INVERSE>(<NOT> r1) = <INVERSE> r1.`

`<INVERSE> Dumpty = DEE.`

(`Dumpty`

=df the identity for`InnerUnion`

aka lattice bottom aka Tropashko's`R10`

.)- Those definitions don't fix
`<INVERSE>`

unique. - I don't see a definition for
`DUM`

that would use`<INVERSE>`

without also using`<NOT>`

to emptify.

Perhaps it'll magically come together if we tie the loose ends with `NotMatching`

?

`r1 NotMatching r2 = (r1 NatJoin <NOT> r2) InnerUnion (r1 NatJoin <NOT> DEE).`

-- writing out emptify in full -- no, not unique`(r1 NatJoin r2) InnerUnion (r1 NotMatching r2) = r1.`

`(r1 NatJoin r2) NatJoin (r1 NotMatching r2) = (r1 NatJoin r2) ^ <NOT> DEE.`

Adding both those doesn't make`NotMatching`

unique.

So this approach ('total unary'/absolute complements) is just as ineffable as my avoiding domain-dependent operators.

Quote from Vadim on May 21, 2021, 2:45 pmQuote from AntC on May 21, 2021, 12:44 amQuote from Vadim on May 20, 2021, 3:08 pmQuote from AntC on May 20, 2021, 8:00 am

`R11`

; the 4 elements`DEE, DUM, Dumpty, R11`

. The axioms and operators all work if we take`R11`

as a false`DUM`

, and leave the true`DUM`

as just some other element.Another example: take the universe inhabited by 4 unary relations [latex] X = \langle \{ p \}, \{ \langle 0 \rangle \}\rangle [/latex], [latex] Y = \langle \{ p \}, \{ \langle 1 \rangle \}\rangle [/latex], [latex] X \wedge Y [/latex], [latex] X \vee Y [/latex]. Some may argue that there are "genuine" DUM and DEE hidden somewhere in that universe, but I'd think their roles can perfectly be played by unary relations, so that those 4 relations is all that you will ever see.

There is a

`DEE`

-- that is, a relation whose heading is a subset of every other relation (not necessarily proper), and content a subset of every other relation projected on that heading. That is`X ^ Y`

.There isn't a

`DUM`

-- that is a relation whose headings is the subset of every other relation, and content a subset of every other relation projected on that heading. (Neither`X`

's nor`Y`

's body are a subset of the other.) But I suspect my definitions would work 'fine' (as well/badly as I'm currently experiencing) by interpreting`DUM = X`

. But equally well/badly by interpreting`DUM = Y`

. The choice is arbitrary -- which is the problem.I don't see any arbitrarines. We have

[latex] X = \langle \{ p \}, \{ \langle 0 \rangle \}\rangle [/latex],

[latex] Y = \langle \{ p \}, \{ \langle 1 \rangle \}\rangle [/latex],

[latex] X \wedge Y = R_{10} [/latex] (lattice bottom),

[latex] X \vee Y = R_{01} [/latex] (lattice top).

Then, we have the operation of tuple set complement. I'd prefer to use the quote symbol notation as a postfix operation, rather than TTM prefix

`<NOT>`

, because the later can be easily confused with boolean algebra negation. (In the relational lattice the analog of boolean negation is the composition of the attribute set complement (AKA inversion) and tuple set complement). The calculation of the tuple set complement of the each unverse inhabitant is straightforward:[latex] X ' = \langle \{ p \}, \{ \langle 0 \rangle \}\rangle ' = \langle \{ p \}, \{ \langle 1 \rangle \}\rangle = Y [/latex]

[latex] Y ' = X [/latex]

[latex] R_{01} ' = R_{10} [/latex]

[latex] R_{10} ' = R_{01} [/latex]

Then, by definition

[latex] R_{00} = R_{10}' [/latex]

This fixes [latex] R_{00} [/latex] uniquely in our universe as [latex] \langle \{ p \}, \emptyset \rangle [/latex]

`<INVERSE> (<INVERSE> r) = r; <NOT> (<NOT> r) = r`

. I think that won't fix either operation to what you want. For example, those are 'solved' if`<INVERSE>, <NOT>`

are merely identity. I've added stupid/ugly axioms like`emptify(DEE) ≠ DEE`

;`DUM`

must be adjacent to`DEE`

. That's not enough to fix anything. (So in your 4-element model, it merely fixes that`R00`

is the element 'opposite'`R11`

-- either could be`X, Y`

, the choice is arbitrary.)Unlike tuple set complement honoring the law of double negation

`x'' = x`

the law for repetitive attribute inversion is more subtle:

`x``` = x``

This makes attribute inversion less intutive compared to tuple set complement.

P.S. I see you made correction post, but the correspondence could have been clearer if you had edited the predecessor post. You can always temporarily delete/ mark the content of your post while in the process of editing so that people would not reply to it.

Quote from AntC on May 21, 2021, 12:44 amQuote from Vadim on May 20, 2021, 3:08 pmQuote from AntC on May 20, 2021, 8:00 am

`R11`

; the 4 elements`DEE, DUM, Dumpty, R11`

. The axioms and operators all work if we take`R11`

as a false`DUM`

, and leave the true`DUM`

as just some other element.Another example: take the universe inhabited by 4 unary relations X = \langle \{ p \}, \{ \langle 0 \rangle \}\rangle , Y = \langle \{ p \}, \{ \langle 1 \rangle \}\rangle , X \wedge Y , X \vee Y . Some may argue that there are "genuine" DUM and DEE hidden somewhere in that universe, but I'd think their roles can perfectly be played by unary relations, so that those 4 relations is all that you will ever see.

There is a

`DEE`

-- that is, a relation whose heading is a subset of every other relation (not necessarily proper), and content a subset of every other relation projected on that heading. That is`X ^ Y`

.There isn't a

`DUM`

-- that is a relation whose headings is the subset of every other relation, and content a subset of every other relation projected on that heading. (Neither`X`

's nor`Y`

's body are a subset of the other.) But I suspect my definitions would work 'fine' (as well/badly as I'm currently experiencing) by interpreting`DUM = X`

. But equally well/badly by interpreting`DUM = Y`

. The choice is arbitrary -- which is the problem.

I don't see any arbitrarines. We have

X = \langle \{ p \}, \{ \langle 0 \rangle \}\rangle ,

Y = \langle \{ p \}, \{ \langle 1 \rangle \}\rangle ,

X \wedge Y = R_{10} (lattice bottom),

X \vee Y = R_{01} (lattice top).

Then, we have the operation of tuple set complement. I'd prefer to use the quote symbol notation as a postfix operation, rather than TTM prefix `<NOT>`

, because the later can be easily confused with boolean algebra negation. (In the relational lattice the analog of boolean negation is the composition of the attribute set complement (AKA inversion) and tuple set complement). The calculation of the tuple set complement of the each unverse inhabitant is straightforward:

X ' = \langle \{ p \}, \{ \langle 0 \rangle \}\rangle ' = \langle \{ p \}, \{ \langle 1 \rangle \}\rangle = Y

Y ' = X

R_{01} ' = R_{10}

R_{10} ' = R_{01}

Then, by definition

R_{00} = R_{10}'

This fixes R_{00} uniquely in our universe as \langle \{ p \}, \emptyset \rangle

`<INVERSE> (<INVERSE> r) = r; <NOT> (<NOT> r) = r`

. I think that won't fix either operation to what you want. For example, those are 'solved' if`<INVERSE>, <NOT>`

are merely identity. I've added stupid/ugly axioms like`emptify(DEE) ≠ DEE`

;`DUM`

must be adjacent to`DEE`

. That's not enough to fix anything. (So in your 4-element model, it merely fixes that`R00`

is the element 'opposite'`R11`

-- either could be`X, Y`

, the choice is arbitrary.)

Unlike tuple set complement honoring the law of double negation

`x'' = x`

the law for repetitive attribute inversion is more subtle:

`x``` = x``

This makes attribute inversion less intutive compared to tuple set complement.

P.S. I see you made correction post, but the correspondence could have been clearer if you had edited the predecessor post. You can always temporarily delete/ mark the content of your post while in the process of editing so that people would not reply to it.

Quote from Vadim on May 21, 2021, 3:36 pmQuote from AntC on May 21, 2021, 4:54 am

- I don't see a definition for
`DUM`

that would use`<INVERSE>`

without also using`<NOT>`

to emptify.I have a system with 4 operation signature and 8 additional axioms:

% Language Options op(300, postfix, "`" ). formulas(assumptions). x ^ y = y ^ x. (x ^ y) ^ z = x ^ (y ^ z). x ^ (x v y) = x. x v y = y v x. (x v y) v z = x v (y v z). x v (x ^ y) = x. x = (x ^ y') v (x ^ y`). x ^ (y' ^ z')' = ((x ^ y)' ^ (x ^ z)')'. (x' ^ (y ^ z)')' = (x' ^ y')' ^ (x' ^ z')'. (y` ^ x') v (y' ^ x `) = (y' v x') ^ (y` v x `). R00 = ((x' ^ x)` ^ x)`. x' ^ x = x ^ R00. x' v x = x v R11. R11 = (x' v x`)`. x` ^ x = R11 ^ x. x` v x = R00 v x. end_of_list. formulas(goals). %R00 = ((x` v x)' v x)'. %R00 = (x' v x`)``'. %R11 = ((x` ^ x)' ^ x)'. end_of_list.Comments:

Axiom at line 15 is the generalization of FDA:

`x = (x ^ R00) v (x ^ R11)`

Axiom at line 16 is distributivity of the

`<OR>`

over`<AND>`

from TTM Appendix AAxiom at line 17 is the dual

Axiom at line 18 has been discovered by expression search in QBQL

Theorems like double tuple set complement, or triple attribute inversion are easily provable. The axioms from the Litak et.al. system are less so (but not refuted by Mace4 either).

Quote from AntC on May 21, 2021, 4:54 am

- I don't see a definition for
`DUM`

that would use`<INVERSE>`

without also using`<NOT>`

to emptify.

I have a system with 4 operation signature and 8 additional axioms:

% Language Options op(300, postfix, "`" ). formulas(assumptions). x ^ y = y ^ x. (x ^ y) ^ z = x ^ (y ^ z). x ^ (x v y) = x. x v y = y v x. (x v y) v z = x v (y v z). x v (x ^ y) = x. x = (x ^ y') v (x ^ y`). x ^ (y' ^ z')' = ((x ^ y)' ^ (x ^ z)')'. (x' ^ (y ^ z)')' = (x' ^ y')' ^ (x' ^ z')'. (y` ^ x') v (y' ^ x `) = (y' v x') ^ (y` v x `). R00 = ((x' ^ x)` ^ x)`. x' ^ x = x ^ R00. x' v x = x v R11. R11 = (x' v x`)`. x` ^ x = R11 ^ x. x` v x = R00 v x. end_of_list. formulas(goals). %R00 = ((x` v x)' v x)'. %R00 = (x' v x`)``'. %R11 = ((x` ^ x)' ^ x)'. end_of_list.

Comments:

Axiom at line 15 is the generalization of FDA: `x = (x ^ R00) v (x ^ R11)`

Axiom at line 16 is distributivity of the `<OR>`

over `<AND>`

from TTM Appendix A

Axiom at line 17 is the dual

Axiom at line 18 has been discovered by expression search in QBQL

Theorems like double tuple set complement, or triple attribute inversion are easily provable. The axioms from the Litak et.al. system are less so (but not refuted by Mace4 either).

Quote from tobega on May 21, 2021, 8:06 pmI'll take the liberty to waffle on with some further thoughts from my limited understanding.

I'm still thinking of some kind of analogy to field extensions in Galois theory (which I don't really pretend to understand despite passing a class in it long ago), so I'll play with that:

We start with the lattice with no attributes, say D, with elements DUM and DEE. Then we extend with an attribute, say A1, to form the lattice D(A

_{1}) with elements DUM(A_{1}) which is heading A_{1}no tuples, and DEE(A_{1}) which has all possible values of A_{1}. We can extend more to D(A_{1}..A_{n}), giving DUM(A_{1}..A_{n}) and DEE(A_{1}..A_{n}). An extension can be characterized as DEE(A_{1}..A_{n}) join DEE(A_{n+1})For any relation in D(A

_{1}..A_{n}), any DEE(B_{1}..B_{k}) where B_{1}..B_{k}is a subset of A_{1}..A_{n}works as identity for join, and any DUM(C_{1}..C_{m}) where C_{1}..C_{m}is a superset of A_{1}..A_{n}works as an identity for inner union.Don't know if that gets us anywhere, but it gives the thought that DUM and DEE could be functions (emptify and fullify). It seems be enough to have just DUM and the biggest possible DEE, call it F (I was going to call it DOLLY but that's probably not PC), the others are easily derived from them and the relation we are looking at.

I'll take the liberty to waffle on with some further thoughts from my limited understanding.

I'm still thinking of some kind of analogy to field extensions in Galois theory (which I don't really pretend to understand despite passing a class in it long ago), so I'll play with that:

We start with the lattice with no attributes, say D, with elements DUM and DEE. Then we extend with an attribute, say A1, to form the lattice D(A_{1}) with elements DUM(A_{1}) which is heading A_{1} no tuples, and DEE(A_{1}) which has all possible values of A_{1}. We can extend more to D(A_{1}..A_{n}), giving DUM(A_{1}..A_{n}) and DEE(A_{1}..A_{n}). An extension can be characterized as DEE(A_{1}..A_{n}) join DEE(A_{n+1})

For any relation in D(A_{1}..A_{n}), any DEE(B_{1}..B_{k}) where B_{1}..B_{k} is a subset of A_{1}..A_{n} works as identity for join, and any DUM(C_{1}..C_{m}) where C_{1}..C_{m} is a superset of A_{1}..A_{n} works as an identity for inner union.

Don't know if that gets us anywhere, but it gives the thought that DUM and DEE could be functions (emptify and fullify). It seems be enough to have just DUM and the biggest possible DEE, call it F (I was going to call it DOLLY but that's probably not PC), the others are easily derived from them and the relation we are looking at.

Quote from AntC on May 21, 2021, 10:34 pmQuote from Vadim on May 21, 2021, 3:36 pmQuote from AntC on May 21, 2021, 4:54 am

- I don't see a definition for
`DUM`

that would use`<INVERSE>`

without also using`<NOT>`

to emptify.I have a system with 4 operation signature and 8 additional axioms:

Are these axioms sufficient to fix your operators uniquely (in terms of lattice meet, join)? Do you have a proof of that uniqueness?Anybody can go around inventing operators and giving some equations mentioning them. And inventing constants like`R00, R11`

. Without proofs of uniqueness, we don't have an algebra.

Quote from Vadim on May 21, 2021, 3:36 pmQuote from AntC on May 21, 2021, 4:54 am

- I don't see a definition for
`DUM`

that would use`<INVERSE>`

without also using`<NOT>`

to emptify.I have a system with 4 operation signature and 8 additional axioms:

`R00, R11`

. Without proofs of uniqueness, we don't have an algebra.

Quote from AntC on May 21, 2021, 10:57 pmQuote from tobega on May 21, 2021, 8:06 pm

We start with the lattice with no attributes, say D, with elements DUM and DEE.

To count as a lattice, we need a (partial) ordering. Or (equivalently as it turns out) a pair of operators that operate on any two elements to produce a third (not necessarily distinct), and that are commutative, associative, idempotent, and mutually dual such that they absorb each other. Read the wiki page on Lattice (ordering), it's simple algebra, unlike Galois theory.

You seem to be building a set of elements. Not every set of elements is a lattice. You seem to have an ordering only amongst relations of the same heading. That's not a lattice: you need an (partial) ordering amongst relations of different headings.

Then we extend with an attribute, say A1, to form the lattice D(A

_{1}) with elements DUM(A_{1}) which is heading A_{1}no tuples, and DEE(A_{1}) which has all possible values of A_{1}. We can extend more to D(A_{1}..A_{n}), giving DUM(A_{1}..A_{n}) and DEE(A_{1}..A_{n}). An extension can be characterized as DEE(A_{1}..A_{n}) join DEE(A_{n+1})How do we generate non-empty relations with less than all possible tuples for that heading? How to prove that subtracting one tuple from DEE(A

_{1}) then subtracting another yields the same relation as subtracting in the reverse ordering? (How to prove that adding tuples to DUM(A1) likewise produces the same yield? How to prove that if you add enough tuples to DUM(A_{1}) you'll arrive at DEE(A_{1})? And inversely subtracting? ) That'll be true if DEE(A_{1}) is a set, but you haven't given any axioms saying it's a set. Neither have you given axioms saying how the set contents relate to the ordering.For any relation in D(A

_{1}..A_{n}), any DEE(B_{1}..B_{k}) where B_{1}..B_{k}is a subset of A_{1}..A_{n}works as identity for join, and any DUM(C_{1}..C_{m}) where C_{1}..C_{m}is a superset of A_{1}..A_{n}works as an identity for inner union.I don't understand "works as an identity for ...". The consequence of the lattice structure, and characteristics of the lattice operators, is there is exactly one identity element. It must work as identity for

`NatJoin`

to any element of any heading.Don't know if that gets us anywhere, but it gives the thought that DUM and DEE could be functions (emptify and fullify). It seems be enough to have just DUM and the biggest possible DEE, call it F (I was going to call it DOLLY but that's probably not PC), the others are easily derived from them and the relation we are looking at.

To repeat for the umpteenth time: there is no problem with

`DEE`

, it's easy to define, and define uniquely. The 'biggest possible' relation -- that is, with all possible attributes and all possible tuples for those attributes (let's call it`Fullest`

) is emphatically not`DEE`

-- because`DEE`

is greater than`Fullest`

in the lattice ordering, because`Fullest`

is not identity for`NatJoin`

for all possible relations/all headings.

Quote from tobega on May 21, 2021, 8:06 pm

We start with the lattice with no attributes, say D, with elements DUM and DEE.

To count as a lattice, we need a (partial) ordering. Or (equivalently as it turns out) a pair of operators that operate on any two elements to produce a third (not necessarily distinct), and that are commutative, associative, idempotent, and mutually dual such that they absorb each other. Read the wiki page on Lattice (ordering), it's simple algebra, unlike Galois theory.

You seem to be building a set of elements. Not every set of elements is a lattice. You seem to have an ordering only amongst relations of the same heading. That's not a lattice: you need an (partial) ordering amongst relations of different headings.

Then we extend with an attribute, say A1, to form the lattice D(A

_{1}) with elements DUM(A_{1}) which is heading A_{1}no tuples, and DEE(A_{1}) which has all possible values of A_{1}. We can extend more to D(A_{1}..A_{n}), giving DUM(A_{1}..A_{n}) and DEE(A_{1}..A_{n}). An extension can be characterized as DEE(A_{1}..A_{n}) join DEE(A_{n+1})

How do we generate non-empty relations with less than all possible tuples for that heading? How to prove that subtracting one tuple from DEE(A_{1}) then subtracting another yields the same relation as subtracting in the reverse ordering? (How to prove that adding tuples to DUM(A1) likewise produces the same yield? How to prove that if you add enough tuples to DUM(A_{1}) you'll arrive at DEE(A_{1})? And inversely subtracting? ) That'll be true if DEE(A_{1}) is a set, but you haven't given any axioms saying it's a set. Neither have you given axioms saying how the set contents relate to the ordering.

_{1}..A_{n}), any DEE(B_{1}..B_{k}) where B_{1}..B_{k}is a subset of A_{1}..A_{n}works as identity for join, and any DUM(C_{1}..C_{m}) where C_{1}..C_{m}is a superset of A_{1}..A_{n}works as an identity for inner union.

I don't understand "works as an identity for ...". The consequence of the lattice structure, and characteristics of the lattice operators, is there is exactly one identity element. It must work as identity for `NatJoin`

to any element of any heading.

To repeat for the umpteenth time: there is no problem with `DEE`

, it's easy to define, and define uniquely. The 'biggest possible' relation -- that is, with all possible attributes and all possible tuples for those attributes (let's call it `Fullest`

) is emphatically not `DEE`

-- because `DEE`

is greater than `Fullest`

in the lattice ordering, because `Fullest`

is not identity for `NatJoin`

for all possible relations/all headings.