Relcons and relfuns are both FOPL

#1 · June 5, 2020, 2:59 pm

I've been chasing down some of the maths underlying the kind of formalism used in App-A and in my previous post on the subject. It ain't easy reading.

In summary:

functions are relations (of the maths sort, not the RA sort)
'well-behaved' relations are functions
AppA relcons are (maths) relations, and (subject to certain conditions), they are functions
first order logic can use either functions or relations (or both) as predicates
there is a mechanical process for converting from one to the other.

IOW the extended RA up to and including new value generation and 'canned' aggregation is FOPL. They can be formally defined by set-builder notation (as I have done).

The only parts of the ERA that are not FOPL are:

TCLOSE and GTC, which require (fixed point) recursion. [The formal definition requires self-reference or summing a series.]
Generalised aggregation (OO Pre 6), which requires 2nd order functions [a 'map' function].

These conclusions re aggregation and TC do not seem to sit well with Alice, but I don't propose to try to figure out why.

The Wikipedia article is a good source, but this is an easier read: https://pavpanchekha.com/blog/functions-relations.html.

Andl - A New Database Language - andl.org

#2 · June 6, 2020, 11:34 am

Quote from dandl on June 5, 2020, 2:59 pm

I've been chasing down some of the maths underlying the kind of formalism used in App-A and in my previous post on the subject. It ain't easy reading.

In summary:

functions are relations (of the maths sort, not the RA sort)

'well-behaved' relations are functions

AppA relcons are (maths) relations, and (subject to certain conditions), they are functions

first order logic can use either functions or relations (or both) as predicates

there is a mechanical process for converting from one to the other.

IOW the extended RA up to and including new value generation and 'canned' aggregation is FOPL. They can be formally defined by set-builder notation (as I have done).

The only parts of the ERA that are not FOPL are:

TCLOSE and GTC, which require (fixed point) recursion. [The formal definition requires self-reference or summing a series.]

Generalised aggregation (OO Pre 6), which requires 2nd order functions [a 'map' function].

These conclusions re aggregation and TC do not seem to sit well with Alice, but I don't propose to try to figure out why.

The Wikipedia article is a good source, but this is an easier read: https://pavpanchekha.com/blog/functions-relations.html.

What do you mean by "well behaved"? According to my understanding not all relations are functions. For example, I'm not sure how TABLE_DUM and SP{P#, QTY} can be regarded as such. In any was, if all relations are functions and all functions are relations, why would we have two terms for the same thing?

I see no need for "(of the maths sort, not the RA sort)". Whether tuple components are distinguished by position or name is not really significant, is it?

Hugh

Coauthor of The Third Manifesto and related books.

#3 · June 6, 2020, 1:06 pm

Quote from Hugh on June 6, 2020, 11:34 am

What do you mean by "well behaved"? According to my understanding not all relations are functions. For example, I'm not sure how TABLE_DUM and SP{P#, QTY} can be regarded as such. In any was, if all relations are functions and all functions are relations, why would we have two terms for the same thing?

I see no need for "(of the maths sort, not the RA sort)". Whether tuple components are distinguished by position or name is not really significant, is it?

Hugh

All relations are in a sense their own "real world truth valuation function". That is, each tuple is mapped to either true or false, the "present" ones to true, the absent ones to false. Not a sense that makes the function broadly suitable for further machine computation (we do such computations using the RA), but it's a function nonetheless.

ADDIT

So TABLE_DEE maps its only member (TUPLE_DEE) to true, and TABLE_DUM maps the only member of its domain (TUPLE_DEE again) to false.

#4 · June 6, 2020, 2:26 pm

Spot on. Relations in maths are just mappings between sets, and apply to all kinds of things. Database relations - as per Erwin.

All functions are relations - they map a key (the arguments) to a singular value. Any relation that does that is a function.

The relcons in App-A are of that form. The relcon PLUS with the predicate X+Y=Z maps the arguments (X,Y) to a singular value (Z) and therefore it is a function.

IMO this 'closes the loop'. Functions are relations and can be treated as such by the RA. Relcons are functions and can be formally defined in set-builder notation. Relcons can be implemented precisely because they are functions. And the RA operators that depend on them are within FOPL. Tidy.

You could add a formal definition of relcons to App-A in the same FOPL style, but not for TCLOSE and aggregation per OO Pre 6. That takes something extra.

Andl - A New Database Language - andl.org

#5 · June 6, 2020, 7:49 pm

Quote from dandl on June 6, 2020, 2:26 pm

Spot on. Relations in maths are just mappings between sets, and apply to all kinds of things. Database relations - as per Erwin.

All functions are relations - they map a key (the arguments) to a singular value. Any relation that does that is a function.

