6 ms·

Prolog and Logic Programming Historical Sources Archive

129 points by homarp 7y ago

triska 7y ago
Very interesting, thank you for sharing this! Knowing the history of Prolog can be very useful to make progress in this area, because quite often, progress in this area means returning to what earlier systems already did. For instance, already in the very first Prolog system, Marseille Prolog, a string like "hello" was treated as a list of characters, i.e., [h,e,l,l,o]. This was great for usability, as one would expect from a language that was designed for natural language processing. Later systems switched this to lists of character codes, denoting code points in the used encoding. For instance, when using ASCII or one of its supersets, "hello" would then mean [104,101,108,108,111], which is much less readable in answers. Still other systems introduced their own ad hoc types that were not lists and therefore could not be handled with Prolog's built-in mechanisms for reasoning about lists, most notably Definite Clause Grammars (DCGs), and thus even required their own dedicated and usually moded predicates for reasoning about them, thereby severely limiting their generality while increasing the complexity of application code. Only the most recent Prolog systems, such as Tau Prolog and Scryer Prolog, are now doing what Marseille Prolog did, namely treating strings as lists of characters, and are also beginning to combine this with efficient internal representations to finally get all advantages at once: usability, generality, simplicity and efficiency. Type checks are another example where Prolog systems are now going back to the solid foundations of Marseille Prolog, after decades of errands. For instance, to preserve monotonicity of Prolog programs, type checks must raise instantiation errors or delay the check if no decision can be made, e.g., the following would be a logically well-justified response because X can still become an integer: ?- integer(X). ERROR: Arguments are not sufficiently instantiated This is also what Marseille Prolog did, for very solid reasons that were very clearly outlined by Battani and Meloni. Prolog vendors soon found out that Prolog systems would sell better to customers who did not care about logical properties if such — to them strange and likely worrying — errors were not shown, and opted to instead answer such queries with silent failure, which is logically wrong and prevents for example declarative debugging techniques and different execution strategies such as iterative deepening: ?- integer(X). false. Now, logically sound type tests are appearing again in Prolog systems. For instance, Scryer Prolog already ships with library(si), where we have: ?- integer_si(X). caught: error(instantiation_error,functor/3) This is correct: We get an instantiation error, because no definite answer can be made at this point. X can become an integer, or a term that is not an integer, so answering either "yes" or "no" would not be appropriate, because the type of X cannot yet be determined. A third example for this are constraints like dif/2, which is a relation with very desirable logical properties, denoting syntactic disequality of terms, i.e., it is true if and only if its arguments are different, and it delays checks until a definite decision can be made. This was present even in the predecessor of Marseille Prolog, Prolog 0, and then treated at best as a strange curiosity or not present at all in many later systems before it became more widely available again. Using constraints also enables an even more elegant solution for the above cases. For instance, using CLP(ℤ), constraint logic programming over integers, we can constrain a variable to integers in the most general way: ?- X in inf..sup. X in inf..sup. Another very interesting aspect is the commercial context in which these systems were developed. There was a lot of money involved, Prolog vendors would give you a licence for thousands and tens of thousands of dollars, and still do today. Not that long ago, when you did a research project as a university student in cooperation with one of the Prolog vendors, the vendor would personally fly over and hand you a hardcopy of the system manual. Then, after you finished the project, the vendor would visit you again to take away the manual.
- 7thaccount 7y ago
  We often don't learn from the greats of computer science (all sorts of APL goodness from the 70s is being rediscovered for data science today). As far as modern Prolog. I know commercial systems still exist, but I assume most work has switched to SWI-Prolog?
  - falsissime 7y ago
    Do not forget SICStus, it´s jitter is truly excellent.
    - 7thaccount 7y ago
      Yeah, I've heard a bit about that one, but have lumped it into the commercial ones that you'd have to have a solid need to justify a license cost like running something important in production that requires support or you'd probably need an academic license.
      - falsissime 7y ago
        https://sicstus.sics.se/order4.html https://sicstus.sics.se/order4.html Includes an evaluation license (free) and a personal license for EUR 165.
        7thaccount 7y ago
        The personal license cannot be used for any commercial purposes (basically just academic research or play). The single-user commercial license is over $2000. Not that any of that is unreasonable in industry, but you're making it out to be cheaper than it is.
        falsissime 7y ago
        $2250 is the first year. Then $750 a year. This includes support. To my understanding, development alone without distribution falls under the personal license.
