# Implicit assumptions in a toy example of view updates

Quote from Vadim on October 28, 2019, 6:43 pmConsider the following relation

`X1`

:

p q 1 a 2 b Our goal is to "solve" view updates problem for the projection of this view onto the column q.

Therefore, given derived relation

`Y1:`

q a b and its later snapshot

`Y2`

:

q a c we are after a relational algebra expression for

`X2`

-- base relation`X`

state at the later moment.Let's write down all the formal assumptions made in this example. I will leverage algebraic perspective and use Prover9/Mace4 as a tool. Hence, we have to distinguish constants from variables and, as you might have already noticed, I have used identifiers with capital letter as relation names for

`X1, X2, Y1, Y2`

.The first assertion is just a definition of convenient auxiliary relation

`Q`

-- the header of`Y1`

`Q = Y1 ^ R00.`

`Y2`

has the same header, of course:

`Q = Y2 ^ R00.`

Next, the derived view

`Y`

is projection of`X`

onto`Q`

, which is expressed formally as:

`X1 v Q = Y1.`

`X2 v Q = Y2.`

What happened after we update

`Y1`

into`Y2`

with the value at the column`q`

of relation`X`

? Those values which didn't change in the relation`Y`

don't change in the relation`X`

:

`((Y1 ^ Y2') ^ X1) v Q = ((Y2 ^ Y1') ^ X2) v Q.`

There the expression

`Y1 ^ Y2'`

is known as binary`NOT_MATCHING`

operation`Y1-Y2`

. Once again, I use unary postfix quotation mark for what is also known as the`<NOT>`

operation from TTM Algebra A, because the axioms for that unary operation are simpler than the axioms for binary`NOT_MATCHING`

.Lastly, we specify what happens in the column

`p`

, that the values didn't change:

`X1 v Q` = X2 v Q`.`

There, the back quote is unary attribute inversion.

Our goal is to prove that the increment of the relation

`X,`

that is`X2 ^ X1'`

, can be expressed via the increment of the relation`Y`

:

`X2 ^ X1' = (Y1 ^ Y2') ^ X1.`

Surprisingly, the problem is still under specified as evidenced by Mace4 counterexample of cardinality 10. What other possible condition is missing?

Consider the following relation `X1`

:

p | q |

1 | a |

2 | b |

Our goal is to "solve" view updates problem for the projection of this view onto the column q.

Therefore, given derived relation `Y1:`

q |

a |

b |

and its later snapshot `Y2`

:

q |

a |

c |

we are after a relational algebra expression for `X2`

-- base relation `X`

state at the later moment.

Let's write down all the formal assumptions made in this example. I will leverage algebraic perspective and use Prover9/Mace4 as a tool. Hence, we have to distinguish constants from variables and, as you might have already noticed, I have used identifiers with capital letter as relation names for `X1, X2, Y1, Y2`

.

The first assertion is just a definition of convenient auxiliary relation `Q`

-- the header of `Y1`

`Q = Y1 ^ R00.`

`Y2`

has the same header, of course:

`Q = Y2 ^ R00.`

Next, the derived view `Y`

is projection of `X`

onto `Q`

, which is expressed formally as:

`X1 v Q = Y1.`

`X2 v Q = Y2.`

What happened after we update `Y1`

into `Y2`

with the value at the column `q`

of relation `X`

? Those values which didn't change in the relation `Y`

don't change in the relation `X`

:

` ((Y1 ^ Y2') ^ X1) v Q = ((Y2 ^ Y1') ^ X2) v Q. `

There the expression `Y1 ^ Y2'`

is known as binary `NOT_MATCHING`

operation `Y1-Y2`

. Once again, I use unary postfix quotation mark for what is also known as the `<NOT>`

operation from TTM Algebra A, because the axioms for that unary operation are simpler than the axioms for binary `NOT_MATCHING`

.

Lastly, we specify what happens in the column `p`

, that the values didn't change:

`X1 v Q` = X2 v Q`.`

There, the back quote is unary attribute inversion.

Our goal is to prove that the increment of the relation `X,`

that is `X2 ^ X1'`

, can be expressed via the increment of the relation `Y`

:

`X2 ^ X1' = (Y1 ^ Y2') ^ X1.`

Surprisingly, the problem is still under specified as evidenced by Mace4 counterexample of cardinality 10. What other possible condition is missing?

Quote from AntC on October 29, 2019, 12:01 amQuote from Vadim on October 28, 2019, 6:43 pm...

Surprisingly, the problem is still under specified as evidenced by Mace4 counterexample of cardinality 10. What other possible condition is missing?