The relcons in App-A are of that form. The relcon PLUS with the predicate X+Y=Z maps the arguments (X,Y) to a singular value (Z) and therefore it is a function.

IMO this 'closes the loop'. Functions are relations and can be treated as such by the RA. Relcons are functions and can be formally defined in set-builder notation. Relcons can be implemented precisely because they are functions. And the RA operators that depend on them are within FOPL. Tidy.

You could add a formal definition of relcons to App-A in the same FOPL style, but not for TCLOSE and aggregation per OO Pre 6. That takes something extra.

Even for TCLOSE, it holds that the relations resulting from an invocation of it are (/can be seen as) a function mapping the (start-of-directed-path, end-of-directed-path) pairs to truth values. That the corresponding predicate is itself not expressible in FOPL, is rather orthogonal to the relation still being a function in the sense indicated.

And I continue to fail to see the added value of these observations, because the RA as we know it already exploits all of the power they offer.

Formally, the reason why this is so is that every relation is equivalent to another one [theoretically] computable by

(EXTEND R {TV := true}) UNION (EXTEND ((INTERSECT SAME_HEADING_AS(R) {}) NOT MATCHING R) {TV := false}).

R is computable from this using (E stands for the EXTEND)

(E WHERE TV) {ALL BUT {TV}}

The two are isomorphic and the former is a function from {all attributes of R} to TV. So the latter is too, and the latter is R.

#6 · June 7, 2020, 1:17 am

Quote from dandl on June 7, 2020, 1:17 am

Quote from Erwin on June 6, 2020, 7:49 pm

Quote from dandl on June 6, 2020, 2:26 pm

Spot on. Relations in maths are just mappings between sets, and apply to all kinds of things. Database relations - as per Erwin.

All functions are relations - they map a key (the arguments) to a singular value. Any relation that does that is a function.

The relcons in App-A are of that form. The relcon PLUS with the predicate X+Y=Z maps the arguments (X,Y) to a singular value (Z) and therefore it is a function.

IMO this 'closes the loop'. Functions are relations and can be treated as such by the RA. Relcons are functions and can be formally defined in set-builder notation. Relcons can be implemented precisely because they are functions. And the RA operators that depend on them are within FOPL. Tidy.

You could add a formal definition of relcons to App-A in the same FOPL style, but not for TCLOSE and aggregation per OO Pre 6. That takes something extra.

Even for TCLOSE, it holds that the relations resulting from an invocation of it are (/can be seen as) a function mapping the (start-of-directed-path, end-of-directed-path) pairs to truth values. That the corresponding predicate is itself not expressible in FOPL, is rather orthogonal to the relation still being a function in the sense indicated.

Orthogonal? It's not at issue that the argument and result of TCLOSE are relations with the same heading, thus the same predicate. The need for TCLOSE shows precisely the limits of FOPL: there is no predicate for "start and end of path through zero or more intermediate nodes". The function required to test that is intrinsically recursive or a results in a series. This is a point of difference with Datalog, in which TCLOSE can be expressed with no great difficulty.

And I continue to fail to see the added value of these observations, because the RA as we know it already exploits all of the power they offer.

Formally, the reason why this is so is that every relation is equivalent to another one [theoretically] computable by

(EXTEND R {TV := true}) UNION (EXTEND ((INTERSECT SAME_HEADING_AS(R) {}) NOT MATCHING R) {TV := false}).

R is computable from this using (E stands for the EXTEND)

(E WHERE TV) {ALL BUT {TV}}

The two are isomorphic and the former is a function from {all attributes of R} to TV. So the latter is too, and the latter is R.

Sorry, I don't follow. The point of my exercise was to provide a formalism of the RA as the basis for incorporating it into some D. Although I don't understand what you're trying to prove, I do know that you can't use a D as part of your proof. There are too many assumptions built into the shorthands of that language to know whether it proves anything.

Quote from Erwin on June 6, 2020, 7:49 pm

Quote from dandl on June 6, 2020, 2:26 pm

Spot on. Relations in maths are just mappings between sets, and apply to all kinds of things. Database relations - as per Erwin.

All functions are relations - they map a key (the arguments) to a singular value. Any relation that does that is a function.

The relcons in App-A are of that form. The relcon PLUS with the predicate X+Y=Z maps the arguments (X,Y) to a singular value (Z) and therefore it is a function.

IMO this 'closes the loop'. Functions are relations and can be treated as such by the RA. Relcons are functions and can be formally defined in set-builder notation. Relcons can be implemented precisely because they are functions. And the RA operators that depend on them are within FOPL. Tidy.

You could add a formal definition of relcons to App-A in the same FOPL style, but not for TCLOSE and aggregation per OO Pre 6. That takes something extra.

