3 ms·

I love Prolog -- the problem I find is that it makes hard stuff easy, but things that should be easy, hard - most of which comes from abuse of backtracking. Whe

I love Prolog -- the problem I find is that it makes hard stuff easy, but things that should be easy, hard - most of which comes from abuse of backtracking. When you realize that default Prolog SLD resolution is just a depth-first search and that every predicate you define really has a implicit "foreach" in front of it, it's easier to wrap your brain around. To get efficiency however, you need to embrace logical vars and use them as "holes" in data-structures (such as diff-lists) that will be filled in later, which does require some restructuring of your thinking sometimes.

YeGoblynQueenne 6y ago
>> When you realize that default Prolog SLD resolution is just a depth-first search and that every predicate you define really has a implicit "foreach" in front of it, it's easier to wrap your brain around. Depth-first search is used to find matching literals, but SLD resolution is not depth-first search; or it would be called "depth-first search". SLD resolution is an algorithm that eliminates literals from a clause until the empty clause is derived, at which point a refutation of the original goal succeeds. For example, let P = {q(a,b) ∧ (p(X,Y) ∨ ¬q(X,Y))} be a definite (logic) program and G = ¬p(X,Y) be a Horn goal. A refutation proof of ¬p(X,Y) by resolution might go like this: a) p(X,Y) unifies with ¬p(X,Y) with substitution θ = ∅ b) ¬q(X,Y) ∧ q(a,b) is derived from (a) (by elimination of the two unifying literals with opposing signs) c) ¬q(X,Y) unifies with q(a,b) with substitution θ = {X/a,Y/b} d) □ [the empty clause] is derived from (c) Thus, ¬p(X,Y) is refuted, with substitution {X/a,Y/b}, i.e. p(X,Y) is true with those variable bindings. Or, as a tree diagram: p(X,Y) ∨ ¬q(X,Y) ¬p(X,Y) \ / \ / \ / \ / \ / \ / ¬q(X,Y) q(a,b) \ / \ / \ / \ / □ Note that in Prolog, P = {q(a,b), p(X,Y):-q(X,Y)} and G = :-p(X,Y). I've written it in clausal form above to help with the elimination of literals. So, depth-first search is used in Prolog (but not mandated by any description of resolution) to find unifying literals for a "query" (i.e. a goal) but depth-first search is not resolution and resolution is not depth-first search. Resolution allows us to derive a set of literals from another set of literals, by elimination of literals that unify but have opposite signs. Indeed, resolution can be notated as: p,q ¬q -------- p Or, from p OR q and NOT q we can infer p. [Note: "elimination" is my own terminology, not often used in logic programming books. The correct description is that from p and ¬p we can derive empty clause.]
- thelazydogsback 6y ago
  All true, but I stand by my assertion (pardon the pun) that "Prolog SLD resolution" is depth first -- unless you're using a non-standard Prolog or some meta-predicate that implements another strategy. And any other strategy that's not WAM-inspired and depth first is prohibitive and unwarranted for the actual running of Prolog programs with all its assumed operational semantics. General resolution (SLD or otherwise) works for some theorem-proving, but not for running general Prolog programs.
  - YeGoblynQueenne 6y ago
    Your original comment said that "default Prolog SLD resolution is just a depth-first search". SLD resolution is not "depth-first search", "just" or with additions. Depth-first search is a search algorithm. In Prolog, depth-first search is used to find literals that unify with a goal, in order to perform resolution. But depth-first search is not part of SLD resolution and depth-first search and SLD resolution are not the same algorithm. You seem to be reformulating your assertion. In the last comment you say that "default Prolog SLD resolution is depth-first". That reformulation also doesn't make sense. The search used by Prolog is depth-first search. But SLD resolution is not "depth-first". There is no context in which "depth-first" makes sense outside of depth-first search and there is no context in which SLD resolution can be said to be "depth-first". That's regardless of implementation. >> General resolution (SLD or otherwise) works for some theorem-proving, but not for running general Prolog programs. I'm sorry, I don't understand this. If I understand correctly, "general" resolution refers to resolution for arbitrary clauses? SLD resolution operates on definite clauses and is sound and refutation complete for definite logic programs. SLDNF resolution is also sound for normal programs. So, yes, resolution "works" for running general Prolog programs.
  - YeGoblynQueenne 6y ago
    Hey. If you are still reading this, I must apologise for my other sibling comment right under yours. I sound like a formalism nazi! I understand what you mean that "Prolog SLD resolution is depth first". You have probably implemented a Prolog meta-interpreter and noticed that it works by putting literals on the stack, then deriving new literals and putting those on the stack, recursively and by creating a new "branch" between each literal. In fact, resolution itself is often described (or rather reasoned about) in terms of resolution trees. It's definitely not the same as depth first search, because it's not a search, but it doesn't take a lot of effort to see what you mean by "depth first" in this case. I should not have been such a terminology miser here. I'm upset myself sometimes when people demand absolute terminological clarify of me when it's obvious what I'm trying to say (and it's obvious to them, they just like to nitpick). So I apologise for the nitpicking.

YeGoblynQueenne 6y ago

>> When you realize that default Prolog SLD resolution is just a depth-first search and that every predicate you define really has a implicit "foreach" in front of it, it's easier to wrap your brain around. Depth-first search is used to find matching literals, but SLD resolution is not depth-first search; or it would be called "depth-first search". SLD resolution is an algorithm that eliminates literals from a clause until the empty clause is derived, at which point a refutation of the original goal succeeds. For example, let P = {q(a,b) ∧ (p(X,Y) ∨ ¬q(X,Y))} be a definite (logic) program and G = ¬p(X,Y) be a Horn goal. A refutation proof of ¬p(X,Y) by resolution might go like this: a) p(X,Y) unifies with ¬p(X,Y) with substitution θ = ∅ b) ¬q(X,Y) ∧ q(a,b) is derived from (a) (by elimination of the two unifying literals with opposing signs) c) ¬q(X,Y) unifies with q(a,b) with substitution θ = {X/a,Y/b} d) □ [the empty clause] is derived from (c) Thus, ¬p(X,Y) is refuted, with substitution {X/a,Y/b}, i.e. p(X,Y) is true with those variable bindings. Or, as a tree diagram: p(X,Y) ∨ ¬q(X,Y) ¬p(X,Y) \ / \ / \ / \ / \ / \ / ¬q(X,Y) q(a,b) \ / \ / \ / \ / □ Note that in Prolog, P = {q(a,b), p(X,Y):-q(X,Y)} and G = :-p(X,Y). I've written it in clausal form above to help with the elimination of literals. So, depth-first search is used in Prolog (but not mandated by any description of resolution) to find unifying literals for a "query" (i.e. a goal) but depth-first search is not resolution and resolution is not depth-first search. Resolution allows us to derive a set of literals from another set of literals, by elimination of literals that unify but have opposite signs. Indeed, resolution can be notated as: p,q ¬q -------- p Or, from p OR q and NOT q we can infer p. [Note: "elimination" is my own terminology, not often used in logic programming books. The correct description is that from p and ¬p we can derive empty clause.]

thelazydogsback 6y ago
All true, but I stand by my assertion (pardon the pun) that "Prolog SLD resolution" is depth first -- unless you're using a non-standard Prolog or some meta-predicate that implements another strategy. And any other strategy that's not WAM-inspired and depth first is prohibitive and unwarranted for the actual running of Prolog programs with all its assumed operational semantics. General resolution (SLD or otherwise) works for some theorem-proving, but not for running general Prolog programs.
- YeGoblynQueenne 6y ago
  Your original comment said that "default Prolog SLD resolution is just a depth-first search". SLD resolution is not "depth-first search", "just" or with additions. Depth-first search is a search algorithm. In Prolog, depth-first search is used to find literals that unify with a goal, in order to perform resolution. But depth-first search is not part of SLD resolution and depth-first search and SLD resolution are not the same algorithm. You seem to be reformulating your assertion. In the last comment you say that "default Prolog SLD resolution is depth-first". That reformulation also doesn't make sense. The search used by Prolog is depth-first search. But SLD resolution is not "depth-first". There is no context in which "depth-first" makes sense outside of depth-first search and there is no context in which SLD resolution can be said to be "depth-first". That's regardless of implementation. >> General resolution (SLD or otherwise) works for some theorem-proving, but not for running general Prolog programs. I'm sorry, I don't understand this. If I understand correctly, "general" resolution refers to resolution for arbitrary clauses? SLD resolution operates on definite clauses and is sound and refutation complete for definite logic programs. SLDNF resolution is also sound for normal programs. So, yes, resolution "works" for running general Prolog programs.
- YeGoblynQueenne 6y ago
  Hey. If you are still reading this, I must apologise for my other sibling comment right under yours. I sound like a formalism nazi! I understand what you mean that "Prolog SLD resolution is depth first". You have probably implemented a Prolog meta-interpreter and noticed that it works by putting literals on the stack, then deriving new literals and putting those on the stack, recursively and by creating a new "branch" between each literal. In fact, resolution itself is often described (or rather reasoned about) in terms of resolution trees. It's definitely not the same as depth first search, because it's not a search, but it doesn't take a lot of effort to see what you mean by "depth first" in this case. I should not have been such a terminology miser here. I'm upset myself sometimes when people demand absolute terminological clarify of me when it's obvious what I'm trying to say (and it's obvious to them, they just like to nitpick). So I apologise for the nitpicking.