Vadim, you're attempting (rather clumsily) the Constant Complement approach. A couple of pertinent quotes from Bancilhon & Spyratos:

"We show that a view can have more than one complement and that the choice of a complement determines an update policy. "

"... computational algorithms (if they exist) implementing steps (1) and (2) must be sought in specific problems:

for example, schemata defined by functional dependencies and views derived by projections. "A "possible condition" is that you've under-specified what must be constant (persistent) through an update via that view. A "possible condition" is you've not recognised any key/Functional Dependency in either the base relvar or the view.

In general, B&S are quite pessimistic about 'solutions' to the update-via-views problem. Furthermore, as I pointed out on the older forum, their approach doesn't even work for the update-base 'problem'.

We've spilled more than enough ink here on update-via-view. I. can't. even.

Quote from Vadim on October 28, 2019, 6:43 pm...

Vadim, you're attempting (rather clumsily) the Constant Complement approach. A couple of pertinent quotes from Bancilhon & Spyratos:

"We show that a view can have more than one complement and that the choice of a complement determines an update policy. "

"... computational algorithms (if they exist) implementing steps (1) and (2) must be sought in specific problems:

for example, schemata defined by functional dependencies and views derived by projections. "

A "possible condition" is that you've under-specified what must be constant (persistent) through an update via that view. A "possible condition" is you've not recognised any key/Functional Dependency in either the base relvar or the view.

In general, B&S are quite pessimistic about 'solutions' to the update-via-views problem. Furthermore, as I pointed out on the older forum, their approach doesn't even work for the update-base 'problem'.

We've spilled more than enough ink here on update-via-view. I. can't. even.

Quote from AntC on October 29, 2019, 5:33 amQuote from AntC on October 29, 2019, 12:01 amQuote from Vadim on October 28, 2019, 6:43 pm...

Vadim, you're attempting (rather clumsily) the Constant Complement approach.

To explain a bit about constant complements:

- Start with the 'leftovers' of the base relvar(s) that are excluded from the view. (That'll be attribute
`p`

in your`X1`

.)- Can you reconstitute
`X1`

from the view content with the 'leftovers'? You can use any known constraints to help.

- In your example, you can't: the only option would be Cartesian product
`X1{ p } x Y1;`

, which'll give 4 tuples with your example, not the 2 original.- If not, augment the 'leftovers' with more attributes and/or tuples from the base relvar(s) until you can reconstitute.

(Then being able to reconstitute should be an axiom in your approach.)- In general, there's many ways to augment: we want the augmented complement to be constant in face of updates through the view.

(You do have an axiom for that.)- In your case, the only way to augment is by making the 'complement' the whole original base table.
- That's not constant in face of updates through the view.
So what you're trying can't be done. (And I'm not surprised; and I don't understand why you say "surprisingly".)

Since UPDATE-through-projection and DELETE-through-projection are forms of update-through-view that are supported in many versions of SQL, that's a poor show for the axiomatic method.

Quote from AntC on October 29, 2019, 12:01 amQuote from Vadim on October 28, 2019, 6:43 pm...

Vadim, you're attempting (rather clumsily) the Constant Complement approach.

To explain a bit about constant complements:

- Start with the 'leftovers' of the base relvar(s) that are excluded from the view. (That'll be attribute
`p`

in your`X1`

.) - Can you reconstitute
`X1`

from the view content with the 'leftovers'? You can use any known constraints to help.- In your example, you can't: the only option would be Cartesian product
`X1{ p } x Y1;`

, which'll give 4 tuples with your example, not the 2 original. - If not, augment the 'leftovers' with more attributes and/or tuples from the base relvar(s) until you can reconstitute.

(Then being able to reconstitute should be an axiom in your approach.) - In general, there's many ways to augment: we want the augmented complement to be constant in face of updates through the view.

(You do have an axiom for that.) - In your case, the only way to augment is by making the 'complement' the whole original base table.
- That's not constant in face of updates through the view.

- In your example, you can't: the only option would be Cartesian product

So what you're trying can't be done. (And I'm not surprised; and I don't understand why you say "surprisingly".)

Since UPDATE-through-projection and DELETE-through-projection are forms of update-through-view that are supported in many versions of SQL, that's a poor show for the axiomatic method.

Quote from Vadim on October 29, 2019, 8:23 pmI agree, since SQL can handle UPDATE-through-projection, certainly, you will have no trouble writing down all the assumptions made in the OP example. To be more concrete, consider for example oracle RDBMS where any join-project view is updateable as soon as the view is

