Hacker News Reader

As a long-time user of Prolog I didn't find the explanation so horrible. Unification is indeed like variable assignment in the constraint-satisfaction sense: bindings are not stateful. As for equality, I believe the author meant == rather than =, or more accurately the 'is' operator in Python and Perl. But maybe regular expression matching would be a better analog for Prolog's theorem proving.

Your statement 2==1+1 is (I'd claim) a weird case in Prolog. Unless you want to code the Peano postulates you need some way to do numerical calculations, and "2 is 1+1" does indeed work in the body of a clause.

Your mathematical explanation of Prolog's theorem proving is precise and correct but almost impenetrable to the average software engineer trying to "get" Prolog. Such explanations only make sense once someone already mostly understands what's going on, and hence aren't useful for beginners. As a first approximation I thought the OP's work wasn't bad.

The simplest way to test equality between two arithmetic expressions in Prolog in a syntax that anyone familiar with imperative programming languages will be comfortable with is to use =:=/2, like this:

  ?- 2 =:= 1+1.
  true.

Prolog has a few different predicates to test (dis-) equality, (non-) equivalence, (non-) unification, subsumption and so forth, and most of them (but not all) use the "=" symbol in some combination, so it's easy for a novice (or an advanced user) to get twisted into knots trying to figure out what exactly each should be used for. My strong intuition is that stating that unification is "like testing equality" will only help to confuse matters further.

The same goes for "simple" explanations that completely miss the point. Logic programming and Prolog are not simple subjects. That's not by design: theorem proving is bloody hard by nature and making a first-order logic language run on a digital computer is even bloody harder. First-order logic is undecidable in the general case and we must jump through hoops constantly to stick to the special cases where a theorem can be proved automatically and the proof procedure is sound and complete, or at least sound. Without an understanding of this fundamental difficulty in automated theorem proving, Prolog does not make sense, in the long run. For example- why those weird Horn clauses? Why not arbitrary clauses? Why depth-first search? Why unification? And so on.

It is certainly possible to learn Prolog incrementally, without first having to digest, I don't know, the proof of the Subsumption Theorem. But every small step in the way must be taken on firm ground, else the student loses her footing and falls down bottomless pits of despair. I know this from first-hand experience and there is even some scholarship on the trouble that university students get in with Prolog because they form the wrong mental models for it. Let me see if I can locate it online.

Yep, here it is:

What's wrong? Understanding beginners' problems with Prolog

https://link.springer.com/article/10.1007/BF00116441

I'm quoting a bit of the abstract:

  The problems that underlie these and other errors seem to be (a) the
  complexity of the Prolog primitives (unification and backtracking) and (b)
  the misfit between students' naive solutions to a problem and the constructs
  that are available in Prolog (e.g. iterative solutions do not map easily to
  recursive programs). This suggests that learning Prolog could be helped by
  (1) coherent and detailed instruction about how Prolog works, (2) emphasis
  on finding recursive solutions that do not rely on primitives such as
  assignment and (3) instruction in programming techniques that allow students
  to implement procedural solutions.

> This is horrible!

Normally moderators would downweight a submission when this is the consensus from knowledgeable commenters. But this thread is so good that I want to leave it up.

Edit: Should we change the link to https://www.j-paine.org/dobbs/prolog_lightbulb.html (via the inimitable DonHopkins at https://news.ycombinator.com/item?id=22242854)? It hasn't been discussed on HN before.

Well, that's certainly a better beginnger-friendly explanation that doesn't try to make up stuff. It does what I say in my second comment above: take small steps on firm ground. That's the way to do it, for sure.

I have no idea if you should change the link to point to it. What's best for HN?

Edit: I just realised who the author is of the lightbulb joke page: Jocelyn Ireson-Paine. He's the spreadsheet guy! Check out his stuff on making spreadsheets safer... with category theory (and Prolog):

http://www.j-paine.org/old_index.html#making_spreadsheets_sa...

Why horn clauses, specifically? By the way, are you aware of resources that explain Prolog the way you did (in terms of logic?) the ones that I do know either explain how to _implement_ prolog (eg. the WAM), or provide a "high-level" explanation of unification --- missing out the details that you've just pointed out. I'd love for an authoritative reference!

Another question: do you know of an easy way to _implement_ prolog? The problem with the WAM is that it is incredibly hard to debug: I had begun implementing it (https://github.com/bollu/warren) but then gave up due to getting boggled in large heap data structures that weren't doing what I wanted, and debugging this manually got far too painful :(

>> Why horn clauses, specifically?

That's a very good question. My (sloppy) answer is that satisfiability of sets of clauses is undecidable for arbitrary clausal languages, but a variant of the resolution rule, SLDNF-Resolution, is refutation-complete for sets of Horn clauses and sound (and complete) for sets of definite clauses. Definite clauses are a subset of Horn clauses having exactly one positive literal (i.e. facts and rules in Prolog). Horn clauses are clauses with at most one positive literal.

Given a set of definite clauses and a Horn goal clause, it is possible to prove by refutation that the goal is true in the context of the program, in a finite number of steps. This is how the Prolog interactive mode works: the user enters a goal clause as a "query" and Prolog tries to refute the query by SLDNF-resolution.

SLDNF-resolution is "SLD resolution with Negatation as (finite) Failure". "SLD resolution" stands for Selective, Linear Definite resolution (it's a long story). Negation as (finite) failure (NAF) accepts that a statement is true if it cannot be proven false under a closed-world assumption (that all we know that is true, is all that we can assume is true). NAF means that Prolog programs can include clauses with negated literals, which is very handy because one often wants to say things like "X is an Evil Demon Bear from Mars if X has green fur and purple-glowing eyes _unless_ X plays the hurdy-gurdy".

These are some of the basic assumptions of Prolog: SLDNF-resolution, definite clauses and negation-as-failure under a closed-world assumption. The goal is to have a package that, under some conditions, can prove a goal given a logic program. Given that, it's possible to write a logic theorem and have it execute like a program, by proving a goal.

In terms of learning resources- if you have a bit of a logic background I think that "Programming in Prolog" by Clocksin and Mellish does a good job of going over both the declarative and imperative reading of Prolog (but it's been more than 10 years since I first read it so I might be wrong).

I haven't even tried implementing Prolog. Too much hard work and it's already been done by others :) So no idea how to do it. But it's probably the easiest way to get a good set of deep insights in the language and I should probably plonk my arse down and do it, myself.

> do you know of an easy way to _implement_ prolog?

There are some examples on the Web; I'm not sure about quality, but here is a couple:

1) https://github.com/norvig/paip-lisp/tree/master/lisp

Norvig implements (some pieces of?) Prolog in Lisp in his book (book text is freely available)

2) https://github.com/prolog8/awkprolog

An implementation of Prolog in AWK.

As a hobby prolog user, I understand what you're saying, but I also think the tutorial does a good job giving a novice a decent taste of how prolog "feels", pragmatically using some terminology of the average programmer.

Sure, one may not be able to write full prolog programs after these Y minutes. But much more importantly, hopefully they are sparked with some interest in learning the language further!

Maybe he's a Moonie. They have a much different definition of Unification. Moon makes all men equal in 'divinity' to Jesus, then assigns them wives to marry.

https://en.wikipedia.org/wiki/Unification_movement

It would be great if someone with a better understanding of Prolog could submit a PR: https://github.com/adambard/learnxinyminutes-docs/edit/maste...