pmcjones 7y ago
Some background on the project: https://mcjones.org/dustydecks/archives/2020/03/18/1064/ https://mcjones.org/dustydecks/archives/2020/03/18/1064/
carapace 7y ago
Does anybody know where I can find the Mixtus partial evaluation system? It's mentioned all over the place (e.g. The Art of Prolog) but I haven't yet been able to locate the actual source. Any help would be greatly appreciated.
bobbane 7y ago
Did not see it mentioned in the article, but I believe Quintus Prolog was the base for Prolog on the Xerox Lisp machine line. They went to the effort of writing special microcode for the unifier, which meant the basically 16-bit 1100 series workstations were competitive in performance with other Prologs at the time.
verdverm 7y ago
I've been using https://cuelang.org https://cuelang.org, a new logical language. It's frickin awesome, logical + engineering = get things done We just released an initial dependency tool for Cuelang based on go mods https://github.com/hofstadter-io/mvs https://github.com/hofstadter-io/mvs
fizixer 7y ago
Rant alert: I've realized there is a big problem with logic programming: the two cultures of mathematical logic, and logic programming. In math logic, you learn propositional/sentential logic, then spend a lot of time with predicate/first-order logic. At this point, you can "return to mathematics" to do any math stuff imaginable under the sun. However, if you want to spend more time being a logician, you can delve into a wide variety of topics, second-order logics, constructive logic, model theory, proof theory, etc, etc, etc. Computer-science/logic-programmers on the other end? First they don't start with prop or pred logic. Absolutely zero building-from-the-ground up about how you could do computations using prop, then maybe move to more sophisticated stuff like pred logic. No, they will throw Hoare logic at you, and Horn clauses, and relational databases, and bound and free variables, and cuts, and what not. And if you complain, I guess you're just not cut out for logic programming. (I guess hardcore full-time mathematical logicians are not cut-out for that either, including Godel mind you). You think they'd stop there. I'm afraid not, far from it. Next they want you to spend all your time about learning about Church and Turing, and Curry-Howard correspondence, and to pretend like "real" logic started in 1933, and 1936, because anything before lambda-calculus is too inferior to be used in computers. Oh but wait, they're not done yet. Now they want you learning a brand new foundation of logic, math, and CS, that even mathematicians hardly need or use for 99% of their work. They want you to think in terms of type theory, and category theory. (So I guess when they say 'brand new foundation' they really mean 'brand new pair of foundations from which you can pick'). I'm starting to think there is something seriously wrong with the way logic is approached in theoretical CS, and logic programming. It's not minimal, and appears to serve as an elitist gatekeeping device, while mathematicians are going about their daily lives producing spectacular results with just prop+pred logic, and category theory has only started getting used in a tiny fraction of mathematical work.
- Twisol 7y ago
  You're right that it's hard. However, I think you're missing one significant point that, at least to some extent, justifies the hardness: computability. Systems like Prolog are based on the idea of "proof search": given a logical statement, find a proof of that statement. Humans do this all the time with classical logic, you might say -- but then, there are very famous statements expressible purely in first-order logic that nobody has found a proof of. This is anathema to computing! We want an "effective method", a "decision procedure", that allows us to compute for finite time and terminate with a positive (or negative!) proof. And we know, thanks to Gödel, that no such procedure exists for first-order logic: any decision procedure will miss proofs for some first-order statements. In order to give ourselves more options for proof search, we need to enrich our logics somehow. This enrichment usually comes in the form of restrictions relative to classical logic. For example, Horn clauses are a fragment of classical logic that we _can_ assign a reasonable decision procedure to -- of which the most basic is probably SLD resolution. But these restrictions traditionally sacrifice more power than we'd like, so we add various things back in, trading computational difficulty (but not decidability!) for expressivity. This is a significant source of complexity, no doubt! Computational logic is hard because we're asking more of it. Classical logic has been around since at least Aristotle, so it's perhaps no surprise that it's been refined into such a simple, well-understood form. Even then, I think if you traveled into various classical modal logics, you'd find those just as inscrutable at first as the logics we use in logic programming. > Hoare logic Mmh... For the most part, Hoare logic is back on the "for humans" side of things, as it's about verifying software rather than implementing software. It brings to bear the full power of classical logic(1), but since you're applying it to programs, most of which have incredibly non-monotonic semantics, you have to consider truth at each point in the program. Most of the machinery in Hoare logic over classical logic is about relating all of those points -- all of those worlds, in a model-theoretic sense. I personally find Hoare logic easier from a mathematical reasoning perspective than any of the logic systems designed for implementation. I think that makes sense, though, because Hoare logic is not about automation. (1) You can instantiate Hoare logic over any particular logical system, so you could apply it for automated verification, but I don't think that's the case the parent was considering.