key-preserving.Unfortunately, in relational algebra perspective, we don't have axioms for functional dependency. In our earlier email exchange you attempted to introduce axioms for binary equivalence relation, but felt short of exhibiting the complete system. It looks like we have no option other than switching perspective to relational calculus. Here is the translated OP example:

%X1 v Q = Y1. exists p X1(p,q) <-> Y1(q). %X2 v Q = Y2. exists p X2(p,q) <-> Y2(q). %X1 v Q` = X2 v Q`. exists p X1(p,q) <-> X2(p,q). %((Y1 ^ Y2') ^ X1) v Q = ((Y2 ^ Y1') ^ X2) v Q. exists q (Y1(q) & -Y2(q)) & X1(p,q) <-> (Y2(q) & -Y1(q)) & X2(p,q). %X1(p,q1) & X1(p,q2) -> q1=q2. %X2(p,q1) & X2(p,q2) -> q1=q2. X1(p1,q) & X1(p2,q) -> p1=p2. X2(p1,q) & X2(p2,q) -> p1=p2.The last two lines express functional dependency q->p as required by the key-preserve condition; the prior commented out portion declared the opposite functional dependency.

Still, the system is under specified as witnessed by the following model:

`X1`

:

p q 1 0

`X2`

:

p q 0 0

`Y1:`

q 0

`Y2`

:

q 0 What formal condition of key-preserved view update rule am I missing?

~~BTW, the 10-element model I mentioned in the original post turned out to be quite helpful, because it doesn't represent any lattice of database relations. Which hints that my 2x2 axiom system is incomplete.~~

I agree, since SQL can handle UPDATE-through-projection, certainly, you will have no trouble writing down all the assumptions made in the OP example. To be more concrete, consider for example oracle RDBMS where any join-project view is updateable as soon as the view is *key-preserving*.

Unfortunately, in relational algebra perspective, we don't have axioms for functional dependency. In our earlier email exchange you attempted to introduce axioms for binary equivalence relation, but felt short of exhibiting the complete system. It looks like we have no option other than switching perspective to relational calculus. Here is the translated OP example:

%X1 v Q = Y1. exists p X1(p,q) <-> Y1(q). %X2 v Q = Y2. exists p X2(p,q) <-> Y2(q). %X1 v Q` = X2 v Q`. exists p X1(p,q) <-> X2(p,q). %((Y1 ^ Y2') ^ X1) v Q = ((Y2 ^ Y1') ^ X2) v Q. exists q (Y1(q) & -Y2(q)) & X1(p,q) <-> (Y2(q) & -Y1(q)) & X2(p,q). %X1(p,q1) & X1(p,q2) -> q1=q2. %X2(p,q1) & X2(p,q2) -> q1=q2. X1(p1,q) & X1(p2,q) -> p1=p2. X2(p1,q) & X2(p2,q) -> p1=p2.

The last two lines express functional dependency q->p as required by the key-preserve condition; the prior commented out portion declared the opposite functional dependency.

Still, the system is under specified as witnessed by the following model:

`X1`

:

p | q |

1 | 0 |

`X2`

:

p | q |

0 | 0 |

`Y1:`

q |

0 |

`Y2`

:

q |

0 |

What formal condition of key-preserved view update rule am I missing?

~~BTW, the 10-element model I mentioned in the original post turned out to be quite helpful, because it doesn't represent any lattice of database relations. Which hints that my 2x2 axiom system is incomplete.~~

Quote from AntC on October 29, 2019, 9:23 pmQuote from Vadim on October 29, 2019, 8:23 pmI agree, since SQL can handle UPDATE-through-projection, certainly, you will have no trouble writing down all the assumptions made in the OP example. To be more concrete, consider for example oracle RDBMS where any join-project view is updateable as soon as the view is

key-preserving.Consider how very different to TTM is SQL wrt update-through-view. SQL doesn't treat views as relvars/not as first-class (contra RM Pre 14). Neither does SQL treat update as a form of assignment (contra RM Pre 21). SQL is all very ad-hoc and unprincipled, but it works (up to a point, Lord Copper). SQL is also very different to the approach in Bancilhon & Spyratos, who assume you're replacing some view content with the update holus bolus/much more like RM Pre 21.

So SQL translates an update statement targetting a view into an update statement targetting the base table(s). In your example we might put it

`UPDATE (SELECT q FROM X1) SET q = 'c' WHERE q = 'b';`

// translated to

`UPDATE X1 SET q = 'c' WHERE q = 'b';`

`DELETE (SELECT q FROM X1) WHERE q = 'b';`

// likewise translated

`DELETE X1 WHERE q = 'b';`

