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!
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
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!
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!
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
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
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.