]>
Lambda the Ultimate - Comments
http://lambda-the-ultimate.org
CommentsenParts of SQL in Codd's "original" RA, part 2
http://lambda-the-ultimate.org/node/5440#comment-94524
<blockquote>
What language are SQL stored procedures in?
</blockquote>
Typically SQL or SQL/PSM, PL/SQL, etc. An SProc could be as simple as a SELECT statement(with parameters).
<blockquote>
Although PSM is defined I don't know any two databases with compatible implementations, so therefore PSM seems a failed part of the standard, ...
</blockquote>
PL/SQL and similar have been around for a long time. We're talking about expressive power, so it doesn't matter whether different vendors implement the standard in different ways. It takes SQL beyond FOL.
<blockquote>
Personally I think PSM is a mistake,
</blockquote>
I agree. I've already said as much. You go on to repeat the observations I already made.
<blockquote>
... this does not mean that SQLs relational part is based on higher order logic.
</blockquote>
My message specifically asked what part you define as "SQL's relational part". And what you mean by "Codd's original RA".
Mon, 26 Jun 2017 06:46:32 +0000AntCWhat would be involved in moving logic beyond FOL?Clarifications
http://lambda-the-ultimate.org/node/5440#comment-94523
The comments about recursion have nothing to do with linear recursion. Recursion does not make a language higher-order.
However, the scare quotes around "Turing complete" were a hint that I was playing fast and loose with terminology. For a start, FOL is a logic not a computational model, so the term does not directly apply. What I meant was that the theorems of FOL are only semidecidable and so already require a Turing machine to compute. I was sloppy though, as this does not imply that FOL has the same expressive power as a universal TM, and it does not. For instance you need to add some axiom of induction (either second order or a first-order axiom schema) to FOL to represent arithmetic over the natural numbers, which famously (Gödel) makes FOL incomplete (edit: or inconsistent).Mon, 26 Jun 2017 06:27:01 +0000Neil MaddenWhat would be involved in moving logic beyond FOL?What language?
http://lambda-the-ultimate.org/node/5440#comment-94522
What language are SQL stored procedures in? SQL does not define say 'Java' as part of the SQL standard. Although PSM is defined I don't know any two databases with compatible implementations, so therefore PSM seems a failed part of the standard, seeing as most of ANSI SQL is usable across multiple database.
Personally I think PSM is a mistake, as the whole point of relational algebra is to specify the operations without explicit iteration, so the database query engine can optimise the query, and is free to change the storage format based on usage statistics.
The other point is that made elsewhere that higher order logic is not the same as a higher order function. So even if we admit PSM permits higher order functions, this does not mean that SQLs relational part is based on higher order logic. As this topic was about logic, you had to pick up which definition of "higher order" was being used from the context. Mon, 26 Jun 2017 05:36:24 +0000Keean SchupkeWhat would be involved in moving logic beyond FOL?Parts of SQL in Codd's "original" RA
http://lambda-the-ultimate.org/node/5440#comment-94521
Keean, you've not defined which parts of SQL you restrict yourself to. Neither have you defined which set of RA operators you count as "original". (Do you include RENAME, although Codd omitted it? Do you include relation-to-relation comparisons, like is-subset-of or is-empty? Do you include the <i>G</i> group-by operator? Presumably you don't include recursive CTEs?)
So I find your claims unsubstantiated so far.
<blockquote>
Stored procedures are not part of SQL, ...
</blockquote>
Maybe you don't use SProcs or the other procedural programming features, but if they're "not part of SQL", what are they? And why does the SQL standard spend so many pages specifying them?
For recursive CTEs, evaluating them to obtain the 'output' relation needs iterating (or recursing) the self-referencing disjunct until no further tuples are produced. That seems to me to be quantifying over that disjunct (a relation expression, so second-order quantification).
On recursion, I'm still researching Neil's (rather alarming) claims. Neil's remarks seem to be limited to a specific form of recursion (linear). And yet he also claims FOL is "Turing complete" (his scare quotes: what do they mean?).
I can't reconcile that claim: Turing complete includes expressing multiple recursion. As I understand it, you can express the Ackermann function (I mean the Peter & Robinson variant) in a Turing-complete algebra, but not in FOL.Mon, 26 Jun 2017 04:39:20 +0000AntCWhat would be involved in moving logic beyond FOL?SEQUEL
http://lambda-the-ultimate.org/node/5426#comment-94520
SEQUEL was a general purpose *programming language* whose the first applications happened to be in the area of application of the LF. There wasn't much overlap between the design of the LF and SEQUEL.
Post '90s, most programming in SEQUEL's successors, Qi and Shen, has not been in the area of application of the LF.
"The Book of Shen" is not expensive and the barriers to comprehension are no steeper than the pay walls around many academic journals. The free online materials on the site would inform even the most casual observer of what the group is doing and the news group is always there to provide information.
In fact at least one member of the Racket mailing list seemed to be aware of the Shen project right from the outset.
<a>https://lists.racket-lang.org/users/archive/2012-January/049829.html</a>
You'll also find discussion of Shen in the Racket IRC.
MarkSun, 25 Jun 2017 11:19:45 +0000Mark TarverType Systems as MacrosUnderstanding
http://lambda-the-ultimate.org/node/5440#comment-94519
I find my understanding of relational algebra is similar to yours. Stored procedures are not part of SQL, so as far as I know there is no way to quantify over relations in SQL, so it is first order. There are recursive queries, but there can be recursive statements in FOL too I think (if you think how you can have recursion in Prolog, which does not have functions, and is first order).Sat, 24 Jun 2017 15:53:41 +0000Keean SchupkeWhat would be involved in moving logic beyond FOL?Transitive closure and FOL
http://lambda-the-ultimate.org/node/5440#comment-94518
For the record, I was careful not to say that FOL can express transitive closure. The correct statement of TC requires expressing "the smallest set such that...". This is inherently a second-order statement, and cannot be correctly stated in FOL (or SQL). The fact that you can compute transitive closure in SQL (and Datalog) is due to the minimal model semantics of those languages: that is, a *restriction* they place on the FOL semantics to achieve decidability. This restriction doesn't make them second-order languages. Sat, 24 Jun 2017 15:11:15 +0000Neil MaddenWhat would be involved in moving logic beyond FOL?What do you mean that FOL is
http://lambda-the-ultimate.org/node/5440#comment-94517
What do you mean that FOL is decidable? The question of whether a given proposition is provable is undecidable. Sat, 24 Jun 2017 13:47:45 +0000Matt MWhat would be involved in moving logic beyond FOL?Well, if you are going to be
http://lambda-the-ultimate.org/node/5440#comment-94516
Well, if you are going to be rude I am not going to continue debating with you. I suggest you find a better reference on the expressivity and semantics of FOL than wikipedia. Sat, 24 Jun 2017 12:23:08 +0000Neil MaddenWhat would be involved in moving logic beyond FOL?Appear to not understand FOL
http://lambda-the-ultimate.org/node/5440#comment-94515
@Neil, I disagree with all of your claims. Are you trolling?
Do you have reference? Even wikipedia (on FOL) disagrees with you.
Yes, FOL is decidable, which is why it's a Good Thing. A Turing complete system is not decidable: you might note Turing developed the abstraction precisely to arrive at an answer for the Entscheidungsproblem -- that is, a negative answer.
Codd developed the Relational Calculus, and then the Relational Algebra as 'executable' counterparts to FOL interpreted into the Relational Model.
Explain to me how you express transitive closure or an aggregate like SUM(r, a) in FOL.
Wikipedia on Transitive closure: "The transitive closure of a binary relation cannot, in general, be expressed in first-order logic (FO)."Sat, 24 Jun 2017 11:49:44 +0000AntCWhat would be involved in moving logic beyond FOL?They are the same orders
http://lambda-the-ultimate.org/node/5440#comment-94514
They are the same orders. Functions are just a particular type of relation. First-order languages only allow variables to range over individuals in the domain of discourse, while second-order allows variables to range over sets of individuals, and so on. You may be able to axiomatise some higher-order function theories in a first-order logic (I'd like to see), but that is not the same thing (proof theory vs semantics): those functions are still higher-order because their arguments denote functions, which are themselves sets (of sets ...) of (tuples of) individuals. Sat, 24 Jun 2017 06:41:29 +0000Neil MaddenWhat would be involved in moving logic beyond FOL?I can only respond from a
http://lambda-the-ultimate.org/node/5440#comment-94513
I can only respond from a phone this weekend so I'll keep it short. I agree logic is syntax + semantics. But when someone talks about FOL or SOL I assume they're talking about the formal system. However you make these definitions, the idea that we can't use FOL as a formal system because it can pin down the naturals seems wrong. It can prove all the same things that SOL can. ZFC uses FOL. Sat, 24 Jun 2017 04:56:12 +0000Matt MWhat would be involved in moving logic beyond FOL?HIgher order vs higher order
http://lambda-the-ultimate.org/node/5440#comment-94512
I'm not sure second-/higher-order logic has anything to do with higher-order functions—those "orders" are about different things.
Typed higher-order functions can be expressed using ML polymorphism. I'm no FOL expert, but I think at least in the usual foundations (FOL + set theory) they're no problem.
If you want to go beyond ML polymorphism, there's System F. Also called second order lambda calculus, and arising from second-order arithmetic minus dependent types. (Source: Proof and types, J.Y. Girard, Chapter 15. Might be one of the easiest chapters in that book to skim, still not easy).Sat, 24 Jun 2017 01:31:14 +0000BlaisorbladeWhat would be involved in moving logic beyond FOL?behavior
http://lambda-the-ultimate.org/node/5442#comment-94511
"Why don't you use existing debug info to get that format meta data?", Dex asked.<br> "Two reasons," Wil explained. "First, it's not debug info: it must be there all the time, without being stripped. I need it to work even if folks try to kill all debug info for a build. Second, there's no method table in existing debug info, which is the interesting part. I would not bother posting about just format debug info."<br> "I ignored you when you said method table," Dex confessed. "It sounded like Smalltalk BS. What does that mean? You want everything to have a vtable?"<br> "In effect, yes," Wil nodded. "You might only use it when something dynamic or interpreted runs, either in debugging or testing; but every C value would be a polymorphic object when it lives in space allocated by a vat. Even native types."<br> "Now you sound like a lunatic," Dex warned. "What kind of vtable? Something more like C++, or more like what a dynamic language uses?"<br> "More like the latter," Wil said, "which would require a dynamic runtime in some scripting to dispatch. I guess I'd start with an AST interpreter using Lisp syntax but Smalltalk message passing semantics. An easy lesson for my sons: here's how you parse, and here's a way to interpret. It would only be crazy the AST uses refcounted nodes."<br> "I hate that crap," Dex admitted sourly. "If you like C, why not stick with it?"<br> "I could always compile a script to C, if I like it enough to keep and use more heavily," Wil said. "But making stuff up as you go along is harder in C, and more dangerous, and not nearly interactive enough for what I want. I hope to demonstrate the state of internal data structures in the middle of a suspended algorithm to my sons. And when writing new things wholesale, this approach makes bottom-up construction easier, since you can see what happens when you put together components like tinker toys."Fri, 23 Jun 2017 23:08:27 +0000Rys McCuskerC runtime type info gimmick which supports scriptingI might get the
http://lambda-the-ultimate.org/node/5440#comment-94510
I might get the confusion—if so, the point is subtle. The original question was:
>> What do you mean it doesn't have a proof theory?
You say:
> The important distinction between first order and second order is therefore about semantics, whereas the difference between FOL and SOL as logics is just syntax.
I think if you change the semantics without getting a matching proof syntax, you don't have a (good) proof theory, at least for logicians that prefer FOL. Logics is defined by having matching syntax and semantics—hence SOL is a perfectly good thing but isn't logics, just set theory.
I agree with the first part:
> The important distinction between first order and second order is therefore about semantics
but the second part is not true in the right sense:
> whereas the difference between FOL and SOL as logics is just syntax.
The problem is that FOL as logics is the combination of "first order (semantics)" + first order syntax; similarly, SOL as a logics is second order semantics + second order syntax. You can encode that syntax into the syntax of first-order logics, and I trust you that the proof still works, but the encoding is not sound enough (because it doesn't impose the extra restrictions on the models).
I'm no logician, but I understand logics is about having matching syntax and semantics. If you drop that requirement, the word "logic" becomes void of meaning. When people build program logics (often on top of some existing semantics), they build a proof theory matching some model theory, so that you can reason within the proof theory of the logic without needing extra assumptions about models. If you can't, you don't have a (good) proof theory. And that's annoying. Compare using Hoare logic, where you reason directly on programs, against reasoning in some complicated model using crazy mathematics we don't get—say bfagh theory. Let's say that Hoare logics is proven sound using bfagh theory. If its proof theory is complete, we can forget about bfaghs and stick to the proof theory. (This argument appears often in papers about program logics for FOO).
Again, using an embedding of syntax that doesn't respect semantics is not doing logics.
After explaining this, maybe I get why Gödel results are claimed to mean that the reduction of mathematics to logics (as Gödel wanted) has failed. By the above discussion and Gödel, we can't study natural numbers purely via proof theory, because it's not complete—we *have* to move to model theory. That is, we can't study naturals within the boundaries of logic. It also follows that FOL is a perfectly good logics, but for classes of models of limited interest — hence we use set theory.
Or we follow a different school and use intuitionistic logics (where we also reject completeness).
The same way, you could also go to a category theorist, give him an isomorphism between the objects of two categories that doesn't preserve the arrows, and claim the categories are isomorphic as categories, it's just the arrows that don't match. That's more clearly false — but even once you fix the terminology and do something interesting with this isomorphism, you still aren't doing category theory.Fri, 23 Jun 2017 21:41:15 +0000BlaisorbladeWhat would be involved in moving logic beyond FOL?