Twisol 7y ago
I've been fascinated by concurrent constraint programming (CCP) for a few years now, but it's hard to find source code for any of the system from back then. My reference for most of this topic is Vijay Saraswat's monograph of the same name, and he mentions systems like "Concurrent Prolog", "GHC" (no relation to the Glasgow Haskell Compiler!), and most importantly for me, "Herbrand", the instantiation of CCP over the Herbrand term universe that Saraswat developed. If anyone is familiar with these topics, any pointers would be much appreciated!
kensai 7y ago
Is there for other languages as well? For example Functional?

129 points by homarp 7y ago

Very interesting, thank you for sharing this! Knowing the history of Prolog can be very useful to make progress in this area, because quite often, progress in this area means returning to what earlier systems already did. For instance, already in the very first Prolog system, Marseille Prolog, a string like "hello" was treated as a list of characters, i.e., [h,e,l,l,o]. This was great for usability, as one would expect from a language that was designed for natural language processing. Later systems switched this to lists of character codes, denoting code points in the used encoding. For instance, when using ASCII or one of its supersets, "hello" would then mean [104,101,108,108,111], which is much less readable in answers. Still other systems introduced their own ad hoc types that were not lists and therefore could not be handled with Prolog's built-in mechanisms for reasoning about lists, most notably Definite Clause Grammars (DCGs), and thus even required their own dedicated and usually moded predicates for reasoning about them, thereby severely limiting their generality while increasing the complexity of application code. Only the most recent Prolog systems, such as Tau Prolog and Scryer Prolog, are now doing what Marseille Prolog did, namely treating strings as lists of characters, and are also beginning to combine this with efficient internal representations to finally get all advantages at once: usability, generality, simplicity and efficiency. Type checks are another example where Prolog systems are now going back to the solid foundations of Marseille Prolog, after decades of errands. For instance, to preserve monotonicity of Prolog programs, type checks must raise instantiation errors or delay the check if no decision can be made, e.g., the following would be a logically well-justified response because X can still become an integer: ?- integer(X). ERROR: Arguments are not sufficiently instantiated This is also what Marseille Prolog did, for very solid reasons that were very clearly outlined by Battani and Meloni. Prolog vendors soon found out that Prolog systems would sell better to customers who did not care about logical properties if such — to them strange and likely worrying — errors were not shown, and opted to instead answer such queries with silent failure, which is logically wrong and prevents for example declarative debugging techniques and different execution strategies such as iterative deepening: ?- integer(X). false. Now, logically sound type tests are appearing again in Prolog systems. For instance, Scryer Prolog already ships with library(si), where we have: ?- integer_si(X). caught: error(instantiation_error,functor/3) This is correct: We get an instantiation error, because no definite answer can be made at this point. X can become an integer, or a term that is not an integer, so answering either "yes" or "no" would not be appropriate, because the type of X cannot yet be determined. A third example for this are constraints like dif/2, which is a relation with very desirable logical properties, denoting syntactic disequality of terms, i.e., it is true if and only if its arguments are different, and it delays checks until a definite decision can be made. This was present even in the predecessor of Marseille Prolog, Prolog 0, and then treated at best as a strange curiosity or not present at all in many later systems before it became more widely available again. Using constraints also enables an even more elegant solution for the above cases. For instance, using CLP(ℤ), constraint logic programming over integers, we can constrain a variable to integers in the most general way: ?- X in inf..sup. X in inf..sup. Another very interesting aspect is the commercial context in which these systems were developed. There was a lot of money involved, Prolog vendors would give you a licence for thousands and tens of thousands of dollars, and still do today. Not that long ago, when you did a research project as a university student in cooperation with one of the Prolog vendors, the vendor would personally fly over and hand you a hardcopy of the system manual. Then, after you finished the project, the vendor would visit you again to take away the manual.

