3 ms·

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 firs

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

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