Even for TCLOSE, it holds that the relations resulting from an invocation of it are (/can be seen as) a function mapping the (start-of-directed-path, end-of-directed-path) pairs to truth values. That the corresponding predicate is itself not expressible in FOPL, is rather orthogonal to the relation still being a function in the sense indicated.

Orthogonal? It's not at issue that the argument and result of TCLOSE are relations with the same heading, thus the same predicate. The need for TCLOSE shows precisely the limits of FOPL: there is no predicate for "start and end of path through zero or more intermediate nodes". The function required to test that is intrinsically recursive or a results in a series. This is a point of difference with Datalog, in which TCLOSE can be expressed with no great difficulty.

And I continue to fail to see the added value of these observations, because the RA as we know it already exploits all of the power they offer.

Formally, the reason why this is so is that every relation is equivalent to another one [theoretically] computable by

(EXTEND R {TV := true}) UNION (EXTEND ((INTERSECT SAME_HEADING_AS(R) {}) NOT MATCHING R) {TV := false}).

R is computable from this using (E stands for the EXTEND)

(E WHERE TV) {ALL BUT {TV}}

The two are isomorphic and the former is a function from {all attributes of R} to TV. So the latter is too, and the latter is R.

Sorry, I don't follow. The point of my exercise was to provide a formalism of the RA as the basis for incorporating it into some D. Although I don't understand what you're trying to prove, I do know that you can't use a D as part of your proof. There are too many assumptions built into the shorthands of that language to know whether it proves anything.

Andl - A New Database Language - andl.org

#7 · June 7, 2020, 1:51 am

Quote from AntC on June 7, 2020, 1:51 am

Quote from dandl on June 7, 2020, 1:17 am

Quote from Erwin on June 6, 2020, 7:49 pm

Quote from dandl on June 6, 2020, 2:26 pm

Spot on. Relations in maths are just mappings between sets, and apply to all kinds of things. Database relations - as per Erwin.

All functions are relations - they map a key (the arguments) to a singular value. Any relation that does that is a function.

The relcons in App-A are of that form. The relcon PLUS with the predicate X+Y=Z maps the arguments (X,Y) to a singular value (Z) and therefore it is a function.

IMO this 'closes the loop'. Functions are relations and can be treated as such by the RA. Relcons are functions and can be formally defined in set-builder notation. Relcons can be implemented precisely because they are functions. And the RA operators that depend on them are within FOPL. Tidy.

You could add a formal definition of relcons to App-A in the same FOPL style, but not for TCLOSE and aggregation per OO Pre 6. That takes something extra.

Even for TCLOSE, it holds that the relations resulting from an invocation of it are (/can be seen as) a function mapping the (start-of-directed-path, end-of-directed-path) pairs to truth values. That the corresponding predicate is itself not expressible in FOPL, is rather orthogonal to the relation still being a function in the sense indicated.

Orthogonal? It's not at issue that the argument and result of TCLOSE are relations with the same heading, thus the same predicate.

Bzzzt. Relations with the same heading do not necessarily have the same predicate. We could wheel out the old Shops-and-Alarms example. We could note that the heading for S WHERE CITY = 'Leeds' is the same as for S; but their predicates are different. Therefore ...

The need for TCLOSE shows precisely the limits of FOPL: there is no predicate for "start and end of path through zero or more intermediate nodes".

That the result of TCLOSE has the same heading as its argument says nothing about the predicate of the result. Of course you can express a predicate to the effect 'there is a chain of nodes from X to Y' (or whatever are the attribute names).

The function required to test that is intrinsically recursive or a results in a series.

A relvar/relation predicate is not a function; it's a membership condition; and it doesn't have to be testable by any 'definite procedure'. It merely has to be asserted by an authorised user making authorised data entry -- or as a logical consequence of relvar predicate(s) together with the logical connectives derived from the relational operations over those relvar(s).

This is a point of difference with Datalog, in which TCLOSE can be expressed with no great difficulty.

If Datalog's TCLOSE produces the same answer as a D's for all possible input values; there is no difference in the FOPL predicate of the result. Unless you're going to get all wishy-washy metaphysical about same extension, different intension. I despair of anything you say getting so cogent as to be wishy-washy metaphysical.

...

Sorry, I don't follow. The point of my exercise was to provide a formalism of the RA as the basis for incorporating it into some D.

Appendix A already does that. Codd 1972 already does that (up to a point). If your exercise has any sane point -- and I haven't seen one so far expressed cogently from you -- then it's going to be logically equivalent to those two sources. We can readily agree those two sources have some limitations/extensions left for the reader. You've failed so far to get the basics across; so any claim that you're covering the leftovers is so far null and void.