7thaccount 7y ago
We often don't learn from the greats of computer science (all sorts of APL goodness from the 70s is being rediscovered for data science today). As far as modern Prolog. I know commercial systems still exist, but I assume most work has switched to SWI-Prolog?
- falsissime 7y ago
  Do not forget SICStus, it´s jitter is truly excellent.
  - 7thaccount 7y ago
    Yeah, I've heard a bit about that one, but have lumped it into the commercial ones that you'd have to have a solid need to justify a license cost like running something important in production that requires support or you'd probably need an academic license.
    - falsissime 7y ago
      https://sicstus.sics.se/order4.html https://sicstus.sics.se/order4.html Includes an evaluation license (free) and a personal license for EUR 165.
      - 7thaccount 7y ago
        The personal license cannot be used for any commercial purposes (basically just academic research or play). The single-user commercial license is over $2000. Not that any of that is unreasonable in industry, but you're making it out to be cheaper than it is.
        falsissime 7y ago
        $2250 is the first year. Then $750 a year. This includes support. To my understanding, development alone without distribution falls under the personal license.

pmcjones 7y ago

Some background on the project: https://mcjones.org/dustydecks/archives/2020/03/18/1064/ https://mcjones.org/dustydecks/archives/2020/03/18/1064/

carapace 7y ago

Does anybody know where I can find the Mixtus partial evaluation system? It's mentioned all over the place (e.g. The Art of Prolog) but I haven't yet been able to locate the actual source. Any help would be greatly appreciated.

bobbane 7y ago

Did not see it mentioned in the article, but I believe Quintus Prolog was the base for Prolog on the Xerox Lisp machine line. They went to the effort of writing special microcode for the unifier, which meant the basically 16-bit 1100 series workstations were competitive in performance with other Prologs at the time.

verdverm 7y ago

I've been using https://cuelang.org https://cuelang.org, a new logical language. It's frickin awesome, logical + engineering = get things done We just released an initial dependency tool for Cuelang based on go mods https://github.com/hofstadter-io/mvs https://github.com/hofstadter-io/mvs

fizixer 7y ago

