I like the idea of walking around Prolog sometimes. But often it is used against its seemingly main purpose. What do lists do there? Prolog should be cool at tasks like: Pierre is french and never met a guy from 2nd floor at the stairs, Joe has french friend who smokes, Bob likes Alice and living under the roof, and Alice can’t stand cigarettes (and Bob); can Alice live in the same house if it has only 3 floors?
Lists though seem so unnatural to logic problems, the same way they emulate integers with lists in ‘too abstract’ lisps.
Lists allow to express certain constraints in more natural way, like "John has three cats at least one of which is male" or "I want a list of all the people that have at least three friends in common".
You don't have to use lists, but that means code duplication and low maintainability (i.e. instead of stating a condition and "repeating" for all the element of the list, you have to duplicate it explicitly).
It is not so much different from a regular language in this regard: you can write Java without using lists and use a variable for every single element, but who wants to do that ?
I like the idea of using Java sometimes. But why does it have numbers and arithmetic? Java should be great at tasks like, "cats are a kind of animal", or "my drawing program can draw both squares and circles." Arithmetic seems so unnatural in an object-oriented language. ;-)
Perhaps Prolog isn't ideally suited to a lot of programming problems -- that's a personal decision to make -- but it's silly to wonder why a general-purpose programming language would have general-purpose data structures.
Nah lists are great in Prolog. You can do all the fun recursion and matching stuff that you can do in functional languages, without extra syntax, and you can throw logic variables into them, so you can get tail recursion no matter which direction you build your list.
The thing to keep in mind about Prolog is that it's not really a logic language so much as a structural language. All operations are defined in terms of terms, so, cyclic terms aside, you can't really have non-structural "infinite" values like you can in a true logic language like TLA+ or SMT2, where infinite vectors with no defined underlying representation are the norm. You could in theory add something like that to Prolog, but you'd be defining a new fundamental type and make it a different language.
Prolog isn't based on first-order logic or anything. Its "logic" is just whatever falls out of its search mechanism and term unification. So e.g. you can't say things like "forall X: P" and expect anything useful to happen. (There's no way to express "forall X" without some finite domain for X, and there's no way in standard prolog to apply P to those uninstantiated Xs.)
Whereas languages like SMT2 and TLA+ are true logic languages in that you can express such abstract statements. You can, and people often do, write an entire meaningful and useful SMT2 program without once mentioning a concrete term. (With TLA+ this is less common due to the focus of its tooling being more on search than deduction.) The solver will apply various tactics to deduce the truth/falsity of your stated theorems.
On the contrary, Prolog does this only in a limited sense, defined exactly by the scope of its search and unification mechanisms. You can't write a meaningful Prolog program without writing concrete terms or term structures. (With the possible exception of playing tricks with dif/2.)
(There are Prolog constraint-solving extensions which basically use Prolog syntax as a frontend to a true logic engine. They're neat and I love them, because Prolog syntax is great, but my original statement applies only to core Prolog.)
TLDR: true logic languages let you talk about infinities; core Prolog does not.
That is not a First Order Logic statement. I think perhaps you mean "forall X, P(X)" or "∀x: P(x)".
This can be expressed in Prolog as "p(X)", where X is an implicitly universally quantified variable.
Do you mean something else? For example, is P meant to be a second-order variable? In that case you can always reprsent it as m(P) in Prolog. Or as m('$P') or some other syntax chosen to denote an existentially quantified second-order term.
In general, could you please clarify what you mean by "true logic engine" and "true logic language"? I'm afraid I'm not familiar with the terms.
>> Prolog isn't based on first-order logic or anything.
Yes, Prolog isn't "based" on FOL. It's an automated theorem-prover for FOL theories that uses SLDNF resolution as an inference rule. You could say it's "based on SLDNF resolution" I guess.
I'm pretty sure quantification exists implicitly, but I'm too rusty. I think someone may better answer that than me (oh, "without some finite domain for X", ok, but that does not preclude it from being logic, and as for infinite domains, I doubt any any system can work with that without undecidability - and very quickly undecidable. But I'm no expert).
> TLDR: true logic languages let you talk about infinities; core Prolog does not.
I cannot accept the first part of that, therefore can't accept the implication that prolog isn't a true LL.
And Erlang has its roots in Prolog. Yet I can't perform unification or backtracking in Erlang.
Quantification does exist implicitly, but (again, constraint solving extensions and dif/2 aside) it's not useful with respect to infinities. \+ (member(X, D), \+ P) works just fine for a finite ground D, but try with an unbound or partially-bound D and you get an instantiation error (at best) or infinite recursion (at worst).
SMT2 is perfectly happy with infinite domains. Yes, you can encounter undecidability (and obviously must in some cases), but it is not a given. You can absolutely prove theorems over infinite domains with it.
I'm basing my arguments on years of experience using Prolog, SMT2, and TLA+. You are free to disagree about the definition of a fuzzy English term, but terms are only valuable inasmuch as they are useful, and defining Prolog strictly as a logic language has not proved useful to me, given how much it differs in capability from true logic languages. The most effective programming style differs greatly between them when you realize that you must always be aware of terms and instantiation. Hence my assertion that it's much better to think of Prolog as a language for dealing with said terms and instantiation, than as a language for expressing logical statements.
To clarify: Prolog imbued with constraint-solving extensions I absolutely consider a logic language. You gain constraints and reasoning over infinities, and it allows you to stop thinking in terms of search and terms. See https://www.metalevel.at/prolog/purity for some examples of what this buys you (scroll down to "Applications to teaching Prolog"). It's enough of a game-changer to me as to warrant a different categorization.
>> Quantification does exist implicitly, but (again, constraint solving
extensions and dif/2 aside) it's not useful with respect to infinities. \+
(member(X, D), \+ P) works just fine for a finite ground D, but try with an
unbound or partially-bound D and you get an instantiation error (at best) or
infinite recursion (at worst).
The instantiation error would be raised by P being unbound, not D. You can
walk over variables with member/2.
In Swi-Prolog:
?- member(X, D).
D = [X|_3304] ;
D = [_3302, X|_3310] ;
D = [_3302, _3308, X|_3316] ;
D = [_3302, _3308, _3314, X|_3322] .
In Sicstus Prolog:
| ?- member(X,D).
D = [X|_A] ? ;
D = [_A,X|_B] ? ;
D = [_A,_B,X|_C] ? ;
D = [_A,_B,_C,X|_D] ?
yes
The instantiation error, e.g. in Swi:
?- (member(X,D), \+ P).
ERROR: Arguments are not sufficiently instantiated
- is an implementation detail, not a feature of the language (although it's
probably in some standard). You could write your own version of \+/2 that
doesn't raise an error.
>> SMT2 is perfectly happy with infinite domains. Yes, you can encounter
undecidability (and obviously must in some cases), but it is not a given. You
can absolutely prove theorems over infinite domains with it.
You can prove theorems in infinite domains with Prolog. For instance, given
the program P, below, the query Q terminates:
P =
{ s(0),
s(s(N)):- s(N)
}
Q = { s(s(s(0))) }
Now that I think about it, member/2, append/2, etc list processing predicates also range over infinite domains.
member(X,[X|T]).
member(X,[H|T]):-
member(X,T).
etc. True for lists of arbitrary length, restricted only by your computer's memory.
I don't think you are interpreting my claims in good faith (moreso in your other post where you are nitpicking about the syntax I am using when talking about cross-language concepts to make a high-level point), so I am not going to address all your statements. But to clarify the specific example I had in mind:
?- \+ (member(X, D), \+ (X < 2)).
fails with an instantiation error on X, as it ought (since </2 requires ground arguments). That's not an "implementation detail", that's how Prolog works. Core Prolog can't handle constraints outside of term structure. There's no way to express "declare an infinite vector D, whose elements are all less than 2" which is trivial to express in FOL.
You can't "write your own version of \+" to cause the above program to give the answer one would expect from FOL, without changing the language, and I'm not making claims about "YeGoblynQueenne's Imagined Prolog".
Your example on naturals breaks down as soon as one tries to make a statement ranging over the domain of all naturals. Even something simple like:
?- forall(s(N), (N = 0; N = s(M), s(M))).
dives headlong into infinite recursion. My only claim is that, it's much easier to understand why this happens if one thinks of Prolog as a search language over structural terms, rather than as a logic language where such a statement could be expected to be useful (if not necessarily decidable). It's beyond me why anyone considers this contentious.
>> It's beyond me why anyone considers this contentious.
Could you tone this sort of thing down please? Its needlessly confrontational
tone only serves to add irrelevant noise to the converstation. Thank you in
advance.
>> ?- L = [_,_,_], \+ (member(X, L), \+ (X < 2)).
Thank you for clarifying your intention with the original example. In that
case, you could redefine </2 to avoid raising an error. Off the top of my head:
1 < 2.
2 < 3.
3 < 4.
etc. Again it's a matter of implementation - in this case, of the predicate
</2, rather than \+/2.
>> ?- forall(s(N), (N = 0; N = s(M), s(M))).
In your previous comment you said that "You can absolutlely prove theorems
over infinite domains with [SMT2]", constrasting it with Prolog that if I
understand correctly, you claim cannot. In my reply to your comment, I gave
examples of theorems over infinite domains (integers and lists), that can be
proven with Prolog.
You given an example of how one of those theories can "go infinite" if you
make the right query. It can, but if you make a different query, it doesn't go
infinite and Prolog proves it. So, Prolog can prove theories over infinite
domains.
EDIT:
>> My only claim is that, it's much easier to understand why this happens if one
thinks of Prolog as a search language over structural terms, rather than as a
logic language where such a statement could be expected to be useful (if not
necessarily decidable).
Your claim would be clearer if you explained what you mean by "logic
language". Given what you've said so far I honestly have no idea what you mean
by that.
In any case, what you say above sounds like the well-understood fact that
Prolog programs have a declarative and a procedural reading and that one must
be aware of the internal machinery of the interpreter to avoid infinite
recursion.
> Could you tone this sort of thing down please? […] Thank you in advance.
These sorts of comments (and your earlier notation nitpicking) come across as smug and condescending. Why start a conversation with someone you don't appear to respect?
> In any case, what you say above sounds like the well-understood fact that Prolog programs have a declarative and a procedural reading and that one must be aware of the internal machinery of the interpreter to avoid infinite recursion.
Yes, hence why I don't understand why my statement is so contentious. I wasn't being hyperbolic with that remark; I really don't understand the strong negative reaction to my off-the-cuff explanation of the above fact.
You're clearly an intelligent person, and I like to think I am too, and since intelligent people should not disagree, let me restate my thesis in clearer terms:
By "logic language" I mean, a language which allows one to express and reason about logical relations (roughly in the sense of first-order logic). Yes, my definition is intentionally vague, as are all language classifications.
Core Prolog (meaning, Horn clauses + terms + SLD + ISO definitions of predicates) allows expressing only the logical relations of equality (=/2) and inequality (dif/2; to contrast, </2 is nonlogical in core Prolog), and then, only over structured terms (i.e., atoms + compounds), and even then, is limited by its resolution strategy. This stands in contrast to languages like SMT2 and TLA+, which permit arbitrary relations over various, even abstract, domains (such as SMT2's capability to express relations on uninterpreted functions) and which do not specify, nor are associated with, a particular resolution strategy. (TLA+ for example, is strongly associated with TLC, but there is also TLAPS, and it is specified expressly independent of any resolution strategy.)
Therefore, for someone who is wondering why Prolog programs should be written in terms of something so concrete as lists, when first-order logic rarely utilizes them, it is best to think of Prolog not as a language for reasoning about logical relations (a "logic language"), but as a language for search and unification of structured terms.
The problem is to me that you're imprecise in your claims, which is OK (edit: changed my mind, it's not ok because it's too close to ex falso (sequitur) quodlibet), and won't admit you're wrong when you are, which is bothering people.
You say "Prolog isn't based on first-order logic or anything", I point out you're wrong via wikipedia, you start fudging. You could have said it's not proper in your view because of the resolution strategy (depth first, typically) and allowing (red) cuts and we'd be with you all the way.
You say "You seem to have had no trouble understanding what I wrote", ducking the point made, viz. "That is not a First Order Logic statement", and that's the crucial point (and I'd agree, quantification over predicates isn't 1st order any more).
You evidently know your stuff but equally so do others, why are you burning bridges instead of trying to work out why there's disagreement. You could say prolog just isn't that impressive and there's better stuff available now, so in your view you don't consider prolog worthy any more, but you start denying it's a logic language at all.
Each of the three things you mentioned is a misinterpretation of what I said, but apparently clarifying intent is "fudging", so I'm done here. I don't care to argue against strawmen for internet points, and I don't care to maintain bridges with antagonistic people.
I think you read this comment as condencension, but that was definitely not my intent. I meant it in all seriousness that I would be grateful if you could reduce the confrontational tone of your comments.
Anyway I'm sorry that we failed to communicate and have a productive conversation.
I apologize for misreading your tone. I personally have a somewhat painful history of being needled and nitpicked by academics, so I am predisposed to infer such intent where none is intended, and unconsciously adapt a defensive/confrontational stance as self-defense.
Certainly, a drawn-out argument was not my original intent. I have no axe to grind, just a realization which I have found personally useful which I thought to share.
> I'm pretty sure quantification exists implicitly, but I'm too rusty.
Indeed, as in most informal logic, all free variables are implicitly universally quantified. I think the thing that makes it seem like it's not so is that people see a clause like:
p(X) :- q(X).
and think "oh, that X isn't really universally quantified, because p(X) isn't always true", but it really is universally quantified; what we're saying is:
The parent is trolling. "Logic language" is not a well-defined term, and it is not even commonly used for anything, as far as I know. The term usually applied to Prolog is "logic programming language". The parent's definition of "logic language" seems to be something like "a theorem prover's input language". Prolog is not that, but nobody claims that it is.
I am not trolling, and I am insulted that you would insinuate that. I'm offering an alternative categorization of Prolog which I have found, over a decade of using Prolog, to elucidate its pragmatic difference from languages which more directly reflect the sort of first-order logical reasoning for which @wruza wishes Prolog would see more use.
To be clear, it's not trolling to point out that theorem provers are also a good choice for reasoning tasks of this kind.
In my opinion it is trolling to repeatedly insist that Prolog wants to be a theorem prover but fails. And to obfuscate this by not using the term "theorem prover" for the kind of tool you have in mind, and to use the non-standard term "logic language" instead.
Your claim is that I'm deliberately obfuscating terminology in order to… help someone on Hacker News understand why lists and finite structure are useful in Prolog? Push an agenda to kick Prolog out of the logic language club? Stir up animosity in the language crowd of HN? Sorry, I'm not following.
Doesn't the simpler explanation, that I made up a term that tries to capture the idea I'm trying to communicate, and didn't define it precisely because it's an HN comment and not a research paper, make more sense?
(Not that "theorem prover" is the correct term. That describes a tool, not a language.)
Can you propose a better term to describe a language for expressing logical statements than "logic language"?
One application that seems to me like it should be a natural fit for Prolog is building a (human) schedule: class goes from 8-4, a student cannot take two classes simultaneously, Joe is not available on Wednesdays, etc.
I forget the specifics but every implementation of such a schedule tends up using lists and explicit recursion, (which I think is unpleasant in Prolog) In fact, most moderately complex solutions of any problem I’ve seen fall back on lists and explicit recursion. (I thought I was using Prolog to avoid all that!) That’s probably a shortcoming of the language.
If you have such constraints, why not use a proper constraint system? Prolog is in a (sometimes not so) sweet spots in terms of exploring search spaces.
For a problem like you've described, just write a SAT instance and be done with it. And if you don't know how large your solution/search space is (even a bound), then there's no alternative to creating lists and giving recursion hints.
"Lists are defined inductively: The atom [] is a list. A compound term with functor . (dot) and arity 2, whose second argument is a list, is itself a list. There exists special syntax for denoting lists: .(A, B) is equivalent to [A|B]. For example, the list .(1, .(2, .(3, []))) can be written (edit: cut for clarity) as [1,2,3]."
One big feature of Prolog that relies on lists are DCGs (Definite Clause Grammars)[0]. Lists are such a ubiquitous data structure that not having them in a language would just be painful.
Right. Developing natural language parsers was one of the main motivations for the development of Prolog. Natural language sentences are lists. List processing is something Prolog is excellent at. It's even better at it than functional languages because more things can be expressed in a tail-recursive way.
DCGs unsugar into lists, but the very fact that there's a non-list-based syntax (although lists are used for terminals, that could easily be avoided) shows that lists aren't actually essential. One has to pick some basic data structure, and lists are good for it, but they're not essential. (For example, one could use a lambda-calculus-based formalism, and then, if desired, encode lists in it in the usual way; or, as Prolog actually does it, encode lists as terms, as tempguy9999 (https://news.ycombinator.com/item?id=21772069) points out.
Correct me if I'm wrong, haven't written a lot of Prolog, but I think most optimisation-based problems are suitable for modelling using Prolog. Scheduling, time tabling, allocation problems such as knapsack problem or bin packing, etc.
Some of these problems can be quite tricky to write regular code for, but just stating the constraints and letting Prolog plan/solve it can be simpler.
I'm doing the advent of code in a different language every day, and since the day 4 was about some constraint resolution, Prolog was the perfect tool there.
That is, even before filling the list with digits, you would already have captured the constraint that two digits will have to be consecutive. Then, while instantiating the list inside has_6_digits/1, something like 134567 would never even be generated, and you wouldn't need to test it for being in range and having increasing digits.
I tried using Prolog for Advent of Code last year. It went okayish, but I seem to recall that some things were unreasonably hard, such as reading from non-Prolog-syntax files. I should give it another try this year. Maybe I missed something obvious.
Lists though seem so unnatural to logic problems, the same way they emulate integers with lists in ‘too abstract’ lisps.