INSERT-through-projection not possible, because you can't translate it into INSERT-to-base. (Well, unless you put Nulls in column

`p`

. We won't go there.)So SQL has a notion of tuples having identity, and that you're changing the content of a tuple(s) identified via the

`WHERE`

condition as a means to grab the identity. In Oracle, that identity can be made explicit: there's a rowid.Unfortunately, in relational algebra perspective, we don't have axioms for functional dependency. In our earlier email exchange you attempted to introduce axioms for binary equivalence relation, but felt short of exhibiting the complete system.

I did some further work after that thread fell quiet. I think I can express a FD, but it relies on fixing

`R00`

as`DUM`

. Without that, anything else is going to be unprovable. And that's where I'm still stuck (after much trying).It looks like we have no option other than switching perspective to relational calculus. Here is the translated OP example:

%X1 v Q = Y1. exists p X1(p,q) <-> Y1(q). %X2 v Q = Y2. exists p X2(p,q) <-> Y2(q). %X1 v Q` = X2 v Q`. exists p X1(p,q) <-> X2(p,q). %((Y1 ^ Y2') ^ X1) v Q = ((Y2 ^ Y1') ^ X2) v Q. exists q (Y1(q) & -Y2(q)) & X1(p,q) <-> (Y2(q) & -Y1(q)) & X2(p,q). %X1(p,q1) & X1(p,q2) -> q1=q2. %X2(p,q1) & X2(p,q2) -> q1=q2. X1(p1,q) & X1(p2,q) -> p1=p2. X2(p1,q) & X2(p2,q) -> p1=p2.The last two lines express functional dependency q->p as required by the key-preserve condition; the prior commented out portion declared the opposite functional dependency.

Still, the system is under specified ...

Vadim stop churning out code and think what you're trying to do: Do the tuples have identity/something that uniquely identifies them other than their content? In your example, you have four possibilities:

- The key is
`{p}`

, the attribute projected away from the view. Then changing the content of the view has no way to connect back to the key.- The key is
`{q}`

, the attribute projected-in to the view. Then the 'leftovers' (attribute`p`

) have no way to connect back to the key.- The key is both
`{p, q}`

, so the projection view potentially has different cardinality to base. Then no way to connect back the broken halves of the key.- There are two keys
`{{p}, {q}}`

, so either project identifies a tuple. But you're then updating`q`

