Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

The Power of Prolog

metalevel.at

Post reply on HN
Print view View original

71–80 of 164 posts

Re: The Power of Prolog

#71

Post by gtycomb »

saosebastiao wrote: post #64
fizixer wrote: post #2

Roughly half the 'power of prolog' comes from the 'power of logic programming' and prolog is by far not the only logic programming language, e.g., - You can do logic programming using minikanren in scheme. (you can also extend the minikanren system if you find a feature missing). - Minikanren was implemented in clojure and called core.logic. - It was also ported to python by Matthew Rocklin I think, called logpy. - T…

You forgot the most successful logic programming language to date: SQL.

Can SQL do resolution or backtracking similar to Prolog, I wonder.

Re: The Power of Prolog

#72

Post by kdtg »

lacampbell wrote: post #60

Can anyone give examples of the kinds of problems prolog is ideally suited to? I took a course on it at university. It looked interesting but I didn't really "get it". It might be worth another look now I have a bit more experience under my belt. I've got a lingering feeling it would solve a certain kind of problem very easily.

Intractable problems i.e., the ones that can't be solve in polynomial time. Logic programming in general is NP-Hard, so it's suitable for NP-Hard problems (constraint satisfaction problems, backtracking, etc). If you try to solve polynomial problems, it doesn't perform well.

Re: The Power of Prolog

#73

Post by ScottBurson »

fizixer wrote: post #45
est wrote: post #34

Earlier quoted context omitted.

what about this? https://github.com/Z3Prover/z3 Is it comparable with prolog or just a subset of prolog?

