I welcome the fact that you have switched from traditional RA
operators to simpler set (D&Ds "A"lgebra: <AND>, <OR>, and <NOT>).
Next, you seemed to approach view update problem algebraically, but
stopped short of writing actual equations for base relations, views,
their increments, and constraints. Here they are:

The base relations:

S - Suppliers
SP - SuppliedParts

Foreigh key constraint between S and SP is formally written as:

(SP ^ S') v R00 = R00.

where I leveraged standard relational lattice operators: "^" - join,
"v" - generalized union, and R00 empty relation with empty header (aka
D&D TABLE_DUM). Informally, foreign key constraint asserts that
SuppliedParts antijoined with Suppliers produce an empty relation.

Next, lets represent the insertion into the view, which is a join of S
and SP, as a relation D (Delta). Therefore, D has the same header as
SP ^ S, which is formally written as

(SP ^ S) ^ R00 = D ^ R00.

Our final assumption is that we insert new supplier data, therefore D
should have no S# in common with the existing data:

(D ^ (SP v S)) ^ R00 = R00.

These three equations are all our knowlwedge about SP ^ S view
updates. Now we plug them (together with RL axiom system) into
Prover9, and derive

(SP v D) ^ (S v D) = (SP ^ S) v D.

with a single press of a button! Informally, under some very natural
conditions (the 3 assertions that I described early) an increment to
the view SP ^ S can be decomposed into independent increments of the
base relations S and D.

I welcome the fact that you have switched from traditional RA
operators to simpler set (D&Ds "A"lgebra: <AND>, <OR>, and <NOT>).
Next, you seemed to approach view update problem algebraically, but
stopped short of writing actual equations for base relations, views,
their increments, and constraints. Here they are:

The base relations:

S - Suppliers
SP - SuppliedParts

Foreigh key constraint between S and SP is formally written as:

(SP ^ S') v R00 = R00.

where I leveraged standard relational lattice operators: "^" - join,
"v" - generalized union, and R00 empty relation with empty header (aka
D&D TABLE_DUM). Informally, foreign key constraint asserts that
SuppliedParts antijoined with Suppliers produce an empty relation.

Next, lets represent the insertion into the view, which is a join of S
and SP, as a relation D (Delta). Therefore, D has the same header as
SP ^ S, which is formally written as

(SP ^ S) ^ R00 = D ^ R00.

Our final assumption is that we insert new supplier data, therefore D
should have no S# in common with the existing data:

(D ^ (SP v S)) ^ R00 = R00.

These three equations are all our knowlwedge about SP ^ S view
updates. Now we plug them (together with RL axiom system) into
Prover9, and derive

(SP v D) ^ (S v D) = (SP ^ S) v D.

with a single press of a button! Informally, under some very natural
conditions (the 3 assertions that I described early) an increment to
the view SP ^ S can be decomposed into independent increments of the
base relations S and D.

I welcome the fact that you have switched from traditional RA
operators to simpler set (D&Ds "A"lgebra: <AND>, <OR>, and <NOT>).
Next, you seemed to approach view update problem algebraically, but
stopped short of writing actual equations for base relations, views,
their increments, and constraints. Here they are:

The base relations:

S - Suppliers
SP - SuppliedParts

Foreigh key constraint between S and SP is formally written as:

(SP ^ S') v R00 = R00.

where I leveraged standard relational lattice operators: "^" - join,
"v" - generalized union, and R00 empty relation with empty header (aka
D&D TABLE_DUM). Informally, foreign key constraint asserts that
SuppliedParts antijoined with Suppliers produce an empty relation.

Next, lets represent the insertion into the view, which is a join of S
and SP, as a relation D (Delta). Therefore, D has the same header as
SP ^ S, which is formally written as

(SP ^ S) ^ R00 = D ^ R00.

Our final assumption is that we insert new supplier data, therefore D
should have no S# in common with the existing data:

(D ^ (SP v S)) ^ R00 = R00.

These three equations are all our knowlwedge about SP ^ S view
updates. Now we plug them (together with RL axiom system) into
Prover9, and derive

(SP v D) ^ (S v D) = (SP ^ S) v D.

with a single press of a button! Informally, under some very natural
conditions (the 3 assertions that I described early) an increment to
the view SP ^ S can be decomposed into independent increments of the
base relations S and D.

I welcome the fact that you have switched from traditional RA
operators to simpler set (D&Ds "A"lgebra: <AND>, <OR>, and <NOT>).
Next, you seemed to approach view update problem algebraically, but
stopped short of writing actual equations for base relations, views,
their increments, and constraints. Here they are:

The base relations:

S - Suppliers
SP - SuppliedParts

Foreigh key constraint between S and SP is formally written as:

(SP ^ S') v R00 = R00.

where I leveraged standard relational lattice operators: "^" - join,
"v" - generalized union, and R00 empty relation with empty header (aka
D&D TABLE_DUM). Informally, foreign key constraint asserts that
SuppliedParts antijoined with Suppliers produce an empty relation.

Next, lets represent the insertion into the view, which is a join of S
and SP, as a relation D (Delta). Therefore, D has the same header as
SP ^ S, which is formally written as

(SP ^ S) ^ R00 = D ^ R00.

Our final assumption is that we insert new supplier data, therefore D
should have no S# in common with the existing data:

(D ^ (SP v S)) ^ R00 = R00.

These three equations are all our knowlwedge about SP ^ S view
updates. Now we plug them (together with RL axiom system) into
Prover9, and derive

(SP v D) ^ (S v D) = (SP ^ S) v D.

with a single press of a button! Informally, under some very natural
conditions (the 3 assertions that I described early) an increment to
the view SP ^ S can be decomposed into independent increments of the
base relations S and D.

I welcome the fact that you have switched from traditional RA
operators to simpler set (D&Ds "A"lgebra: <AND>, <OR>, and <NOT>).
Next, you seemed to approach view update problem algebraically, but
stopped short of writing actual equations for base relations, views,
their increments, and constraints. Here they are:

The base relations:

S - Suppliers
SP - SuppliedParts

Foreigh key constraint between S and SP is formally written as:

(SP ^ S') v R00 = R00.

where I leveraged standard relational lattice operators: "^" - join,
"v" - generalized union, and R00 empty relation with empty header (aka
D&D TABLE_DUM). Informally, foreign key constraint asserts that
SuppliedParts antijoined with Suppliers produce an empty relation.

Next, lets represent the insertion into the view, which is a join of S
and SP, as a relation D (Delta). Therefore, D has the same header as
SP ^ S, which is formally written as

(SP ^ S) ^ R00 = D ^ R00.

Our final assumption is that we insert new supplier data, therefore D
should have no S# in common with the existing data:

(D ^ (SP v S)) ^ R00 = R00.

These three equations are all our knowlwedge about SP ^ S view
updates. Now we plug them (together with RL axiom system) into
Prover9, and derive

(SP v D) ^ (S v D) = (SP ^ S) v D.

with a single press of a button! Informally, under some very natural
conditions (the 3 assertions that I described early) an increment to
the view SP ^ S can be decomposed into independent increments of the
base relations S and D.

I welcome the fact that you have switched from traditional RA
operators to simpler set (D&Ds "A"lgebra: <AND>, <OR>, and <NOT>).
Next, you seemed to approach view update problem algebraically, but
stopped short of writing actual equations for base relations, views,
their increments, and constraints. Here they are:

The base relations:

S - Suppliers
SP - SuppliedParts

Foreigh key constraint between S and SP is formally written as:

(SP ^ S') v R00 = R00.

where I leveraged standard relational lattice operators: "^" - join,
"v" - generalized union, and R00 empty relation with empty header (aka
D&D TABLE_DUM). Informally, foreign key constraint asserts that
SuppliedParts antijoined with Suppliers produce an empty relation.

Next, lets represent the insertion into the view, which is a join of S
and SP, as a relation D (Delta). Therefore, D has the same header as
SP ^ S, which is formally written as

(SP ^ S) ^ R00 = D ^ R00.

Our final assumption is that we insert new supplier data, therefore D
should have no S# in common with the existing data:

(D ^ (SP v S)) ^ R00 = R00.

These three equations are all our knowlwedge about SP ^ S view
updates. Now we plug them (together with RL axiom system) into
Prover9, and derive

(SP v D) ^ (S v D) = (SP ^ S) v D.

with a single press of a button! Informally, under some very natural
conditions (the 3 assertions that I described early) an increment to
the view SP ^ S can be decomposed into independent increments of the
base relations S and D.

I welcome the fact that you have switched from traditional RA
operators to simpler set (D&Ds "A"lgebra: <AND>, <OR>, and <NOT>).
Next, you seemed to approach view update problem algebraically, but
stopped short of writing actual equations for base relations, views,
their increments, and constraints. Here they are:

The base relations:

S - Suppliers
SP - SuppliedParts

Foreigh key constraint between S and SP is formally written as:

(SP ^ S') v R00 = R00.

where I leveraged standard relational lattice operators: "^" - join,
"v" - generalized union, and R00 empty relation with empty header (aka
D&D TABLE_DUM). Informally, foreign key constraint asserts that
SuppliedParts antijoined with Suppliers produce an empty relation.

Next, lets represent the insertion into the view, which is a join of S
and SP, as a relation D (Delta). Therefore, D has the same header as
SP ^ S, which is formally written as

(SP ^ S) ^ R00 = D ^ R00.

Our final assumption is that we insert new supplier data, therefore D
should have no S# in common with the existing data:

(D ^ (SP v S)) ^ R00 = R00.

These three equations are all our knowlwedge about SP ^ S view
updates. Now we plug them (together with RL axiom system) into
Prover9, and derive

(SP v D) ^ (S v D) = (SP ^ S) v D.

with a single press of a button! Informally, under some very natural
conditions (the 3 assertions that I described early) an increment to
the view SP ^ S can be decomposed into independent increments of the
base relations S and D.

I welcome the fact that you have switched from traditional RA
operators to simpler set (D&Ds "A"lgebra: <AND>, <OR>, and <NOT>).
Next, you seemed to approach view update problem algebraically, but
stopped short of writing actual equations for base relations, views,
their increments, and constraints. Here they are:

The base relations:

S - Suppliers
SP - SuppliedParts

Foreigh key constraint between S and SP is formally written as:

(SP ^ S') v R00 = R00.

where I leveraged standard relational lattice operators: "^" - join,
"v" - generalized union, and R00 empty relation with empty header (aka
D&D TABLE_DUM). Informally, foreign key constraint asserts that
SuppliedParts antijoined with Suppliers produce an empty relation.

Next, lets represent the insertion into the view, which is a join of S
and SP, as a relation D (Delta). Therefore, D has the same header as
SP ^ S, which is formally written as

(SP ^ S) ^ R00 = D ^ R00.

Our final assumption is that we insert new supplier data, therefore D
should have no S# in common with the existing data:

(D ^ (SP v S)) ^ R00 = R00.

These three equations are all our knowlwedge about SP ^ S view
updates. Now we plug them (together with RL axiom system) into
Prover9, and derive

(SP v D) ^ (S v D) = (SP ^ S) v D.

with a single press of a button! Informally, under some very natural
conditions (the 3 assertions that I described early) an increment to
the view SP ^ S can be decomposed into independent increments of the
base relations S and D.

I welcome the fact that you have switched from traditional RA
operators to simpler set (D&Ds "A"lgebra: <AND>, <OR>, and <NOT>).
Next, you seemed to approach view update problem algebraically, but
stopped short of writing actual equations for base relations, views,
their increments, and constraints. Here they are:

The base relations:

S - Suppliers
SP - SuppliedParts

Foreigh key constraint between S and SP is formally written as:

(SP ^ S') v R00 = R00.

where I leveraged standard relational lattice operators: "^" - join,
"v" - generalized union, and R00 empty relation with empty header (aka
D&D TABLE_DUM). Informally, foreign key constraint asserts that
SuppliedParts antijoined with Suppliers produce an empty relation.

Next, lets represent the insertion into the view, which is a join of S
and SP, as a relation D (Delta). Therefore, D has the same header as
SP ^ S, which is formally written as

(SP ^ S) ^ R00 = D ^ R00.

Our final assumption is that we insert new supplier data, therefore D
should have no S# in common with the existing data:

(D ^ (SP v S)) ^ R00 = R00.

These three equations are all our knowlwedge about SP ^ S view
updates. Now we plug them (together with RL axiom system) into
Prover9, and derive

(SP v D) ^ (S v D) = (SP ^ S) v D.

with a single press of a button! Informally, under some very natural
conditions (the 3 assertions that I described early) an increment to
the view SP ^ S can be decomposed into independent increments of the
base relations S and D.

vadimtro (AT) gmail (DOT) com wrote:
Thanks. Although the relational lattice has seemed a fuzzy to me (no
doubt that's my fault as usually takes me years before I feel confident
in a mathematical topic), I gather that this example is about "insert"
to JOIN. Just guessing but I gather that RL could be seen as a
alternative way of understanding RM, maybe more fundamental in some ways
and maybe has some more useful mechanical theoretical tools, so I wonder
what happens with "delete" to JOIN (which I believe is the operation
that many people find controversial)?

BTW, ever since I first read about it, I've tried to use the TTM algebra
in my head because the small and tight definitions make it easier to
check my thoughts by comparing results in terms of relations. But I
find most other people tune out when I use them to explain myself. The
chapter 4 in the original TTM was by itself worth the price of the book
to me because before that I just talked about "uniform sentences" and
had an even harder time trying to explain to people what I meant. It
was also harder to understand myself! I even overload &, | and ^ to save
writing but also to emphasize the parallels with simple logic.
Overloading those operators has never bothered me even though I know
many technocrats don't like it. I don't mind if bakers make bread
instead of baking it or manufacturers make products rather than build them.

Also BTW, because I didn't think it affected the problem, I wasn't
assuming any foreign key, but if I did I could express the one involving
S and SP as: SP{S#} & S{S#} = SP{S#} (where & means <AND>).