TTM without tuples
Quote from AntC on July 1, 2021, 10:18 pm"My meaning of [xxx] may be different to yours, and maybe other people's" comes straight from Humpty Dumpty.Actually it comes straight from computing. The computing profession is notorious for not coming to an agreement on standard terminology, and is a contrast to many of the well-established sciences and engineering subjects, who once a new topic is researched, tend towards standardised phraseology as an aid to communication. (If you write a computing paper for publication, you typically have to define your terms to ensure the reader knows what you mean in the paper by word 'XXX', even when 'XXX' is a well-known term).
So I tried to explain what I meant by coercion, which for me is a much more general concept than what typically is the case in specific programming languages.
Absolutely. Anyone who insists that their definition of X is right while mine is wrong is just asking to start a religion war.
I don't personally find coercion a useful term, perhaps because (a) developers tend not to agree on what it means (b) the meaning has shifted over time (c) the (current) definition does not capture anything useful enough to stand in its own right.
FWIW I tend to use cast for conversions that preserve bits over meaning; conversion for those that preserve meaning over bits; coercion for those the compiler snuck in; and add words like explicit and widening as needed. It works for me.
Quote from David Livingstone on July 1, 2021, 7:06 pmThank you for the responses to my posting.
The Third Manifesto provides essentially 2 things. Firstly a formal logical model (expressed as a set of prescriptions, and a set of proscriptions). Secondly a syntax for expressing things in terms of that model. The model is about relations and databases, and usually called the TTM model. The syntax is called Tutorial D. Date & Darwen's books make clear that other syntaxes than Tutorial D could be devised to express and use the TTM model. (In my case, RAQUEL is just another such syntax. I'd like to have a graphical version of it, which would then be yet another syntax).
Date & Darwen also make clear that the TTM model is nothing to do with how it is physically implemented; it's a purely logical model.
My intent in my contribution was to consider solely the TTM logical model - not any syntax, and not any physical implementation. I'm sorry if I’ve not made that very clear.
Because a logical model is an abstract thing, we always need some form of syntax to express the abstract logical model in a concrete form, that we can write down and then read. So Date & Darwen created Tutorial D to make sure they had a syntax that they could use to precisely express their TTM model.
We tend to think about the abstract model in terms of the syntax because psychologically it's difficult not to. But in the long run we need to learn to distinguish the two.
Now the question of tuples and attributes. Here is an analogy of what I'm trying to get at. When I think of a human being, I think of a creature consisting of a head, body, left arm, right arm, left leg and right leg. I need the concepts of arms, legs, etc in order to understand the concept of a human being. I don't mean that it’s possible to see a lone leg (left or right) walking down the street on its own, or a head rolling along on its own, or ... . Arms and legs are necessary to understand human beings, but do not exist independently of human beings.
Likewise a relation consists of attributes and tuples, but I don’t expect attributes and tuples to appear ON THEIR OWN in a relational database. Even if I were to use TTM model relations as part of a general purpose programming language, I don’t want attributes and tuples to appear ON THEIR OWN in that programming language.
When I agree with dandl, that’s all I’m getting at. Of course the logical consequence is that all operators, etc, etc whose purpose is to support the existence of tuples INDEPENDENTLY OF relations need not appear ON THEIR OWN.
Since the concepts of attributes and tuples are integral to the concept of relations (at least TTM model relations) then the Tutorial D syntax used to express the TTM model MUST include the means to express attributes and tuples. Such syntax is especially useful if you want to refer to some particular attribute or tuple in a relation, or to create a relation value from component attribute or tuple values.
This post and your earlier one make some thoughtful assumptions. But regarding one of them, TTM does not provide "a formal logical model". If it did, it would be easy to settle the argument in Appendix E of DTATRM between the two authors.
Appendix A says that a relation has a heading and a conforming set of tuples.
This requirement is easy to express formally in propositional form or in quantified form as a model constraint, for example in propositional form as a conjunction of four entailments:
(A∧B→C)∧(A∨B→C)∧(¬(A∨B)→C)∧(¬(A∧B)→C).
A, B and C can name many different propositions, for example, suppose A and B name sets of tuples and C names the set union of the headings of A and B.
One of the tautologies the constraint entails is:
(A∧B→C)∧(A∨B→C)∧(¬(A∨B)→C)∧(¬(A∧B)→C)
→
(A∧B∧C→(A∨B⇔A∧B)).
When read as a logical argument, the first line of the overall entailment is a premise and the third line is a conclusion. The argument is logically valid.
Note the rather important logical equivalence in the conclusion. Also note that this argument becomes invalid when its conclusion and premise are reversed.
C could name many other things, for example the proposition that an IMS segment has records named A and B or it could name the set intersection of common attributes. Regardless, many tautologies can be expressed.
The many possible propositions named by C show why even when much of Codd's papers from 1970 to 1972 is misunderstood and ignored, the very first sentence of the 1970 paper still applies to any dbms that claims to be relational. For example, to allow the Appendix A definition mentioned above, a dbms must support the above model constraint or a logical equivalent, for example such that (A∧B∧C) is understood as an internal representation and (A∧B) as an external one. But the internal dbms, data correctness scope is both representations.
For some purposes, that particular model constraint isn't even needed, provided an argument uses external and internal representations independently. For example,
(A∧B∧C)→¬(A∧B)→(A∧B∧¬C)
Is a tautology in its own right. It is important because it applies to some of the examples in Appendix E. In fact when it is understood as an argument the entailment connectives in this expression can be replaced by equivalence connectives:
(A∧B∧C)↔¬(A∧B)↔(A∧B∧¬C).
When defining such model constraints or their support for some particular data management feature, a useful question dbms designers and data designers might ask is " when or under what conditions is A∨B→A∧B∧C true? ".
A simple quantified version of the argument (A∧B∧C)→¬(A∧B)→(A∧B∧¬C) is:
∃a((Pa∧Qb∧Ca)↔¬(Pa∧Qb)↔(Pa∧Qb∧¬Ca)),
which shows three relations in predicate form, two of them sharing a common attribute named 'a'. Codd's 1972 union-compatible and relative complement requirements apply to the join factor (Pa∧¬Ca) of the complex join (Pa∧Qb∧¬Ca).
Now expand the quantified tautology to assert that the extension of Ca is a subset of Pa's extension. The expansion:
∃a((Pa∧Qb∧Ca)↔¬(Pa∧Qb)↔(Pa∧Qb∧¬Ca)∧(Ca→Pa))
is also a tautology.
By contrast the attempt to expand by asserting that the extension of Pa is a subset of Ca's:
∃a((Pa∧Qb∧Ca)↔¬(Pa∧Qb)↔(Pa∧Qb∧¬Ca)∧(Pa→Ca)),
is an invalid argument and therefore not a tautology. The reason appears to be that first-order predicate logic can't deduce proper supersets from negated subsets. But this doesn't matter to Codd's model and algebra.
Note the above tautologies have no need for primary keys. Other ones with other constraints are needed for that requirement.
Far beyond the efficiency of formal logic for settling certain TTM missunderstandings, it is remarkable that supposed relational language compilers are dedicated to external end-user representations. It should be obvious from the above that a dbms that supports the relations between internal and external representations requires a different sublanguage compiler than that used by end-users. Proving automatically the logical validity of predicate relations by accessing only the definitions of predicate extensions that Codd's finite model requires is an insignificant machine cost compared to all the IO needed for evaluating the extensions themselves.
It should also be fairly clear that his finite model has the potentially great advantage of being able to exploit Godel's completeness theorem which states for example that systems based on first order logic which are limited in that they don't count (don't do arithmetic) are capable of self-proving both of completeness and consistency. By "applied predicate calculus" Codd didn't mean any old application, rather he meant a limited application, limited to the 1970-1972 requirements. This doesn't prevent requiring a coexistent Turing model, it just means that the data language implementation must be logically independent.
Quote from David Livingstone on July 1, 2021, 7:06 pmThank you for the responses to my posting.
The Third Manifesto provides essentially 2 things. Firstly a formal logical model (expressed as a set of prescriptions, and a set of proscriptions). Secondly a syntax for expressing things in terms of that model. The model is about relations and databases, and usually called the TTM model. The syntax is called Tutorial D. Date & Darwen's books make clear that other syntaxes than Tutorial D could be devised to express and use the TTM model. (In my case, RAQUEL is just another such syntax. I'd like to have a graphical version of it, which would then be yet another syntax).
Date & Darwen also make clear that the TTM model is nothing to do with how it is physically implemented; it's a purely logical model.
My intent in my contribution was to consider solely the TTM logical model - not any syntax, and not any physical implementation. I'm sorry if I’ve not made that very clear.
Because a logical model is an abstract thing, we always need some form of syntax to express the abstract logical model in a concrete form, that we can write down and then read. So Date & Darwen created Tutorial D to make sure they had a syntax that they could use to precisely express their TTM model.
We tend to think about the abstract model in terms of the syntax because psychologically it's difficult not to. But in the long run we need to learn to distinguish the two.
Now the question of tuples and attributes. Here is an analogy of what I'm trying to get at. When I think of a human being, I think of a creature consisting of a head, body, left arm, right arm, left leg and right leg. I need the concepts of arms, legs, etc in order to understand the concept of a human being. I don't mean that it’s possible to see a lone leg (left or right) walking down the street on its own, or a head rolling along on its own, or ... . Arms and legs are necessary to understand human beings, but do not exist independently of human beings.
Likewise a relation consists of attributes and tuples, but I don’t expect attributes and tuples to appear ON THEIR OWN in a relational database. Even if I were to use TTM model relations as part of a general purpose programming language, I don’t want attributes and tuples to appear ON THEIR OWN in that programming language.
When I agree with dandl, that’s all I’m getting at. Of course the logical consequence is that all operators, etc, etc whose purpose is to support the existence of tuples INDEPENDENTLY OF relations need not appear ON THEIR OWN.
Since the concepts of attributes and tuples are integral to the concept of relations (at least TTM model relations) then the Tutorial D syntax used to express the TTM model MUST include the means to express attributes and tuples. Such syntax is especially useful if you want to refer to some particular attribute or tuple in a relation, or to create a relation value from component attribute or tuple values.
Quote from p c on July 12, 2021, 1:12 amQuote from David Livingstone on July 1, 2021, 7:06 pmThank you for the responses to my posting.
The Third Manifesto provides essentially 2 things. Firstly a formal logical model (expressed as a set of prescriptions, and a set of proscriptions). Secondly a syntax for expressing things in terms of that model. The model is about relations and databases, and usually called the TTM model. The syntax is called Tutorial D. Date & Darwen's books make clear that other syntaxes than Tutorial D could be devised to express and use the TTM model. (In my case, RAQUEL is just another such syntax. I'd like to have a graphical version of it, which would then be yet another syntax).
...
This post and your earlier one make some thoughtful assumptions. But regarding one of them, TTM does not provide "a formal logical model". If it did, it would be easy to settle the argument in Appendix E of DTATRM between the two authors.
Would it? How?
Do you propose that a formal logical model would include views?
Do you have such a model?
Far beyond the efficiency of formal logic for settling certain TTM missunderstandings, it is remarkable that supposed relational language compilers are dedicated to external end-user representations. It should be obvious from the above that a dbms that supports the relations between internal and external representations requires a different sublanguage compiler than that used by end-users. Proving automatically the logical validity of predicate relations by accessing only the definitions of predicate extensions that Codd's finite model requires is an insignificant machine cost compared to all the IO needed for evaluating the extensions themselves.
Although it's not clear how you got here, I do agree. The surface language (in which user queries and updates are expressed) is insufficiently powerful to manage how they should be implemented or executed. Indeed, given a suitable internal sub-language, the view updating problem disappears. Simply use the ISL to specify how.
It should also be fairly clear that his finite model has the potentially great advantage of being able to exploit Godel's completeness theorem which states for example that systems based on first order logic which are limited in that they don't count (don't do arithmetic) are capable of self-proving both of completeness and consistency. By "applied predicate calculus" Codd didn't mean any old application, rather he meant a limited application, limited to the 1970-1972 requirements. This doesn't prevent requiring a coexistent Turing model, it just means that the data language implementation must be logically independent.
Again, I agree. The query language should not be Turing complete, in the interests of query rewriting and optimisation. It can include things that Codd's did not, like extend and aggregate but it's probably an open question whether it should include fixed point recursion, like TCLOSE and SQL.
Quote from p c on July 12, 2021, 1:12 amThis post and your earlier one make some thoughtful assumptions. But regarding one of them, TTM does not provide "a formal logical model". If it did, it would be easy to settle the argument in Appendix E of DTATRM between the two authors.
I take your point, especially if you're thinking of (say) predicate calculus as the kind of logic in question. I think Date and Darwen consider TTM as a formal logical model, but only express it informally, via the their prescriptions and proscriptions.
I think it is hard to express a useful relational model like TTM with the mathematical rigour that a mathematician demands, while at the same time making it intelligible to the majority of computer programmers and software designers. At least, I've found it so. I wrote a mathematical spec of RAQUEL using Z Schema Calculus (the only formal method I've learnt properly). But I found that to make it more generally meaningful, I had to omit some of the basic stuff from the Z spec, which meant it wasn't really rigorous. (It also meant I could avoid using some complicated software tools to write the maths !). Even then, for every assertion I wrote mathematically, I added a translation in English to say what it meant, so that it would be (hopefully) helpful to anyone who read it. It also meant that I didn't, and couldn't, do any proofs to demonstrate that the model was internally consistent, which is essential for a mathematician. So while I think the model is consistent (and writing it out helped me find a few bugs), I haven't proved it and so can't be certain. I doubt I'm enough of a mathematician to do satisfactory proofs anyway.
Quote from dandl on July 12, 2021, 4:20 amDo you propose that a formal logical model would include views?
From past published papers, and the difference in opinions between Date and Darwen, it seems to me that there is not yet any general agreement regarding view UPDATING, even conceptually. Without that, I don't think it worth trying to define views in their entirety in a formal logical model.
It seems to me that if you want to include the automatic derivation of view update assignments from view definitions - so that the former derivations can be included in the formal model - then it is only possible if the functions (i.e. relational algebra operators) used in view definitions are all inverse functions (i.e. you can operate them in both directions, so to speak). This is only possible if the functions/operators are injective. Alas, most relational algebra operators are not inverse.
I think this is the root cause of Darwen's, and others', valid objections to Date's proposals. In effect, a valid update depends in general on the design of a view's underlying relvar(s) as well as the relational formalism. Design uses the formalism, rather than being part of it. To be fair to Date, he does propose that the designs of underlying relvar(s) be completely tied down with integrity constraints, so that then a formal derivation of update assignment(s) could be derived from a view definition expression. I don't know if there is a proof of this.
Quote from David Livingstone on July 12, 2021, 5:35 pmQuote from dandl on July 12, 2021, 4:20 amDo you propose that a formal logical model would include views?
From past published papers, and the difference in opinions between Date and Darwen, it seems to me that there is not yet any general agreement regarding view UPDATING, even conceptually. Without that, I don't think it worth trying to define views in their entirety in a formal logical model.
It seems to me that if you want to include the automatic derivation of view update assignments from view definitions - so that the former derivations can be included in the formal model - then it is only possible if the functions (i.e. relational algebra operators) used in view definitions are all inverse functions (i.e. you can operate them in both directions, so to speak). This is only possible if the functions/operators are injective. Alas, most relational algebra operators are not inverse.
I think this is the root cause of Darwen's, and others', valid objections to Date's proposals. In effect, a valid update depends in general on the design of a view's underlying relvar(s) as well as the relational formalism. Design uses the formalism, rather than being part of it. To be fair to Date, he does propose that the designs of underlying relvar(s) be completely tied down with integrity constraints, so that then a formal derivation of update assignment(s) could be derived from a view definition expression. I don't know if there is a proof of this.
That wasn't my question. I want to know:
- Would a formal logical model include views?
- Do you have such a model you can show us?
- How would that resolve the problem of view updating?
IMO views are a kind of query expession, expressed as a WFF, not part of the underlying model. View updating is relational assignment, in which WFFs are evaluated and assigned to one or more relvars. The task of constructing those WFFs falls to the user/developer and cannot in general be derived mechanically from the logical model. Please confirm or refute.
Quote from dandl on July 14, 2021, 12:38 amQuote from David Livingstone on July 12, 2021, 5:35 pmQuote from dandl on July 12, 2021, 4:20 amDo you propose that a formal logical model would include views?
From past published papers, and the difference in opinions between Date and Darwen, it seems to me that there is not yet any general agreement regarding view UPDATING, even conceptually. Without that, I don't think it worth trying to define views in their entirety in a formal logical model.
It seems to me that if you want to include the automatic derivation of view update assignments from view definitions - so that the former derivations can be included in the formal model - then it is only possible if the functions (i.e. relational algebra operators) used in view definitions are all inverse functions (i.e. you can operate them in both directions, so to speak). This is only possible if the functions/operators are injective. Alas, most relational algebra operators are not inverse.
I think this is the root cause of Darwen's, and others', valid objections to Date's proposals. In effect, a valid update depends in general on the design of a view's underlying relvar(s) as well as the relational formalism. Design uses the formalism, rather than being part of it. To be fair to Date, he does propose that the designs of underlying relvar(s) be completely tied down with integrity constraints, so that then a formal derivation of update assignment(s) could be derived from a view definition expression. I don't know if there is a proof of this.
That wasn't my question. I want to know:
- Would a formal logical model include views?
A model that includes view updating presumably would. In the absence of view updating, views are just relational expressions.
- Do you have such a model you can show us?
I think David's comment, that "... there is not yet any general agreement regarding view UPDATING, even conceptually. Without that, I don't think it worth trying to define views in their entirety in a formal logical model," is a reasonable summary. There are some models of view updating (Date's, for example -- see https://www.amazon.co.uk/View-Updating-Relational-Theory-C-J/dp/1449357849) but no general agreement that it's a useful/reasonable/needful feature, let alone agreement on how to automatically do it.
Quote from David Livingstone on July 12, 2021, 5:35 pmQuote from dandl on July 12, 2021, 4:20 amDo you propose that a formal logical model would include views?
From past published papers, and the difference in opinions between Date and Darwen, it seems to me that there is not yet any general agreement regarding view UPDATING, even conceptually. Without that, I don't think it worth trying to define views in their entirety in a formal logical model.
It seems to me that if you want to include the automatic derivation of view update assignments from view definitions - so that the former derivations can be included in the formal model - then it is only possible if the functions (i.e. relational algebra operators) used in view definitions are all inverse functions (i.e. you can operate them in both directions, so to speak). This is only possible if the functions/operators are injective. Alas, most relational algebra operators are not inverse.
I think this is the root cause of Darwen's, and others', valid objections to Date's proposals. In effect, a valid update depends in general on the design of a view's underlying relvar(s) as well as the relational formalism. Design uses the formalism, rather than being part of it. To be fair to Date, he does propose that the designs of underlying relvar(s) be completely tied down with integrity constraints, so that then a formal derivation of update assignment(s) could be derived from a view definition expression. I don't know if there is a proof of this.
Quote from p c on July 14, 2021, 2:15 pmQuote from David Livingstone on July 12, 2021, 5:35 pmQuote from dandl on July 12, 2021, 4:20 amDo you propose that a formal logical model would include views?
From past published papers, and the difference in opinions between Date and Darwen, it seems to me that there is not yet any general agreement regarding view UPDATING, even conceptually. Without that, I don't think it worth trying to define views in their entirety in a formal logical model.
It seems to me that if you want to include the automatic derivation of view update assignments from view definitions - so that the former derivations can be included in the formal model - then it is only possible if the functions (i.e. relational algebra operators) used in view definitions are all inverse functions (i.e. you can operate them in both directions, so to speak). This is only possible if the functions/operators are injective. Alas, most relational algebra operators are not inverse.
I think this is the root cause of Darwen's, and others', valid objections to Date's proposals. In effect, a valid update depends in general on the design of a view's underlying relvar(s) as well as the relational formalism. Design uses the formalism, rather than being part of it. To be fair to Date, he does propose that the designs of underlying relvar(s) be completely tied down with integrity constraints, so that then a formal derivation of update assignment(s) could be derived from a view definition expression. I don't know if there is a proof of this.
Actually, it appears that Appendix E bases its arguments on propositional logic. This can be done but it's tricky. It requires introducing logically independent relations. This is needed to make it explicit which relations are involved in an expression. It's also one of the reasons why the appendix is so long when it doesn't need to be.
Take the open shop /set alarm conjunction negation argument which for some unknown reason is premised on just one relation when at least three are involved. Apparently, TTM coders presume the same. It encourages a mentality that asks questions such as "Would it? How? Do you propose that a formal logical model would include views? Do you have such a model?". Some questions have no practical answer without regurgitating all of history.
The open shop set alarm example conclusions are completely invalidated by just two lines of predicate logic:
∀x(¬(Ax1∧Ax2))↔(¬∃x(Ax1∧Ax2)) is logically valid,
But ∀x(¬(Ax1∧Ax2))↔(¬∃x(Ax1)) is invalid.
Re union/disjunction, ∀x(¬(Ax1∨Ax2))↔(¬∃x(Ax1∧Ax2)) is invalid, but
∀x(¬(Ax1∨Ax2))↔(¬∃x(Ax1∨Ax2)) is valid.
But ∀x(¬(Ax1∨Ax2))→(¬∃x(Ax1∧Ax2)) is valid.
Why is such a proof program not embedded in every compiler that calls itself relational?
For what purpose?
Tutorial D is relational and its Rel compiler requires no such thing.
Quote from p c on July 14, 2021, 2:15 pmQuote from David Livingstone on July 12, 2021, 5:35 pmQuote from dandl on July 12, 2021, 4:20 amDo you propose that a formal logical model would include views?
From past published papers, and the difference in opinions between Date and Darwen, it seems to me that there is not yet any general agreement regarding view UPDATING, even conceptually. Without that, I don't think it worth trying to define views in their entirety in a formal logical model.
It seems to me that if you want to include the automatic derivation of view update assignments from view definitions - so that the former derivations can be included in the formal model - then it is only possible if the functions (i.e. relational algebra operators) used in view definitions are all inverse functions (i.e. you can operate them in both directions, so to speak). This is only possible if the functions/operators are injective. Alas, most relational algebra operators are not inverse.
I think this is the root cause of Darwen's, and others', valid objections to Date's proposals. In effect, a valid update depends in general on the design of a view's underlying relvar(s) as well as the relational formalism. Design uses the formalism, rather than being part of it. To be fair to Date, he does propose that the designs of underlying relvar(s) be completely tied down with integrity constraints, so that then a formal derivation of update assignment(s) could be derived from a view definition expression. I don't know if there is a proof of this.
Actually, it appears that Appendix E bases its arguments on propositional logic. This can be done but it's tricky. It requires introducing logically independent relations. This is needed to make it explicit which relations are involved in an expression. It's also one of the reasons why the appendix is so long when it doesn't need to be.
Take the open shop /set alarm conjunction negation argument which for some unknown reason is premised on just one relation representation when at least three are involved.
Shop-and-alarm is deliberately a minimal example to illustrate the point. The 'rules of the game' are that there must be a view to update through; there must be at least one based-on relvar; for demonstration purposes, Darwen's response stipulates two based-ons. I can see no match-up from what you say to Appendix E. Please give some specific references.
Apparently, TTM coders presume the same.
Again I see no evidence for your claim. Please give a reference. How do you know what "TTM coders presume"? Come to that, who/what is a "TTM coder"? You mean somebody who codes in Tutorial D? AFAICT that's only two people on the planet.
It encourages a mentality that asks questions such as "Would it? How? Do you propose that a formal logical model would include views? Do you have such a model?". Some questions have no practical answer without regurgitating all of history.
Again empty, unsubstantiated claims.
The open shop set alarm example conclusions are completely invalidated by just two lines of predicate logic:
∀x(¬(Ax1∧Ax2))↔(¬∃x(Ax1∧Ax2)) is logically valid,
But ∀x(¬(Ax1∧Ax2))↔(¬∃x(Ax1)) is invalid.
Re union/disjunction, ∀x(¬(Ax1∨Ax2))↔(¬∃x(Ax1∧Ax2)) is invalid, but
∀x(¬(Ax1∨Ax2))↔(¬∃x(Ax1∨Ax2)) is valid.
But ∀x(¬(Ax1∨Ax2))→(¬∃x(Ax1∧Ax2)) is valid.
Why is such a proof program not embedded in every compiler that calls itself relational?
Do you have any evidence they aren't? Do you have any evidence for anything you claim? Or do you just make up waffle out of thin air?
I expect optimising transformations to a query that a DBMS applies are based on predicate-logic equivalences, whether or not the DBMS vendor explicitly consults inferences. Optimisations are far more likely to be driven from uniqueness (keys) and inclusion dependencies (foreign keys) than logic-chopping negations and existentials.