10 ms·

"The thing to keep in mind about Prolog is that it's not really a logic language [...]" WWWut? Eh??? Come again? Plz esspalin.

colanderman 7y ago
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.
- tempguy9999 7y ago
  With respect, at least some of that's badly wrong. From https://en.wikipedia.org/wiki/Prolog https://en.wikipedia.org/wiki/Prolog "Prolog has its roots in first-order logic" 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.
  - JadeNB 7y ago
    > 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: ∀X, p(X) ← q(X). i.e., for all X values, in order to prove p(X), it suffices to prove q(X). See, for example, https://en.wikipedia.org/wiki/Horn_clause#Definition https://en.wikipedia.org/wiki/Horn_clause#Definition , which says > In the non-propositional case, all variables[note 2] in a clause are implicitly universally quantified with the scope being the entire clause. Prolog's resolution exactly follows this proof strategy; see, for example, https://en.wikipedia.org/wiki/SLD_resolution https://en.wikipedia.org/wiki/SLD_resolution .
    - tempguy9999 7y ago
      Appreciated. Knew ∀ was in there somewhere... Will check out SLD
  - colanderman 7y ago
    > "Prolog has its roots in first-order logic" 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 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.
- YeGoblynQueenne 7y ago
  >> "forall X: P" 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.
  - colanderman 7y ago
    > That is not a First Order Logic statement. I think perhaps you mean "forall X, P(X)" or "∀x: P(x)". You seem to have had no trouble understanding what I wrote. What's the point of this comment?
tom_mellior 7y ago
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.
- colanderman 7y ago
  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.
  - tom_mellior 7y ago
    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.
    - colanderman 7y ago
      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"?

colanderman 7y ago

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.

tempguy9999 7y ago
With respect, at least some of that's badly wrong. From https://en.wikipedia.org/wiki/Prolog https://en.wikipedia.org/wiki/Prolog "Prolog has its roots in first-order logic" 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.
- JadeNB 7y ago
  > 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: ∀X, p(X) ← q(X). i.e., for all X values, in order to prove p(X), it suffices to prove q(X). See, for example, https://en.wikipedia.org/wiki/Horn_clause#Definition https://en.wikipedia.org/wiki/Horn_clause#Definition , which says > In the non-propositional case, all variables[note 2] in a clause are implicitly universally quantified with the scope being the entire clause. Prolog's resolution exactly follows this proof strategy; see, for example, https://en.wikipedia.org/wiki/SLD_resolution https://en.wikipedia.org/wiki/SLD_resolution .
  - tempguy9999 7y ago
    Appreciated. Knew ∀ was in there somewhere... Will check out SLD
- colanderman 7y ago
  > "Prolog has its roots in first-order logic" 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 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.
YeGoblynQueenne 7y ago
>> "forall X: P" 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.
- colanderman 7y ago
  > That is not a First Order Logic statement. I think perhaps you mean "forall X, P(X)" or "∀x: P(x)". You seem to have had no trouble understanding what I wrote. What's the point of this comment?

tom_mellior 7y ago

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.

colanderman 7y ago
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.
- tom_mellior 7y ago
  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.
  - colanderman 7y ago
    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"?