Although I don't understand what you're trying to prove, I do know that you can't use a D as part of your proof. There are too many assumptions built into the shorthands of that language to know whether it proves anything.

>sigh< The abstract concepts expressed for a D in the TTM doco are not shorthands 'we do not prescribe syntax'. Tutorial D includes plenty of shorthands; they're expanded in Appendix A (and in various discussions in DTATRM); the semantics of the core operators is given in Appendix A. Yes the FORMAL DEFINITIONS give assumptions; they're more than adequate to prove how the A algebra works as a whole.

Quote from dandl on June 7, 2020, 1:17 am

Quote from Erwin on June 6, 2020, 7:49 pm

Quote from dandl on June 6, 2020, 2:26 pm

Spot on. Relations in maths are just mappings between sets, and apply to all kinds of things. Database relations - as per Erwin.

All functions are relations - they map a key (the arguments) to a singular value. Any relation that does that is a function.

The relcons in App-A are of that form. The relcon PLUS with the predicate X+Y=Z maps the arguments (X,Y) to a singular value (Z) and therefore it is a function.

IMO this 'closes the loop'. Functions are relations and can be treated as such by the RA. Relcons are functions and can be formally defined in set-builder notation. Relcons can be implemented precisely because they are functions. And the RA operators that depend on them are within FOPL. Tidy.

You could add a formal definition of relcons to App-A in the same FOPL style, but not for TCLOSE and aggregation per OO Pre 6. That takes something extra.

Even for TCLOSE, it holds that the relations resulting from an invocation of it are (/can be seen as) a function mapping the (start-of-directed-path, end-of-directed-path) pairs to truth values. That the corresponding predicate is itself not expressible in FOPL, is rather orthogonal to the relation still being a function in the sense indicated.

Orthogonal? It's not at issue that the argument and result of TCLOSE are relations with the same heading, thus the same predicate.

Bzzzt. Relations with the same heading do not necessarily have the same predicate. We could wheel out the old Shops-and-Alarms example. We could note that the heading for S WHERE CITY = 'Leeds' is the same as for S; but their predicates are different. Therefore ...

The need for TCLOSE shows precisely the limits of FOPL: there is no predicate for "start and end of path through zero or more intermediate nodes".

That the result of TCLOSE has the same heading as its argument says nothing about the predicate of the result. Of course you can express a predicate to the effect 'there is a chain of nodes from X to Y' (or whatever are the attribute names).

The function required to test that is intrinsically recursive or a results in a series.

A relvar/relation predicate is not a function; it's a membership condition; and it doesn't have to be testable by any 'definite procedure'. It merely has to be asserted by an authorised user making authorised data entry -- or as a logical consequence of relvar predicate(s) together with the logical connectives derived from the relational operations over those relvar(s).

This is a point of difference with Datalog, in which TCLOSE can be expressed with no great difficulty.

If Datalog's TCLOSE produces the same answer as a D's for all possible input values; there is no difference in the FOPL predicate of the result. Unless you're going to get all wishy-washy metaphysical about same extension, different intension. I despair of anything you say getting so cogent as to be wishy-washy metaphysical.

...

Sorry, I don't follow. The point of my exercise was to provide a formalism of the RA as the basis for incorporating it into some D.

Appendix A already does that. Codd 1972 already does that (up to a point). If your exercise has any sane point -- and I haven't seen one so far expressed cogently from you -- then it's going to be logically equivalent to those two sources. We can readily agree those two sources have some limitations/extensions left for the reader. You've failed so far to get the basics across; so any claim that you're covering the leftovers is so far null and void.

Although I don't understand what you're trying to prove, I do know that you can't use a D as part of your proof. There are too many assumptions built into the shorthands of that language to know whether it proves anything.

>sigh< The abstract concepts expressed for a D in the TTM doco are not shorthands 'we do not prescribe syntax'. Tutorial D includes plenty of shorthands; they're expanded in Appendix A (and in various discussions in DTATRM); the semantics of the core operators is given in Appendix A. Yes the FORMAL DEFINITIONS give assumptions; they're more than adequate to prove how the A algebra works as a whole.

#8 · June 7, 2020, 10:30 am

Quote from Erwin on June 6, 2020, 1:06 pm

Quote from Hugh on June 6, 2020, 11:34 am

What do you mean by "well behaved"? According to my understanding not all relations are functions. For example, I'm not sure how TABLE_DUM and SP{P#, QTY} can be regarded as such. In any was, if all relations are functions and all functions are relations, why would we have two terms for the same thing?

I see no need for "(of the maths sort, not the RA sort)". Whether tuple components are distinguished by position or name is not really significant, is it?

Hugh

