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