so destroying the key/no way to connect them back.- So there's good sense in Oracle's rule that everything must be
key-preserving. (BTW it's not just that the view must preserve keys: the update can't change the key content either. One of Codd's 12 rules is to that effect.)What formal condition of key-preserved view update rule am I missing?

There's nothing you could add. Simply, you can't achieve update-through-view by this holus-bolus replacing content.

BTW, the 10-element model I mentioned in the original post turned out to be quite helpful, because it doesn't represent any lattice of database relations. Which hints that my 2x2 axiom system is incomplete.

Your axiom system used

`R00`

to obtain headings.`R00`

is under-specified. Everything using`R00`

is incomplete.

Quote from Vadim on October 29, 2019, 8:23 pmkey-preserving.

Consider how very different to TTM is SQL wrt update-through-view. SQL doesn't treat views as relvars/not as first-class (contra RM Pre 14). Neither does SQL treat update as a form of assignment (contra RM Pre 21). SQL is all very ad-hoc and unprincipled, but it works (up to a point, Lord Copper). SQL is also very different to the approach in Bancilhon & Spyratos, who assume you're replacing some view content with the update holus bolus/much more like RM Pre 21.

So SQL translates an update statement targetting a view into an update statement targetting the base table(s). In your example we might put it

`UPDATE (SELECT q FROM X1) SET q = 'c' WHERE q = 'b';`

// translated to

`UPDATE X1 SET q = 'c' WHERE q = 'b';`

`DELETE (SELECT q FROM X1) WHERE q = 'b';`

// likewise translated

`DELETE X1 WHERE q = 'b';`

INSERT-through-projection not possible, because you can't translate it into INSERT-to-base. (Well, unless you put Nulls in column `p`

. We won't go there.)

So SQL has a notion of tuples having identity, and that you're changing the content of a tuple(s) identified via the `WHERE`

condition as a means to grab the identity. In Oracle, that identity can be made explicit: there's a rowid.

Unfortunately, in relational algebra perspective, we don't have axioms for functional dependency. In our earlier email exchange you attempted to introduce axioms for binary equivalence relation, but felt short of exhibiting the complete system.

I did some further work after that thread fell quiet. I think I can express a FD, but it relies on fixing `R00`

as `DUM`

. Without that, anything else is going to be unprovable. And that's where I'm still stuck (after much trying).

It looks like we have no option other than switching perspective to relational calculus. Here is the translated OP example:

Still, the system is under specified ...

Vadim stop churning out code and think what you're trying to do: Do the tuples have identity/something that uniquely identifies them other than their content? In your example, you have four possibilities:

- The key is
`{p}`

, the attribute projected away from the view. Then changing the content of the view has no way to connect back to the key. - The key is
`{q}`

, the attribute projected-in to the view. Then the 'leftovers' (attribute`p`

) have no way to connect back to the key. - The key is both
`{p, q}`

, so the projection view potentially has different cardinality to base. Then no way to connect back the broken halves of the key. - There are two keys
`{{p}, {q}}`

, so either project identifies a tuple. But you're then updating`q`

so destroying the key/no way to connect them back. - So there's good sense in Oracle's rule that everything must be
*key-preserving*. (BTW it's not just that the view must preserve keys: the update can't change the key content either. One of Codd's 12 rules is to that effect.)

What formal condition of key-preserved view update rule am I missing?

There's nothing you could add. Simply, you can't achieve update-through-view by this holus-bolus replacing content.

Your axiom system used `R00`

to obtain headings. `R00`

is under-specified. Everything using `R00`

is incomplete.

Quote from p c on October 30, 2019, 7:44 amThe comments are not quite right. You can make a logically valid proof that applies whether or not keys are preserved. Propositional logic is enough to prove that.

It's known that if you have an operator such as rename then you can express an FD but it appears that complete and consistent systems don't have such an operator.

The comments are not quite right. You can make a logically valid proof that applies whether or not keys are preserved. Propositional logic is enough to prove that.

It's known that if you have an operator such as rename then you can express an FD but it appears that complete and consistent systems don't have such an operator.

Quote from p c on October 30, 2019, 10:17 amWhen a proof argument says nothing else about r{q} it can't conclude r{p,q}.

However it can assume that in a premise.

It can prove r{p,q} from r{q} when p is known, such as when Forall q((r(q) = 'c' ) -> ((r(p) = 2 )). Of course this is known by the dbms when it derives the projection r{q}.

That predicate describes a set, not a tuple. But it is obviously a singleton set, so several FD's could apply.

So long as an argument doesn't assume the truth of both of that predicate and of another predicate that is identical except that r{q} = 'b', it can be a logically valid argument.

Plus, if r obeys some FD before the argument is applied it will still obey after. Such a proof argument doesn't even need to explicitly assume an FD, it only needs to be written such that the desired FD is not contradicted.

When a proof argument says nothing else about r{q} it can't conclude r{p,q}.

However it can assume that in a premise.

It can prove r{p,q} from r{q} when p is known, such as when Forall q((r(q) = 'c' ) -> ((r(p) = 2 )). Of course this is known by the dbms when it derives the projection r{q}.

That predicate describes a set, not a tuple. But it is obviously a singleton set, so several FD's could apply.

So long as an argument doesn't assume the truth of both of that predicate and of another predicate that is identical except that r{q} = 'b', it can be a logically valid argument.

Plus, if r obeys some FD before the argument is applied it will still obey after. Such a proof argument doesn't even need to explicitly assume an FD, it only needs to be written such that the desired FD is not contradicted.

Quote from Vadim on October 30, 2019, 4:56 pmQuote from AntC on October 29, 2019, 9:23 pmI think I can express a FD, but it relies on fixing

`R00`

as`DUM`

. Without that, anything else is going to be unprovable. And that's where I'm still stuck (after much trying).This is recurring theme of yours, but again, I'm more confused about uniqueness now, than in the past (before you raised the issue). What is uniqueness of constants and operations in

Universal Algebra? I don't see it covered anywhere, except perhaps couple of exercises in undergraduate algebra textbooks asking to prove uniqueness of`0`

in a group or ring. Once again, there is nothing special about constants compared to operations, so why are the book authors compelled to prove uniqueness of`0`

? And if we start questioning uniqueness of other operations, then we get nowhere in any algebra.Look at the issue from the model theory perspective. As long as your axiom system outputs models which you can interpret as database relations, where exactly is the problem of the uniqueness of

`R00`

? How does the alleged nonuniqueness affect the theorems that you canformallydeduce in your system?When you are saying that an axiom system has to associate

`R00`

with`Dum`

unambiguously, you mean something else. There is a concept of representative relation algebras, that is when formal elements of algebra can be interpreted as binary relations and operations in both systems match. I think you are after analogous concept in the area of relational lattices. Given a model satisfying a formal system of relational lattice axioms, would we always be able to interpret the elements of the model as database relations? I didn't encounter such "abnormal" models in either LMH or 2x2 axiom system, but the question is open.

Your axiom system used

`R00`

to obtain headings.`R00`

is under-specified. Everything using`R00`

is incomplete.The axiom system is a system of requirements to which operations should comply. All operations are introduced at once, and there is no intrinsic order among them.

I made mistake claiming that the 10-element model is not representable by database of relations. Here is the counterexample translated into database terms:

`X1`

:

p q 1 a 2 b

`X2`

:

p q 1 a 1 b 2 a 2 b

`Y1`

:

q a b

`Y2`

:

q a b In both this counter example, and the one from predicate calculus perspective the view

`Y`

didn't change at all! So it is neither`insert`

, nor`update`

, nor`delete`

, and I agree with your comment that the additional information whether we are deleting, updating, or inserting tuples is important -- as I just found out the hard way.The 2x2 axiom system lives.

Quote from AntC on October 29, 2019, 9:23 pmI think I can express a FD, but it relies on fixing

`R00`

as`DUM`

. Without that, anything else is going to be unprovable. And that's where I'm still stuck (after much trying).

This is recurring theme of yours, but again, I'm more confused about uniqueness now, than in the past (before you raised the issue). What is uniqueness of constants and operations in *Universal Algebra*? I don't see it covered anywhere, except perhaps couple of exercises in undergraduate algebra textbooks asking to prove uniqueness of `0`

in a group or ring. Once again, there is nothing special about constants compared to operations, so why are the book authors compelled to prove uniqueness of `0`

? And if we start questioning uniqueness of other operations, then we get nowhere in any algebra.

Look at the issue from the model theory perspective. As long as your axiom system outputs models which you can interpret as database relations, where exactly is the problem of the uniqueness of `R00`

? How does the alleged nonuniqueness affect the theorems that you can *formally* deduce in your system?

When you are saying that an axiom system has to associate `R00`

with `Dum`

unambiguously, you mean something else. There is a concept of representative relation algebras, that is when formal elements of algebra can be interpreted as binary relations and operations in both systems match. I think you are after analogous concept in the area of relational lattices. Given a model satisfying a formal system of relational lattice axioms, would we always be able to interpret the elements of the model as database relations? I didn't encounter such "abnormal" models in either LMH or 2x2 axiom system, but the question is open.

`R00`

to obtain headings.`R00`

is under-specified. Everything using`R00`

is incomplete.

The axiom system is a system of requirements to which operations should comply. All operations are introduced at once, and there is no intrinsic order among them.

I made mistake claiming that the 10-element model is not representable by database of relations. Here is the counterexample translated into database terms:

`X1`

:

p | q |

1 | a |

2 | b |

`X2`

:

p | q |

1 | a |

1 | b |

2 | a |

2 | b |

`Y1`

:

q |

a |

b |

`Y2`

:

q |

a |

b |

In both this counter example, and the one from predicate calculus perspective the view `Y`

didn't change at all! So it is neither `insert`

, nor `update`

, nor `delete`

, and I agree with your comment that the additional information whether we are deleting, updating, or inserting tuples is important -- as I just found out the hard way.

The 2x2 axiom system lives.

Quote from AntC on November 5, 2019, 2:10 am(Apologies to everybody other than Vadim for burdening the forum with double-dutch.)Quote from Vadim on October 30, 2019, 4:56 pmQuote from AntC on October 29, 2019, 9:23 pmI think I can express a FD, but it relies on fixing

`R00`

as`DUM`

. Without that, anything else is going to be unprovable. And that's where I'm still stuck (after much trying).This is recurring theme of yours, but again, I'm more confused about uniqueness now, than in the past (before you raised the issue). What is uniqueness of constants and operations in

Universal Algebra? I don't see it covered anywhere, except perhaps couple of exercises in undergraduate algebra textbooks asking to prove uniqueness of`0`

in a group or ring.When a Universal Algebra text says "An

onn-ary operationAis a function ", it means the operation " takesnelements ofAand returns a single element ofA." Not only returns a single element but that provably it returns a single element for all possible combos ofnelements as operands.Once again, there is nothing special about constants compared to operations, so why are the book authors compelled to prove uniqueness of

`0`

?Yes a constant is just a nullary operation. All operations are defined by axioms (including for

`0`

). We have to prove those axioms are sufficient to fix`0`

otherwise any axiom that uses`0`

to define some operation fails to define that operation as a function. (i.e. it might just define a 'relation' in the algebraic sense.)So for example we have to prove that a definition for

`R01`

aka`DEE`

fixes it uniquely. (That's trivial, a blink of an eye in Prover9.)And if we start questioning uniqueness of other operations, then we get nowhere in any algebra.

Certainly it's tedious to prove uniqueness for every constant/operation introduced. So I guess textbook authors don't trouble the reader with it. If you're breaking new algebraic ground, you must prove uniqueness. So

Principia Mathematicais full of tedious proofs (and when mechanised theorem provers became available, they showed that some of Russell & Whitehead's proofs are not complete.)Look at the issue from the model theory perspective. As long as your axiom system outputs models which you can interpret as database relations, where exactly is the problem of the uniqueness of

`R00`

?But so far I

can'tinterpret the models as database relations. Mace4 keeps throwing up models where`R00`

might be`DUM`

, or might be some relation with a single attribute and all possible tuples for that heading. By "might be" I mean is consistent with.How does the alleged nonuniqueness affect the theorems that you can

formallydeduce in your system?Mostly by failing to prove that what I want to be functions are in fact functions (including for the dratted nullary function

`R00`

).When you are saying that an axiom system has to associate

`R00`

with`Dum`

unambiguously, you mean something else.I mean something like the following, since you only seem to understand talking in code.

Take generalised difference aka NOT MATCHING. You have equations characterising that in one of your papers: (I won't say axioms defining or proving it; but having stared long and hard at these following equations, I'm sure they fix

`/`

-- if only I could fix`R00`

.)(x ^ y) v (x \ y) = x. (x ^ y) ^ (x \ y) = (x ^ y) ^ R00. (x ^ y) v d2(x, y) = x. % duplicate def'n, changing the name (x ^ y) ^ d2(x, y) = (x ^ y) ^ R00. % % x \ y = d2(x, y). % [goal] % (x \ (x \ y)) = (x ^ y) v (x ^ R00). % [goal] MATCHING equiv double-NOT MATCHINGNote

`\`

is defined in terms of only`^, v, R00`

.Mace4 finds a counter-example for that first goal in no time. To give my axioms in full:

x ^ x = x. x ^ y = y ^ x. x ^ (y ^ z) = (x ^ y) ^ z. R01 ^ x = x. % R01 provably unique R10 ^ x = R10. % R10 provably unique x ^ z = x & y ^ z = y <-> z ^ (x v y) = (x v y). % distributivity axiom % % that (non-standard) def'n for v is provably unique. R00 ^ x != x <-> x v R00 = R01. % R00 not provably uniqueBy all means supply your own definitions/axioms for

`R00`

. (I can offer you heaps.) What you can't do in this 'game' is supply definitions for`\`

in terms of other operators -- unless those are defined in terms of`^, v`

. Because then you're potentially talking about some other operation.

There is a concept of representative relation algebras,

I have no idea what that is, do you? Or is this more cargo-cult algebra from you? The very first thing that wikipedia page says (in effect) is that this has nothing to do with relational algebra in the database sense.

that is when formal elements of algebra can be interpreted as binary relations and operations in both systems match. I think you are after analogous concept in the area of relational lattices.

I have no idea what you're talking about. I suspect you have no idea either.

Given a model satisfying a formal system of relational lattice axioms, would we always be able to interpret the elements of the model as database relations? I didn't encounter such "abnormal" models in either LMH or 2x2 axiom system, but the question is open.

Tadeus conceded [private email with you] that the LMH system doesn't fix

`R00`

(their`H`

).

`R00`

to obtain headings.`R00`

is under-specified. Everything using`R00`

is incomplete.The axiom system is a system of requirements to which operations should comply.

There is an overarching requirement (I've already quoted the very first sentence of the wiki on UA) that operations must be functions.

All operations are introduced at once, and there is no intrinsic order among them.

Sure. So what? For my sanity, since

`v`

is supposed to be the dual of`^`

, I'd rather work with a definition that specifies`v`

as the dual of`^`

. It's a perfectly valid way to define a bi-lattice, by which I mean you can prove all the same theorems.

Quote from Vadim on October 30, 2019, 4:56 pmQuote from AntC on October 29, 2019, 9:23 pm`R00`

as`DUM`

. Without that, anything else is going to be unprovable. And that's where I'm still stuck (after much trying).This is recurring theme of yours, but again, I'm more confused about uniqueness now, than in the past (before you raised the issue). What is uniqueness of constants and operations in

Universal Algebra? I don't see it covered anywhere, except perhaps couple of exercises in undergraduate algebra textbooks asking to prove uniqueness of`0`

in a group or ring.

When a Universal Algebra text says "An ** n-ary operation** on

*A*is a function ", it means the operation " takes

*n*elements of

*A*and returns a single element of

*A*." Not only returns a single element but that provably it returns a single element for all possible combos of

*n*elements as operands.

Once again, there is nothing special about constants compared to operations, so why are the book authors compelled to prove uniqueness of

`0`

?

Yes a constant is just a nullary operation. All operations are defined by axioms (including for `0`

). We have to prove those axioms are sufficient to fix `0`

otherwise any axiom that uses `0`

to define some operation fails to define that operation as a function. (i.e. it might just define a 'relation' in the algebraic sense.)

So for example we have to prove that a definition for `R01`

aka `DEE`

fixes it uniquely. (That's trivial, a blink of an eye in Prover9.)

And if we start questioning uniqueness of other operations, then we get nowhere in any algebra.

Certainly it's tedious to prove uniqueness for every constant/operation introduced. So I guess textbook authors don't trouble the reader with it. If you're breaking new algebraic ground, you must prove uniqueness. So *Principia Mathematica* is full of tedious proofs (and when mechanised theorem provers became available, they showed that some of Russell & Whitehead's proofs are not complete.)

Look at the issue from the model theory perspective. As long as your axiom system outputs models which you can interpret as database relations, where exactly is the problem of the uniqueness of

`R00`

?

But so far I *can't* interpret the models as database relations. Mace4 keeps throwing up models where `R00`

might be `DUM`

, or might be some relation with a single attribute and all possible tuples for that heading. By "might be" I mean is consistent with.

How does the alleged nonuniqueness affect the theorems that you can

formallydeduce in your system?

Mostly by failing to prove that what I want to be functions are in fact functions (including for the dratted nullary function `R00`

).

When you are saying that an axiom system has to associate

`R00`

with`Dum`

unambiguously, you mean something else.

I mean something like the following, since you only seem to understand talking in code.

Take generalised difference aka NOT MATCHING. You have equations characterising that in one of your papers: (I won't say axioms defining or proving it; but having stared long and hard at these following equations, I'm sure they fix `/`

-- if only I could fix `R00`

.)

(x ^ y) v (x \ y) = x. (x ^ y) ^ (x \ y) = (x ^ y) ^ R00. (x ^ y) v d2(x, y) = x. % duplicate def'n, changing the name (x ^ y) ^ d2(x, y) = (x ^ y) ^ R00. % % x \ y = d2(x, y). % [goal] % (x \ (x \ y)) = (x ^ y) v (x ^ R00). % [goal] MATCHING equiv double-NOT MATCHING

Note `\`

is defined in terms of only `^, v, R00`

.

Mace4 finds a counter-example for that first goal in no time. To give my axioms in full:

x ^ x = x. x ^ y = y ^ x. x ^ (y ^ z) = (x ^ y) ^ z. R01 ^ x = x. % R01 provably unique R10 ^ x = R10. % R10 provably unique x ^ z = x & y ^ z = y <-> z ^ (x v y) = (x v y). % distributivity axiom % % that (non-standard) def'n for v is provably unique. R00 ^ x != x <-> x v R00 = R01. % R00 not provably unique

By all means supply your own definitions/axioms for `R00`

. (I can offer you heaps.) What you can't do in this 'game' is supply definitions for `\`

in terms of other operators -- unless those are defined in terms of `^, v`

. Because then you're potentially talking about some other operation.

There is a concept of representative relation algebras,

I have no idea what that is, do you? Or is this more cargo-cult algebra from you? The very first thing that wikipedia page says (in effect) is that this has nothing to do with relational algebra in the database sense.

that is when formal elements of algebra can be interpreted as binary relations and operations in both systems match. I think you are after analogous concept in the area of relational lattices.

I have no idea what you're talking about. I suspect you have no idea either.

Given a model satisfying a formal system of relational lattice axioms, would we always be able to interpret the elements of the model as database relations? I didn't encounter such "abnormal" models in either LMH or 2x2 axiom system, but the question is open.

Tadeus conceded [private email with you] that the LMH system doesn't fix `R00`

(their `H`

).

`R00`

to obtain headings.`R00`

is under-specified. Everything using`R00`

is incomplete.The axiom system is a system of requirements to which operations should comply.

There is an overarching requirement (I've already quoted the very first sentence of the wiki on UA) that operations must be functions.

All operations are introduced at once, and there is no intrinsic order among them.

Sure. So what? For my sanity, since `v`

is supposed to be the dual of `^`

, I'd rather work with a definition that specifies `v`

as the dual of `^`

. It's a perfectly valid way to define a bi-lattice, by which I mean you can prove all the same theorems.