All relations are in a sense their own "real world truth valuation function". That is, each tuple is mapped to either true or false, the "present" ones to true, the absent ones to false. Not a sense that makes the function broadly suitable for further machine computation (we do such computations using the RA), but it's a function nonetheless.

ADDIT

So TABLE_DEE maps its only member (TUPLE_DEE) to true, and TABLE_DUM maps the only member of its domain (TUPLE_DEE again) to false.

The tuples in a relation are all and only those that would map to TRUE under the truth-valued function you adduce. The codomain of that function does thus not explicitly appear in the relation. A relation that is a function is one that has at least one non-key attribute, such as QTY in SP{S#, P#, QTY}.

Hugh

Coauthor of The Third Manifesto and related books.

#9 · June 8, 2020, 12:46 am

Quote from dandl on June 8, 2020, 12:46 am

Quote from AntC on June 7, 2020, 1:51 am

Quote from dandl on June 7, 2020, 1:17 am

Quote from Erwin on June 6, 2020, 7:49 pm

Quote from dandl on June 6, 2020, 2:26 pm

Spot on. Relations in maths are just mappings between sets, and apply to all kinds of things. Database relations - as per Erwin.

All functions are relations - they map a key (the arguments) to a singular value. Any relation that does that is a function.

The relcons in App-A are of that form. The relcon PLUS with the predicate X+Y=Z maps the arguments (X,Y) to a singular value (Z) and therefore it is a function.

IMO this 'closes the loop'. Functions are relations and can be treated as such by the RA. Relcons are functions and can be formally defined in set-builder notation. Relcons can be implemented precisely because they are functions. And the RA operators that depend on them are within FOPL. Tidy.

You could add a formal definition of relcons to App-A in the same FOPL style, but not for TCLOSE and aggregation per OO Pre 6. That takes something extra.

Even for TCLOSE, it holds that the relations resulting from an invocation of it are (/can be seen as) a function mapping the (start-of-directed-path, end-of-directed-path) pairs to truth values. That the corresponding predicate is itself not expressible in FOPL, is rather orthogonal to the relation still being a function in the sense indicated.

Orthogonal? It's not at issue that the argument and result of TCLOSE are relations with the same heading, thus the same predicate.

Bzzzt. Relations with the same heading do not necessarily have the same predicate. We could wheel out the old Shops-and-Alarms example. We could note that the heading for S WHERE CITY = 'Leeds' is the same as for S; but their predicates are different. Therefore ...

No, I meant predicate in the strict sense of first order predicate logic. You cannot express transitive closure in first order predicate logic.

The need for TCLOSE shows precisely the limits of FOPL: there is no predicate for "start and end of path through zero or more intermediate nodes".

That the result of TCLOSE has the same heading as its argument says nothing about the predicate of the result. Of course you can express a predicate to the effect 'there is a chain of nodes from X to Y' (or whatever are the attribute names).

The result has a FOPL predicate that strictly determines what can be a member of the set, but it does not and cannot have a FOPL predicate to generate the additional set members to make it a TC.

The function required to test that is intrinsically recursive or a results in a series.

A relvar/relation predicate is not a function; it's a membership condition; and it doesn't have to be testable by any 'definite procedure'. It merely has to be asserted by an authorised user making authorised data entry -- or as a logical consequence of relvar predicate(s) together with the logical connectives derived from the relational operations over those relvar(s).

Again, I'm talking FOPL predicates, which are functions. An authorised user might apply a predicate like 'stuff my granny knows' but that's not FOPL.

This is a point of difference with Datalog, in which TCLOSE can be expressed with no great difficulty.

If Datalog's TCLOSE produces the same answer as a D's for all possible input values; there is no difference in the FOPL predicate of the result. Unless you're going to get all wishy-washy metaphysical about same extension, different intension. I despair of anything you say getting so cogent as to be wishy-washy metaphysical.

Datalog is not FOPL. QED.

...

Sorry, I don't follow. The point of my exercise was to provide a formalism of the RA as the basis for incorporating it into some D.

Appendix A already does that. Codd 1972 already does that (up to a point). If your exercise has any sane point -- and I haven't seen one so far expressed cogently from you -- then it's going to be logically equivalent to those two sources. We can readily agree those two sources have some limitations/extensions left for the reader. You've failed so far to get the basics across; so any claim that you're covering the leftovers is so far null and void.

They do not. Codd omits formalisms for generating new values: all his values are literals. App-A omits formalisms for its relcons, TCLOSE and aggregation, all of which are part of the RA in TD.

Although I don't understand what you're trying to prove, I do know that you can't use a D as part of your proof. There are too many assumptions built into the shorthands of that language to know whether it proves anything.

>sigh< The abstract concepts expressed for a D in the TTM doco are not shorthands 'we do not prescribe syntax'. Tutorial D includes plenty of shorthands; they're expanded in Appendix A (and in various discussions in DTATRM); the semantics of the core operators is given in Appendix A. Yes the FORMAL DEFINITIONS give assumptions; they're more than adequate to prove how the A algebra works as a whole.

You wrote in a D, therefore you employed its specific syntax. App-A expands shorthands and provides (some) formalisms, so you should use A (not a D) if you want to prove something at the formal level. QED.

Quote from AntC on June 7, 2020, 1:51 am

Quote from dandl on June 7, 2020, 1:17 am

Quote from Erwin on June 6, 2020, 7:49 pm

Quote from dandl on June 6, 2020, 2:26 pm

Spot on. Relations in maths are just mappings between sets, and apply to all kinds of things. Database relations - as per Erwin.

All functions are relations - they map a key (the arguments) to a singular value. Any relation that does that is a function.

The relcons in App-A are of that form. The relcon PLUS with the predicate X+Y=Z maps the arguments (X,Y) to a singular value (Z) and therefore it is a function.

IMO this 'closes the loop'. Functions are relations and can be treated as such by the RA. Relcons are functions and can be formally defined in set-builder notation. Relcons can be implemented precisely because they are functions. And the RA operators that depend on them are within FOPL. Tidy.

You could add a formal definition of relcons to App-A in the same FOPL style, but not for TCLOSE and aggregation per OO Pre 6. That takes something extra.

Even for TCLOSE, it holds that the relations resulting from an invocation of it are (/can be seen as) a function mapping the (start-of-directed-path, end-of-directed-path) pairs to truth values. That the corresponding predicate is itself not expressible in FOPL, is rather orthogonal to the relation still being a function in the sense indicated.

Orthogonal? It's not at issue that the argument and result of TCLOSE are relations with the same heading, thus the same predicate.

Bzzzt. Relations with the same heading do not necessarily have the same predicate. We could wheel out the old Shops-and-Alarms example. We could note that the heading for S WHERE CITY = 'Leeds' is the same as for S; but their predicates are different. Therefore ...

No, I meant predicate in the strict sense of first order predicate logic. You cannot express transitive closure in first order predicate logic.

The need for TCLOSE shows precisely the limits of FOPL: there is no predicate for "start and end of path through zero or more intermediate nodes".

That the result of TCLOSE has the same heading as its argument says nothing about the predicate of the result. Of course you can express a predicate to the effect 'there is a chain of nodes from X to Y' (or whatever are the attribute names).

The result has a FOPL predicate that strictly determines what can be a member of the set, but it does not and cannot have a FOPL predicate to generate the additional set members to make it a TC.

The function required to test that is intrinsically recursive or a results in a series.

A relvar/relation predicate is not a function; it's a membership condition; and it doesn't have to be testable by any 'definite procedure'. It merely has to be asserted by an authorised user making authorised data entry -- or as a logical consequence of relvar predicate(s) together with the logical connectives derived from the relational operations over those relvar(s).

Again, I'm talking FOPL predicates, which are functions. An authorised user might apply a predicate like 'stuff my granny knows' but that's not FOPL.

This is a point of difference with Datalog, in which TCLOSE can be expressed with no great difficulty.

If Datalog's TCLOSE produces the same answer as a D's for all possible input values; there is no difference in the FOPL predicate of the result. Unless you're going to get all wishy-washy metaphysical about same extension, different intension. I despair of anything you say getting so cogent as to be wishy-washy metaphysical.

Datalog is not FOPL. QED.

...

Sorry, I don't follow. The point of my exercise was to provide a formalism of the RA as the basis for incorporating it into some D.

Appendix A already does that. Codd 1972 already does that (up to a point). If your exercise has any sane point -- and I haven't seen one so far expressed cogently from you -- then it's going to be logically equivalent to those two sources. We can readily agree those two sources have some limitations/extensions left for the reader. You've failed so far to get the basics across; so any claim that you're covering the leftovers is so far null and void.

They do not. Codd omits formalisms for generating new values: all his values are literals. App-A omits formalisms for its relcons, TCLOSE and aggregation, all of which are part of the RA in TD.

Although I don't understand what you're trying to prove, I do know that you can't use a D as part of your proof. There are too many assumptions built into the shorthands of that language to know whether it proves anything.

>sigh< The abstract concepts expressed for a D in the TTM doco are not shorthands 'we do not prescribe syntax'. Tutorial D includes plenty of shorthands; they're expanded in Appendix A (and in various discussions in DTATRM); the semantics of the core operators is given in Appendix A. Yes the FORMAL DEFINITIONS give assumptions; they're more than adequate to prove how the A algebra works as a whole.

You wrote in a D, therefore you employed its specific syntax. App-A expands shorthands and provides (some) formalisms, so you should use A (not a D) if you want to prove something at the formal level. QED.

Andl - A New Database Language - andl.org

#10 · June 8, 2020, 6:42 am

Quote from AntC on June 8, 2020, 6:42 am
I'm not going to dignify this nonsense with any sort of reply.

Quote from dandl on June 8, 2020, 12:46 am

Quote from AntC on June 7, 2020, 1:51 am

Quote from dandl on June 7, 2020, 1:17 am

Quote from Erwin on June 6, 2020, 7:49 pm

Quote from dandl on June 6, 2020, 2:26 pm

Spot on. Relations in maths are just mappings between sets, and apply to all kinds of things. Database relations - as per Erwin.

All functions are relations - they map a key (the arguments) to a singular value. Any relation that does that is a function.

The relcons in App-A are of that form. The relcon PLUS with the predicate X+Y=Z maps the arguments (X,Y) to a singular value (Z) and therefore it is a function.

IMO this 'closes the loop'. Functions are relations and can be treated as such by the RA. Relcons are functions and can be formally defined in set-builder notation. Relcons can be implemented precisely because they are functions. And the RA operators that depend on them are within FOPL. Tidy.

You could add a formal definition of relcons to App-A in the same FOPL style, but not for TCLOSE and aggregation per OO Pre 6. That takes something extra.

Even for TCLOSE, it holds that the relations resulting from an invocation of it are (/can be seen as) a function mapping the (start-of-directed-path, end-of-directed-path) pairs to truth values. That the corresponding predicate is itself not expressible in FOPL, is rather orthogonal to the relation still being a function in the sense indicated.

Orthogonal? It's not at issue that the argument and result of TCLOSE are relations with the same heading, thus the same predicate.

Bzzzt. Relations with the same heading do not necessarily have the same predicate. We could wheel out the old Shops-and-Alarms example. We could note that the heading for S WHERE CITY = 'Leeds' is the same as for S; but their predicates are different. Therefore ...

No, I meant predicate in the strict sense of first order predicate logic. You cannot express transitive closure in first order predicate logic.

The need for TCLOSE shows precisely the limits of FOPL: there is no predicate for "start and end of path through zero or more intermediate nodes".

That the result of TCLOSE has the same heading as its argument says nothing about the predicate of the result. Of course you can express a predicate to the effect 'there is a chain of nodes from X to Y' (or whatever are the attribute names).

The result has a FOPL predicate that strictly determines what can be a member of the set, but it does not and cannot have a FOPL predicate to generate the additional set members to make it a TC.

The function required to test that is intrinsically recursive or a results in a series.

A relvar/relation predicate is not a function; it's a membership condition; and it doesn't have to be testable by any 'definite procedure'. It merely has to be asserted by an authorised user making authorised data entry -- or as a logical consequence of relvar predicate(s) together with the logical connectives derived from the relational operations over those relvar(s).

Again, I'm talking FOPL predicates, which are functions. An authorised user might apply a predicate like 'stuff my granny knows' but that's not FOPL.

This is a point of difference with Datalog, in which TCLOSE can be expressed with no great difficulty.

If Datalog's TCLOSE produces the same answer as a D's for all possible input values; there is no difference in the FOPL predicate of the result. Unless you're going to get all wishy-washy metaphysical about same extension, different intension. I despair of anything you say getting so cogent as to be wishy-washy metaphysical.

Datalog is not FOPL. QED.

...

Sorry, I don't follow. The point of my exercise was to provide a formalism of the RA as the basis for incorporating it into some D.

Appendix A already does that. Codd 1972 already does that (up to a point). If your exercise has any sane point -- and I haven't seen one so far expressed cogently from you -- then it's going to be logically equivalent to those two sources. We can readily agree those two sources have some limitations/extensions left for the reader. You've failed so far to get the basics across; so any claim that you're covering the leftovers is so far null and void.

They do not. Codd omits formalisms for generating new values: all his values are literals. App-A omits formalisms for its relcons, TCLOSE and aggregation, all of which are part of the RA in TD.

Although I don't understand what you're trying to prove, I do know that you can't use a D as part of your proof. There are too many assumptions built into the shorthands of that language to know whether it proves anything.

>sigh< The abstract concepts expressed for a D in the TTM doco are not shorthands 'we do not prescribe syntax'. Tutorial D includes plenty of shorthands; they're expanded in Appendix A (and in various discussions in DTATRM); the semantics of the core operators is given in Appendix A. Yes the FORMAL DEFINITIONS give assumptions; they're more than adequate to prove how the A algebra works as a whole.

You wrote in a D, therefore you employed its specific syntax. App-A expands shorthands and provides (some) formalisms, so you should use A (not a D) if you want to prove something at the formal level. QED.

I'm not going to dignify this nonsense with any sort of reply.

Quote from dandl on June 8, 2020, 12:46 am

Quote from AntC on June 7, 2020, 1:51 am

Quote from dandl on June 7, 2020, 1:17 am

Quote from Erwin on June 6, 2020, 7:49 pm

Quote from dandl on June 6, 2020, 2:26 pm

Spot on. Relations in maths are just mappings between sets, and apply to all kinds of things. Database relations - as per Erwin.

All functions are relations - they map a key (the arguments) to a singular value. Any relation that does that is a function.

The relcons in App-A are of that form. The relcon PLUS with the predicate X+Y=Z maps the arguments (X,Y) to a singular value (Z) and therefore it is a function.

IMO this 'closes the loop'. Functions are relations and can be treated as such by the RA. Relcons are functions and can be formally defined in set-builder notation. Relcons can be implemented precisely because they are functions. And the RA operators that depend on them are within FOPL. Tidy.

You could add a formal definition of relcons to App-A in the same FOPL style, but not for TCLOSE and aggregation per OO Pre 6. That takes something extra.

Even for TCLOSE, it holds that the relations resulting from an invocation of it are (/can be seen as) a function mapping the (start-of-directed-path, end-of-directed-path) pairs to truth values. That the corresponding predicate is itself not expressible in FOPL, is rather orthogonal to the relation still being a function in the sense indicated.

Orthogonal? It's not at issue that the argument and result of TCLOSE are relations with the same heading, thus the same predicate.

Bzzzt. Relations with the same heading do not necessarily have the same predicate. We could wheel out the old Shops-and-Alarms example. We could note that the heading for S WHERE CITY = 'Leeds' is the same as for S; but their predicates are different. Therefore ...

No, I meant predicate in the strict sense of first order predicate logic. You cannot express transitive closure in first order predicate logic.

The need for TCLOSE shows precisely the limits of FOPL: there is no predicate for "start and end of path through zero or more intermediate nodes".

That the result of TCLOSE has the same heading as its argument says nothing about the predicate of the result. Of course you can express a predicate to the effect 'there is a chain of nodes from X to Y' (or whatever are the attribute names).

The result has a FOPL predicate that strictly determines what can be a member of the set, but it does not and cannot have a FOPL predicate to generate the additional set members to make it a TC.

The function required to test that is intrinsically recursive or a results in a series.

A relvar/relation predicate is not a function; it's a membership condition; and it doesn't have to be testable by any 'definite procedure'. It merely has to be asserted by an authorised user making authorised data entry -- or as a logical consequence of relvar predicate(s) together with the logical connectives derived from the relational operations over those relvar(s).

Again, I'm talking FOPL predicates, which are functions. An authorised user might apply a predicate like 'stuff my granny knows' but that's not FOPL.

This is a point of difference with Datalog, in which TCLOSE can be expressed with no great difficulty.

If Datalog's TCLOSE produces the same answer as a D's for all possible input values; there is no difference in the FOPL predicate of the result. Unless you're going to get all wishy-washy metaphysical about same extension, different intension. I despair of anything you say getting so cogent as to be wishy-washy metaphysical.

Datalog is not FOPL. QED.

...

Sorry, I don't follow. The point of my exercise was to provide a formalism of the RA as the basis for incorporating it into some D.

Appendix A already does that. Codd 1972 already does that (up to a point). If your exercise has any sane point -- and I haven't seen one so far expressed cogently from you -- then it's going to be logically equivalent to those two sources. We can readily agree those two sources have some limitations/extensions left for the reader. You've failed so far to get the basics across; so any claim that you're covering the leftovers is so far null and void.

They do not. Codd omits formalisms for generating new values: all his values are literals. App-A omits formalisms for its relcons, TCLOSE and aggregation, all of which are part of the RA in TD.

Although I don't understand what you're trying to prove, I do know that you can't use a D as part of your proof. There are too many assumptions built into the shorthands of that language to know whether it proves anything.

>sigh< The abstract concepts expressed for a D in the TTM doco are not shorthands 'we do not prescribe syntax'. Tutorial D includes plenty of shorthands; they're expanded in Appendix A (and in various discussions in DTATRM); the semantics of the core operators is given in Appendix A. Yes the FORMAL DEFINITIONS give assumptions; they're more than adequate to prove how the A algebra works as a whole.

You wrote in a D, therefore you employed its specific syntax. App-A expands shorthands and provides (some) formalisms, so you should use A (not a D) if you want to prove something at the formal level. QED.

TTM Forum

The Forum for Discussion about The Third Manifesto and Related Matters

Relcons and relfuns are both FOPL