Disclaimer: My knowledge on this topic is not in depth (as I said, I'm still learning). I haven't heard of Z3 but it says it's a theorem prover, so it would be comparable to systems like Coq, Isabelle, which are also considered programming languages, and then compared to Agda, Idris, and, last but not the least, Haskell. So a distilled form of your question would be: - How does logic programming compare to pure funct…

> Coq, Isabelle are interactive theorem provers or proof assistants, not automatic theorem provers which is a lot harder to do

Automatic theorem provers for first-order logic (FOL) have existed for some time [0], but higher-order logic (HOL) is another matter. The difference is that in HOL, predicates can be variables; in FOL they are all constants. HOL allows you to write rules for mathematical induction; for example:

  ∀P P(0) ∧ (∀n n ≥ 0 ∧ P(n) ⇒ P(n + 1)) ⇒ (∀n n ≥ 0 ⇒ P(n))
This says that for any predicate P on the natural numbers, if you can show, first, that P(0), and second, that for any natural n, P(n) implies P(n + 1), then you can conclude that P is true for any n. This rule is not a valid FOL statement, because it starts off quantifying over possible predicates, which is not permitted in FOL.

Reasoning of this kind, although usually informal, is necessary for programmers to understand any iterative or recursive piece of code. To understand such code, you have to know what invariant it maintains; proofs of such invariants are always inductive. So HOL is required, in most cases, for formal verification of software.

But no one has figured out how to build an automated prover for HOL. My own theory as to why is simply that the branching factor is higher. It's like the difference between chess and Go: the branching factor -- the average number of possible moves from any board position -- is small enough in chess that brute-force search can be sufficient to play at a world level, at least in the mid- and end-game; but in Go, it's much larger, so that brute-force search doesn't get you very far.

As you say, lacking a fully automated HOL prover, people have been using proof assistants instead. These keep track of the details of the proof, which is still a very useful function, and can perform certain simple deductive steps themselves, but require manual intervention at certain critical points, such as the introduction of induction hypotheses.

[0] https://en.wikipedia.org/wiki/Automated_theorem_proving

Re: The Power of Prolog

#74

Post by zmonx »

dmh2000 wrote: post #69
nwatson wrote: post #53

The Japanese government spent US $400 million in the '80's (a lot in those days) to try to jump ahead of "western" computer technology via its "5th Generation Project". https://news.ycombinator.com/item?id=14047780 The basis for it all ... Prolog.

and it was an epic fail https://en.wikipedia.org/wiki/Fifth_generation_computer#Fail... A primary problem was the choice of concurrent logic programming as the bridge between the parallel computer architecture and the use of logic as a knowledge representation and problem solving language for AI applications.

Personal anecdote: I once asked a retired Japanese computer scientist why the 5th generation project had failed. He replied with:

"What do you mean 'failed'? All my colleagues who worked on this project have become professors!" In this respect, the project was actually a smashing success.

Re: The Power of Prolog

#76

Post by candiodari »

julian_1 wrote: post #68
Jtsummers wrote: post #13

Earlier quoted context omitted.

It was worse. That office had an aversion to anything not-Microsoft for dev tools unless they were for the embedded systems we maintained. They also had an aversion to any language that wasn't "industry standard", whatever that meant (because, clearly, prolog and others do have industry standards associated with them; here they meant commonly used and easy to hire for).

This is a frustration of mine. At university they try to install a knowledge of all kinds of crazy languages, before you're ready to appreciate their value and the issues they attempt to address. The most glaring example is probably teaching Haskell in first-year. As a working programmer, you're then corralled into following prescriptive industry-practice - that always errs on the side of dumbing down the choice of t…

You're being asked to be a consultant, you know. They want to pretend that if you rewrite Prolog in C#, it'll be simpler, and that the average C# programmer (the cheapest one they can hire) will simply understand (badly written) logic programming solvers and be able to modify them.

Eventually you'll figure out to simply double your hourly rate and ask "do you want a bad Haskell implementation to go with that as well ? How about SQL ? Lisp ?"

Don't forget to terminate with "by the way here's my card" (asking them to mention their personal referral code "ID10T") when the inevitable happens, nobody understands that code at all when they have to modify it. And every time they ask you to update it you increase your hourly rate 20%.

You know, management realism. You can be victimized by it, or you can make a living out of it.

Re: The Power of Prolog

#77

Post by tannhaeuser »

Karrot_Kream wrote: post #20
fizixer wrote: post #2

Roughly half the 'power of prolog' comes from the 'power of logic programming' and prolog is by far not the only logic programming language, e.g., - You can do logic programming using minikanren in scheme. (you can also extend the minikanren system if you find a feature missing). - Minikanren was implemented in clojure and called core.logic. - It was also ported to python by Matthew Rocklin I think, called logpy. - T…

Not really. I use SWI Prolog for a lot of personal projects (that actually see QPS no less) and there's a lot more to it than that. SWI gives you: good debugging support (with trace and spy), hooks into the Prolog database (with asserta/z and retract), optimized implementations of difference lists, online help, and so much more. Don't even get me started on its amazing DCG support that makes Regex feel like a Neolith…

And Prolog is actually an ISO-standardized language so you have a choice of implementations to choose from (for example Yap Prolog, which I found much faster than SWI last I checked, or the highly regarded commercial Sicstus Prolog). Plus, implementing a Prolog engine isn't too much of an effort to do on your own (like I did two times). In fact, there are multiple Prolog implementations for the JVM, for JavaScript, etc.

Re: The Power of Prolog

#78

Post by benjiweber »

gtycomb wrote: post #71
saosebastiao wrote: post #64

Earlier quoted context omitted.

You forgot the most successful logic programming language to date: SQL.

Can SQL do resolution or backtracking similar to Prolog, I wonder.

SQL gives you all the solutions to query by default unless you limit them right?

A relation (table) in SQL is conceptually a predicate that holds for all tuples (rows) therein. You can AND the predicates with "NATURAL JOIN". You can OR them with "UNION"

e.g. this example https://www.doc.gold.ac.uk/~mas02gw/prolog_tutorial/prologpa...

becomes something like this in SQL.

  example=# select * from red;
    item   
  ---------
   apple_1
   block_1
   car_27
  (3 rows)
  
  example=# select * from car;
     item    
  -----------
   desoto_48
   edsel_57
  (2 rows)
  
  example=# select * from blue;
     item   
  ----------
   flower_3
   glass_9
   honda_81
  (3 rows)
  
  example=# select * from bike;
     item   
  ----------
   iris_8
   my_bike
   honda_81
  (3 rows)
  
  example=# CREATE view fun as (select item from red NATURAL JOIN car) UNION (select item from blue NATURAL JOIN bike);
  CREATE VIEW
  
  example=# SELECT * FROM fun;
     item   
  ----------
   honda_81
  (1 row)

Re: The Power of Prolog

#79

Post by c-cube »

ScottBurson wrote: post #73
fizixer wrote: post #45

Earlier quoted context omitted.

Disclaimer: My knowledge on this topic is not in depth (as I said, I'm still learning). I haven't heard of Z3 but it says it's a theorem prover, so it would be comparable to systems like Coq, Isabelle, which are also considered programming languages, and then compared to Agda, Idris, and, last but not the least, Haskell. So a distilled form of your question would be: - How does logic programming compare to pure funct…

> Coq, Isabelle are interactive theorem provers or proof assistants, not automatic theorem provers which is a lot harder to do Automatic theorem provers for first-order logic (FOL) have existed for some time [0], but higher-order logic (HOL) is another matter. The difference is that in HOL, predicates can be variables; in FOL they are all constants. HOL allows you to write rules for mathematical induction; for exampl…

There are some automated theorem provers for higher-order logic [0][1], but they are not very good yet compared to their first-order counterpart. There are also some provers specialized in inductive proofs [2][3], although the frontier with proof assistants such as Coq or Isabelle starts getting blurry as you often need the user's intervention to explicitely provide lemmas.

I have some hopes that this is going to change in the next few years thanks to a colleague's effort [4] to build better higher-order provers. He's an expert in Sledgehammer (a tool to use automated provers from Isabelle) which is already a productivity boost, and should become better with this project.

You are right that the search space is more difficult to handle. Induction (and similar formulas) is particularly hard to handle because one usually has to introduce lemmas, and these lemmas have to be "guessed" (infinite branching factor there). Existing provers basically rely on heuristics to try and find lemmas that would be useful for solving the current goal(s). ACL2 [3] for instance uses heuristics accumulated and refined for decades.

Hopefully, proof assistants will get tighter and tighter integration with automated provers, and the user will have to specify only the main lemmas and the overall shape of a proof, leaving the details to CPU crunching.

[0] https://page.mi.fu-berlin.de/cbenzmueller/leo/ [1] https://www.ps.uni-saarland.de/~cebrown/satallax/ [2] https://github.com/sorinica/spike-prover [3] https://www.cs.utexas.edu/users/moore/acl2/ [4] http://matryoshka.gforge.inria.fr/

Re: The Power of Prolog

#80

Post by c-cube »

skdotdan wrote: post #75

Something I would like to be able to understand/know/study is how logic programming languages are implemented and how their runtime looks like.

you can start by looking for "warren abstract machine" (usually shortened as WAM). It's an intermediate format for compiling prolog programs (sets of Horn clauses, that is, rules). It makes every operation very explicit, including unification (to match the current goal against each rule's conclusion) and backtracking (to enumerate solutions; this involves stacks, unsurprisingly). I think most state of the art prolog implementations are then able to compile this format to native code. Of course prolog also requires that the runtime has a GC (to collect dead terms) and that it can dynamically add/remove rules, use reflection to observe the shape of a term, etc.

https://en.wikipedia.org/wiki/XSB is an implementation to which Warren contributes, with additional features such as tabling (a powerful form of memoization that avoids many infinite recursions).

Post reply on HN