3 ms·

Very nice! A key attraction of pure Prolog code is indeed that it can be evaluated in different ways to obtain better termination and performance characteristic

by triska 7y ago

Very nice! A key attraction of pure Prolog code is indeed that it can be evaluated in different ways to obtain better termination and performance characteristics, and to derive more semantic consequences of programs. The equation "Algorithm = Logic + Control" indicates this ability to provide and use different ways of control to evaluate the logical meaning of Prolog code. These slides seem to focus primarily, and in fact exclusively, on an important control mechanism called SLDNF resolution (SLD resolution with negation as failure): https://en.wikipedia.org/wiki/SLD_resolution https://en.wikipedia.org/wiki/SLD_resolution This is the standard execution method of Prolog. There are other ways to execute Prolog code too though, notably SLG resolution. SLG resolution is also called tabling, and it is provided by an increasing number of Prolog implementations and also in different variations. SLG resolution is a control strategy that terminates in many cases where SLDNF resolution does not terminate. For example, the Prolog predicate a :- a. terminates (and fails) with SLG resolution, but not with SLDNF resolution. Note that Prolog is restricted to least Herbrand models. This is different from answer set programming (ASP), where you get all models. For example, the above program has two models in ASP (and in logic) namely one where a is true and one where a is false, but only one least Herbrand model (where a is false). A common criticism of Prolog is that is "confined to depth first search", but that is not the case: You can reason about Prolog code in many different ways, and also execute it with iterative deepening, for example. This is in fact a major attraction of Prolog, not available in most other programming languages. However, the more impure constructs you use, the more this flexibility shrinks. The ability to use different control mechanisms is a strong argument to use, as far as possible, the pure monotonic core of Prolog.

nils-m-holm 7y ago
I am glad to see you respond here! It was one of your comments here on HN that brought me back to PROLOG and your homepage was a great inspiration to me. Does SLDNF really not terminate in cases that produce a cyclic answer or is it the subsequent step that replaces instantiated variables with values that will not terminate? E.g. the step that prints frames? In the latter case, would an occurs check solve the problem? How is tabling different from SLD with memoization? If this is too complicated to explain in passing, pointers to literature would be welcome!
- triska 7y ago
  I'm beyond flattered to hear this, thank you so much for writing this! Your paper is so nicely done that it definitely warrants an interesting discussion! SLDNF resolution really does not terminate in many cases, also if no variables at all are involved. The "a :- a." example which I mentioned is such a case: Speaking in terms of resolution, the resolvent of ¬a and (a ∨ ¬a) is again ¬a, and so it continues if we simply blindly try to derive ⊥ and do not check for saturation of derived clauses. This program is also not subject to occurs check (s.t.o), so occurs check does not solve the problem either even though it is in itself a good idea to use. Memoization in the sense of "remembering what has already been derived" does not improve termination either in this case, since nothing has been derived yet. You can easily implement a simple form of memoization within Prolog, but SLG resolution goes well beyond that and can improve not only performance but in fact even termination characteristics, as the above example shows. An interesting reference that may serve as a useful starting point to implement tabling is the paper Tabling as a Library with Delimited Control by Desouter et al.: https://biblio.ugent.be/publication/6880648/file/6885145.pdf https://biblio.ugent.be/publication/6880648/file/6885145.pdf I'm looking forward to seeing more papers and slides from you about these topics, and to discussing them here, keep up the nice work!
  - nils-m-holm 7y ago
    > SLDNF resolution really does not terminate in many cases, also if no variables at all are involved. The "a :- a." example which I mentioned is such a case [...] I see! In a hurry, my mind substituted "A :- A.", but your example is indeed more interesting than that! Now I am curious as to how SLG resoultion deals with this case. This is definitely something I will look into at some point! At the moment I am at a stage where I am happy that my retract/1 implementation is respecting the logical view. :) > I'm looking forward to seeing more papers and slides from you about these topics, and to discussing them here, keep up the nice work! Thank you!

by triska 7y ago

nils-m-holm 7y ago

I am glad to see you respond here! It was one of your comments here on HN that brought me back to PROLOG and your homepage was a great inspiration to me. Does SLDNF really not terminate in cases that produce a cyclic answer or is it the subsequent step that replaces instantiated variables with values that will not terminate? E.g. the step that prints frames? In the latter case, would an occurs check solve the problem? How is tabling different from SLD with memoization? If this is too complicated to explain in passing, pointers to literature would be welcome!

triska 7y ago
I'm beyond flattered to hear this, thank you so much for writing this! Your paper is so nicely done that it definitely warrants an interesting discussion! SLDNF resolution really does not terminate in many cases, also if no variables at all are involved. The "a :- a." example which I mentioned is such a case: Speaking in terms of resolution, the resolvent of ¬a and (a ∨ ¬a) is again ¬a, and so it continues if we simply blindly try to derive ⊥ and do not check for saturation of derived clauses. This program is also not subject to occurs check (s.t.o), so occurs check does not solve the problem either even though it is in itself a good idea to use. Memoization in the sense of "remembering what has already been derived" does not improve termination either in this case, since nothing has been derived yet. You can easily implement a simple form of memoization within Prolog, but SLG resolution goes well beyond that and can improve not only performance but in fact even termination characteristics, as the above example shows. An interesting reference that may serve as a useful starting point to implement tabling is the paper Tabling as a Library with Delimited Control by Desouter et al.: https://biblio.ugent.be/publication/6880648/file/6885145.pdf https://biblio.ugent.be/publication/6880648/file/6885145.pdf I'm looking forward to seeing more papers and slides from you about these topics, and to discussing them here, keep up the nice work!
- nils-m-holm 7y ago
  > SLDNF resolution really does not terminate in many cases, also if no variables at all are involved. The "a :- a." example which I mentioned is such a case [...] I see! In a hurry, my mind substituted "A :- A.", but your example is indeed more interesting than that! Now I am curious as to how SLG resoultion deals with this case. This is definitely something I will look into at some point! At the moment I am at a stage where I am happy that my retract/1 implementation is respecting the logical view. :) > I'm looking forward to seeing more papers and slides from you about these topics, and to discussing them here, keep up the nice work! Thank you!