Rant alert: I've realized there is a big problem with logic programming: the two cultures of mathematical logic, and logic programming. In math logic, you learn propositional/sentential logic, then spend a lot of time with predicate/first-order logic. At this point, you can "return to mathematics" to do any math stuff imaginable under the sun. However, if you want to spend more time being a logician, you can delve into a wide variety of topics, second-order logics, constructive logic, model theory, proof theory, etc, etc, etc. Computer-science/logic-programmers on the other end? First they don't start with prop or pred logic. Absolutely zero building-from-the-ground up about how you could do computations using prop, then maybe move to more sophisticated stuff like pred logic. No, they will throw Hoare logic at you, and Horn clauses, and relational databases, and bound and free variables, and cuts, and what not. And if you complain, I guess you're just not cut out for logic programming. (I guess hardcore full-time mathematical logicians are not cut-out for that either, including Godel mind you). You think they'd stop there. I'm afraid not, far from it. Next they want you to spend all your time about learning about Church and Turing, and Curry-Howard correspondence, and to pretend like "real" logic started in 1933, and 1936, because anything before lambda-calculus is too inferior to be used in computers. Oh but wait, they're not done yet. Now they want you learning a brand new foundation of logic, math, and CS, that even mathematicians hardly need or use for 99% of their work. They want you to think in terms of type theory, and category theory. (So I guess when they say 'brand new foundation' they really mean 'brand new pair of foundations from which you can pick'). I'm starting to think there is something seriously wrong with the way logic is approached in theoretical CS, and logic programming. It's not minimal, and appears to serve as an elitist gatekeeping device, while mathematicians are going about their daily lives producing spectacular results with just prop+pred logic, and category theory has only started getting used in a tiny fraction of mathematical work.

Twisol 7y ago
You're right that it's hard. However, I think you're missing one significant point that, at least to some extent, justifies the hardness: computability. Systems like Prolog are based on the idea of "proof search": given a logical statement, find a proof of that statement. Humans do this all the time with classical logic, you might say -- but then, there are very famous statements expressible purely in first-order logic that nobody has found a proof of. This is anathema to computing! We want an "effective method", a "decision procedure", that allows us to compute for finite time and terminate with a positive (or negative!) proof. And we know, thanks to Gödel, that no such procedure exists for first-order logic: any decision procedure will miss proofs for some first-order statements. In order to give ourselves more options for proof search, we need to enrich our logics somehow. This enrichment usually comes in the form of restrictions relative to classical logic. For example, Horn clauses are a fragment of classical logic that we _can_ assign a reasonable decision procedure to -- of which the most basic is probably SLD resolution. But these restrictions traditionally sacrifice more power than we'd like, so we add various things back in, trading computational difficulty (but not decidability!) for expressivity. This is a significant source of complexity, no doubt! Computational logic is hard because we're asking more of it. Classical logic has been around since at least Aristotle, so it's perhaps no surprise that it's been refined into such a simple, well-understood form. Even then, I think if you traveled into various classical modal logics, you'd find those just as inscrutable at first as the logics we use in logic programming. > Hoare logic Mmh... For the most part, Hoare logic is back on the "for humans" side of things, as it's about verifying software rather than implementing software. It brings to bear the full power of classical logic(1), but since you're applying it to programs, most of which have incredibly non-monotonic semantics, you have to consider truth at each point in the program. Most of the machinery in Hoare logic over classical logic is about relating all of those points -- all of those worlds, in a model-theoretic sense. I personally find Hoare logic easier from a mathematical reasoning perspective than any of the logic systems designed for implementation. I think that makes sense, though, because Hoare logic is not about automation. (1) You can instantiate Hoare logic over any particular logical system, so you could apply it for automated verification, but I don't think that's the case the parent was considering.

Twisol 7y ago

I've been fascinated by concurrent constraint programming (CCP) for a few years now, but it's hard to find source code for any of the system from back then. My reference for most of this topic is Vijay Saraswat's monograph of the same name, and he mentions systems like "Concurrent Prolog", "GHC" (no relation to the Glasgow Haskell Compiler!), and most importantly for me, "Herbrand", the instantiation of CCP over the Herbrand term universe that Saraswat developed. If anyone is familiar with these topics, any pointers would be much appreciated!

kensai 7y ago

Is there for other languages as well? For example Functional?