Uniqueness of Dum (R00)
Quote from AntC on July 26, 2019, 6:28 am
Most of SQL syntax looks odd by any programming language standards.
As I pointed out a while back, it has common roots with Cobol, which is still one of the most widespread programming languages in actual use, as opposed to fashion.
Quoted identifiers must be one of the more stupid bits of SQL syntax
Quoted identifiers in the Lisp tradition go back for more than 50 years, and in the database world at least back to CODASYL DML in 1971. The use of phrases as Real World identifiers is of course as old as language: we kludge around our inability to use New York as an identifier by using New_York, NewYork, or something else, and compared to "New York" (SQL's form) these alternatives are no beauties.
IMO this is mostly a matter of implementer laziness: somehow the designers and implementers of Fortran and Algol managed to allow phrasal identifiers without even marking them specially, though with a few complementary uglinesses: in Fortran you need to quote OR, AND, and the equality and ordering operators (symbolic equivalents weren't generally available a the time),and in Algol keywords must either be quoted or else delimited with spaces. Another well-known use of phrasal identifiers is in electronic hardware design, and indeed if you google "escaped identifiers" you mostly find references to Verilog.
Much the same might be said of case-sensitivity and reserved words: they make life easier for implementers, not for users.
Quote from johnwcowan on July 26, 2019, 3:38 pmQuote from AntC on July 26, 2019, 6:28 amMost of SQL syntax looks odd by any programming language standards.
As I pointed out a while back, it has common roots with Cobol, which is still one of the most widespread programming languages in actual use, as opposed to fashion.
COBOL programmer of 30+ years standing here. Most of COBOL syntax has always looked odd to me. I have never got used to it. Even though I could spot a missing full stop on line 1,320 of a 6,000-line program.
Quoted identifiers must be one of the more stupid bits of SQL syntax
Quoted identifiers in the Lisp tradition go back for more than 50 years,
Hang on, hang on. LISP QUOTE is not the same thing. That's where you're treating code as data, in order to manipulate the code in a macro before executing it. Neither COBOL nor SQL (nor ALGOL) does that.
and in the database world at least back to CODASYL DML in 1971. The use of phrases as Real World identifiers is of course as old as language: we kludge around our inability to use New York as an identifier by using New_York, NewYork, or something else, and compared to "New York" (SQL's form) these alternatives are no beauties.
IMO this is mostly a matter of implementer laziness: somehow the designers and implementers of Fortran and Algol managed to allow phrasal identifiers without even marking them specially, though with a few complementary uglinesses: in Fortran you need to quote OR, AND, and the equality and ordering operators (symbolic equivalents weren't generally available a the time),and in Algol keywords must either be quoted or else delimited with spaces.
KDF-9 ALGOL programmer here: that was one of the few implementations that tried sticking very close to the 1960 Language report and actually had single symbols for reserved words, that were printed on the Flexowriter underlined. Oh yes! this was bleeding-edge technology. The implementors were very proud of their work (as I was told at length by a very nerdy grey-haired lady at NPL Teddington). It was the users who hated it, because entering code at the teletype/line editor was an enormous pain.
Sorry John, I think you're just plain wrong.
Another well-known use of phrasal identifiers is in electronic hardware design, and indeed if you google "escaped identifiers" you mostly find references to Verilog.
Much the same might be said of case-sensitivity and reserved words: they make life easier for implementers, not for users.
Again I disagree. Computer languages are not like natural languages -- that is, do not have remotely relatable semantics. That's why it's utterly pointless to put a verb MOVE in COBOL. As a user, I want reserved words, and I don't care two hoots for language implementors.
Quote from AntC on July 26, 2019, 4:07 pmQuoted identifiers must be one of the more stupid bits of SQL syntax
Quoted identifiers in the Lisp tradition go back for more than 50 years,
Hang on, hang on. LISP
QUOTEis not the same thing. That's where you're treating code as data, in order to manipulate the code in a macro before executing it. Neither COBOL nor SQL (nor ALGOL) does that.
Not what I'm talking about. Quoted identifiers are marked by vertical bars at each end, |like this|; alternatively, individually disallowed characters can be quoted with \ (or / in pre-Common-Lisp varieties), like\ this. I'm not sure exactly when in the continuous development of Maclisp these features were introduced (sometime between 1965 and 1979, when Zetalisp split off). I do know they are less popular than they once were, but by no means extinct. Scheme didn't have them in the standard (though commonly implemented anyway) until quite recently.
That's why it's utterly pointless to put a verb MOVE in COBOL.
APL doesn't even have IF or WHILE, so it's a continuum, and where you prefer to be is entirely a matter of taste.
Quote from AntC on July 26, 2019, 6:28 amA couple of remarks on QBQL syntax. Like David B, I find it highly counter-intuitive. So I'm making these remarks to help explain in advance of responding to another post from Vadim which purports to show some sort of 'proof' in QBQL. I've no idea whether that's proving something that agrees with what I'm trying to do, or disproves it.
Of course Vadim is entitled to use whatever syntax he chooses in his own notation. But if you're trying to explain something on a TTM forum you need to use the lingua franca here -- either Tutorial D or A algebra. Or include a great deal of explanation how QBQL notation corresponds.
QBQL initial purpose was to be a complimentary tool to Prover9/Mace4. To move the code effortlessly between the tools it should comply with the established system. This is why syntax with heavy algebraic emphasis.
Hmm. I'd prefer to say QBQL is untyped. If you want to use String types, how do I include a space/tab/newline character inside a value? AFAICT space is significant as a attribute-value delimiter, and newline is significant as a tuple delimiter. Oh but then semicolon delimits the end of something(?)
QBQL is a research tool. The quirks how to represent Irish names, or even phrases with spaces are trivialities, that IMO were not worth spending 5 minute time solving. The field of database systems is pretty crowded to add yet another competitor.
I certainly do ask if
"p=q"means the same as[p=q]. If "p=q" is 'just a name', what does the embedded equal sign mean? If it's not denoting an equi-relation then please don't put an equal sign.
They are the same. Initially it was [p=q], but then I decided that "p=q" syntax is more natural. You are right, the fact that QBQL engine gives a special treatment to double quoted literals with equality sign is confusing.
I'm stuck with non-stop thunderstorms outside; and threats of a typhoon. So I've caught up on Vadim's request earlier in this thread to edit out some lapsed quotes on another thread.
On the uniqueness of R00; or rather, on the properties of R00 that we need in terms of lattice meet/join to validate the claim that Roo corresponds to DUM, here's some stuff I was unable to prove -- that is to get Prover9 to prove. I can't remember exactly which stuff I failed to prove for which choices of axioms, so let's just say this is stuff R00 must satisfy in order to have a workable axiomatised model of relations. Take this list as a program of work to prove the lattice algebra correctly implements Appendix A's model of relations. Note none of these are quasi-equational, so presumably Litak et al is not interested in them, and that's why they're getting such weak results within their quasi-equational straitjacket -- as is revealed more in their 2015 paper that has been conceded previously:
* R00 != R01. That is: DUM is distinct from DEE.
For any workable set of relation values, we need to embed counterparts to logical True, False. Then lattice meet ≡ NaturalJOIN implements logical AND; lattice join ≡ InnerUnion implements logical OR; DEE NOTMATCHING x implements logical NOT x. So any set of values that claims to model relations must have at least two distinct values; and one must model True, one False. We don't have a workable NOTMATCHING (because it's defined in terms of R00, which isn't unique).
* forall x [(x NatJOIN R00 != x) EQUIV (x InnerUnion R00 = R01)]
Gloss: relation x being non-empty can be expressed in two ways: emptified x not equal x; x InnerUnion DUM is Dee. Notice the corollary of that, viz: relation x being empty can be expressed in two ways: emptified x = x; x InnerUnion DUM is DUM *is* a theorem, but only because this is inferrable from the lattice axioms:
* forall z forall x [(x NatJoin z = x) EQUIV (x InnerUnion z = z)]
Substituting R00 for z in there is not telling us anything about R00. This is a symptom of R00's definitions (so far) being unable to fix R00.
* forall x [(x NatJoin R00 = R00) EQUIV (x = R00 OR x = R01)]
There's a stronger form of that (which is uglier to express, so I'll do it in English): for any two relations, their NatJOIN being DUM is equivalent to either one or both being DUM, and the other being DEE (i.e. if it's not DUM).
This seems like it's a special property of DUM; but no: we could substitute any constant q in place of R00; then all this is requiring is that DUM/R00/q be displacement 1/along a single edge in the lattice from DEE. I.e. there is no relation 'between' DEE and DUM/R00/q. Again this is a symptom of R00's definitions (so far) being unable to fix R00.
OK I could just make all of the above axioms. I could add in Litak et al's two axioms mentioning R00 (their H). Does that give R00 all the needed properties? No! We don't get
* distributivity of NatJOIN over InnerUnion; and distributivity of InnerUnion over NatJOIN; for
* both combs of all three relations same heading; and all three relations empty.
The Litak axioms get us some of those, but not all.
Quote from johnwcowan on August 5, 2019, 1:36 pmQuote from AntC on August 5, 2019, 1:32 pmOn the uniqueness of R00; or rather, on the properties of R00 that we need in terms of lattice meet/join to validate the claim that Roo corresponds to DUM
I like the idea of referring to R00 as "Roo".
Where's Kanga?
Quote from AntC on August 5, 2019, 1:32 pmI'm stuck with non-stop thunderstorms outside; and threats of a typhoon. So I've caught up on Vadim's request earlier in this thread to edit out some lapsed quotes on another thread.
The thread become little tidier now, thank you. Still it is stuck on misunderstanding what was achieved there [if anything]. And there were just too many objections to try to explain them all. For example, why uniqueness of R00 matters [in that context]? We just take some equalities, and juggle them getting some other identities. Those are perfectly valid algebraic transformations.
Presumably, I would have lessen the confusion if I started with the operation "relation squared" right from the beginning of the thread...
Take this list as a program of work to prove the lattice algebra correctly implements Appendix A's model of relations. Note none of these are quasi-equational, so presumably Litak et al is not interested in them, and that's why they're getting such weak results within their quasi-equational straitjacket -- as is revealed more in their 2015 paper that has been conceded previously:
* R00 != R01. That is: DUM is distinct from DEE.
It is not derivable from the relational lattice axioms. In the universe [database] consisting of a single relation, it would be both R00 and R01. Such universe consisting of one very lonely relation is vacuous, of course, but this is besides the point.
For any workable set of relation values, we need to embed counterparts to logical True, False. Then lattice meet ≡ NaturalJOIN implements logical AND; lattice join ≡ InnerUnion implements logical OR; DEE NOTMATCHING x implements logical NOT x. So any set of values that claims to model relations must have at least two distinct values; and one must model True, one False. We don't have a workable NOTMATCHING (because it's defined in terms of R00, which isn't unique).
* forall x [(x NatJOIN R00 != x) EQUIV (x InnerUnion R00 = R01)]
The latex is right there, supported on the forum. I understand, this is not a peer reviewed publication, but if you make some effort, you'll draw satisfaction from neatly written formulas.
Am I correctly understanding that you proposed the above as an axiom with the goal to derive
R_{00} \neq R_{01}
from it?
Gloss: relation x being non-empty can be expressed in two ways: emptified x not equal x; x InnerUnion DUM is Dee. Notice the corollary of that, viz: relation x being empty can be expressed in two ways: emptified x = x; x InnerUnion DUM is DUM *is* a theorem, but only because this is inferrable from the lattice axioms:
* forall z forall x [(x NatJoin z = x) EQUIV (x InnerUnion z = z)]
Substituting R00 for z in there is not telling us anything about R00. This is a symptom of R00's definitions (so far) being unable to fix R00.
* forall x [(x NatJoin R00 = R00) EQUIV (x = R00 OR x = R01)]
There's a stronger form of that (which is uglier to express, so I'll do it in English): for any two relations, their NatJOIN being DUM is equivalent to either one or both being DUM, and the other being DEE (i.e. if it's not DUM).
Are you trying to assert that there is no other relations in the lattice interval between R00 and R01?
This has been discussed at page 10 of Relational Lattice foundation for Algebraic Logic
This seems like it's a special property of DUM; but no: we could substitute any constant q in place of R00; then all this is requiring is that DUM/R00/q be displacement 1/along a single edge in the lattice from DEE. I.e. there is no relation 'between' DEE and DUM/R00/q. Again this is a symptom of R00's definitions (so far) being unable to fix R00.
OK I could just make all of the above axioms. I could add in Litak et al's two axioms mentioning R00 (their H). Does that give R00 all the needed properties? No! We don't get
* distributivity of NatJOIN over InnerUnion; and distributivity of InnerUnion over NatJOIN; for
* both combs of all three relations same heading; and all three relations empty.
The Litak axioms get us some of those, but not all.
The fact that their axiom system is not quite complete is quite easy to establish. Just combine all the axioms and find a counterexample for distributivity law. It exhibits the model
^ : | 0 1 2 3 4 5 6 7 8 ---+------------------ 0 | 0 5 2 3 0 5 2 3 5 1 | 5 1 5 5 1 5 1 1 1 2 | 2 5 2 5 2 5 2 5 5 3 | 3 5 5 3 3 5 5 3 5 4 | 0 1 2 3 4 5 6 7 8 5 | 5 5 5 5 5 5 5 5 5 6 | 2 1 2 5 6 5 6 8 8 7 | 3 1 5 3 7 5 8 7 8 8 | 5 1 5 5 8 5 8 8 8 v : | 0 1 2 3 4 5 6 7 8 ---+------------------ 0 | 0 4 0 0 4 0 4 4 4 1 | 4 1 6 7 4 1 6 7 8 2 | 0 6 2 0 4 2 6 4 6 3 | 0 7 0 3 4 3 4 7 7 4 | 4 4 4 4 4 4 4 4 4 5 | 0 1 2 3 4 5 6 7 8 6 | 4 6 6 4 4 6 6 4 6 7 | 4 7 4 7 4 7 4 7 7 8 | 4 8 6 7 4 8 6 7 8 R00 : 0
[p q] a b
[p q] a b c d
Quote from johnwcowan on August 5, 2019, 2:23 pmQuote from dandl on August 5, 2019, 2:12 pmWhere's Kanga?
I suppose you could apply that name to R01, but roo (lower case) is a shortening of kangaroo used in Australia.
You don't say. I thought they were all called Skippy (unless they're boomers or joeys of course).