BTW, I brought this up a while ago, but nothing came of it:
BTW, I brought this up a while ago, but nothing came of it:
Eventually that did get into XSB under the name answer subsumption, in various other systems called mode directed tabling. It is also in SWI, added by Fabrizio Riguzzi and changed significantly under all the tabling work carried out recently. The concept comes with some pitfalls though. A couple of papers have been published on the soundness of this approach.
See https://www.swi-prolog.org/pldoc/man?section=tabling-mode-directed for the SWI-Prolog implementation. The interface combines most of what is provided by other systems. You can see already one issue: the
last from B-Prolog/YAP are poorly defined as the execution order under tabling is poorly defined.
I tried first to comment out the table directive, and use iterative deepening: it works of course, yielding the solution
?- length(L,_),go(L). L = [lr(s), rl(f), lr(w), rl(s), lr(c), rl(f), lr(s)] .
Meanwhile, I was thinking about mode directed tabling (Jan answer was not yet there…), indeed just change the directive to
:- table wsc(_,_,_,_,lattice(shortest/3)).
and you will get the same solution as above:
?- go(L). L = [lr(s), rl(f), lr(w), rl(s), lr(c), rl(f), lr(s)].
shortest/3 was of course grabbed from the docs page.
Maybe noteworthy, on your original code, I first tried to
?- unleash(-all). ?- trace. ?- go(L).
and there it loops, after having tried to start tabling on each wsc/5 variant. Not the easiest thing to debug…
In this case,
table wsc(_,_,_,_,first) works but table
wsc(_,_,_,_,last) goes into an infinite loop, as expected; so
all wouldn’t be a viable mode unless there were also a way to look at results and prune them by checking for circularity.
I found this paper: Tabling with Sound Answer Subsumption (this will take me a while to read!) … are there others you can suggest? The XSB manual has only a single example with
lattice(Pred) and I couldn’t find any documentation on what happens if the call to Pred fails (if failure of Pred causes the associated answer to be removed, then I was wondering if I could use that to prune results – in the wolf-sheep-cabbage example, to remove answers with loops).
BTW, one paper by Warren ( LPOP2018 XSB Position Paper) has a
fold mode … I’m guessing that’s a generalization of SWI-pl’s and YAP’s
That was the one I was primarily referring to. Thanks for finding. I vaguely recall there is more, but I’m not sure.
AFAIK, the lattice predicate should not fail and failure should be considered an error. If you do not want to change anything, just make the lattice predicate return the current accumulated answer. Are you referring to some way to force early completion?. Early completion is -for example- used for ground goals. Once proven, we know there is no point in trying to produce more answers.
No (AFAIK), but it is related. It came up in one of our virtual meeting on tabling. I missed it and I think it isn’t even documented in the XSB manual (not sure). The idea of the lattice predicate is that this predicate satisfies the condition to make the computation sound, which is why XSB calls it answer subsumption.
fold is technically completely equivalent to
lattice, but promises no soundness and thus you can define
last and other unsound relations using it. At least, that is my current understanding …
Is the paper worthy of adding to Useful Prolog references Papers section?
Since I haven’t used tabling yet, I don’t know if this out on the extreme or a good general paper.
I’d rate it a pretty advanced topic. There is a lot more to say about tabling that would help people much more and that is nowhere documented. The most concrete are probably various sections of the XSB manual. David Warren once started on a book, but there is not more than a draft with, AFAIK no plan to finish it. I have a copy. I could ask David what he thinks about making it available online, maybe in some wiki format such that the community can use and enhance it?
As far as I can tell,
fold isn’t documented in the XSB manual. There’s this compiler option (which I don’t understand):
unfold_off When specified, singleton sets optimizations are not performed during specialization. This option is necessary in Version 3.8 for the specialization of table declarations that select only a single chain rule of the predicate.
BTW, most of the links on DS Warren’s homepage don’t work (" ftp.cs.sunysb.edu*’s server IP address could not be found"), including his draft book on tabling. I don’t know how that’s related to the tutorial in the manual (Chapter 5).
I would suggest throwing an error in that case – silent failure of a lattice predicate is probably very difficult to debug. As you say, the lattice predicate can always return the current accumulated answer.
Yes, I’m trying to force early completion when a solution is a circular path.
I think that is related to code specialization, not to the fold(pred) option of tabling under answer subsumption (but I could be wrong).
Might make sense. As I read the code, failure is interpreted as keeping the existing answer. More a long term issue I’d say though.
A post was split to a new topic: Create Wiki book from XSB tabling text by David S Warren?
I’m starting to think you’re right about that.
The tabling mode
first gives a hint … it gives a single solution that (I think) is guaranteed to not have a loop. But subsequent solutions (including
last) aren’t prevented from infinite backtracking.
(I need to think a bit more about this … possibly delimited continuations (which I think are used in implementing tabling) might lead to a more elegant solution than passing around a set of states and checking for loops.)
Picat claims to be able to solve this problem, and produce a list of actions, using “tabling”. Does anyone on this list know Picat, and can explain how this is done?
(http://picat-lang.org/ Example 4)
The planner module in Picat (which is used in Example 4) is basically tabled (optimal) path-finding with a bit extra features. More defails about this is the Picat book (http://picat-lang.org/picatbook2015/constraint_solving_and_planning_with_picat.pdf ), page 95ff (PDF file pages 103ff). Section 5.2 describes the implementation of unbounded best_plan.
It could be that you need eager tabling. SWI-Prolog only implements lazy tabling, means you cannot use SWI-Prolog tabling to generate infinite solutions via tabling. There is a paper from Picat folks about their eager tabling, which is able to continue tabling and returning results at the same time.
In my system I have eager and lazy tabling but not yet recursion. Picat is able to combine eager tabling with recursion, I am not yet that far. The difference between lazy and eager also affects mode directed tabling. Here is an example from my system:
:- use_module(library(advanced/tabling)). p(a,1). p(b,2). p(b,0). p(b,3). :- table q(_,max). q(X,Y) :- p(X,Y). :- table r(_,max) as [eager(true)]. r(X,Y) :- p(X,Y).
And now querying to see the difference:
Jekejeke Prolog 4, Runtime Library 1.4.2 ?- q(X,Y). X = a, Y = 1 ; X = b, Y = 3 ?- r(X,Y). X = a, Y = 1 ; X = b, Y = 2 ; X = b, Y = 3
I notice that for the shortest path, Picat uses
table(+,+,-,min), where the “
-” is for the parameter that gets the generated path. That’s the argument that causes SWI-Prolog’s tabling to not prevent an infinite loop – AFAICT, SWI-Prolog doesn’t distinguish between input and output parameters
In Picat, does a “
-” in the
table declaration mean that the argument’s value isn’t used when deciding to reuse an entry?
Anyway, shortest path isn’t what I was trying to do – it was all paths that don’t contain a cycle … can Picat handle that? (e.g., change the declaration to
Is this the same “eager tabling” as in Linear Tabling Strategies and Optimizations by Zhou, Sato, Shen ? I couldn’t find the Picat paper you mentioned.
Isn’t this distinction often referred to as batched scheduling vs local scheduling? It is true that current SWI-Prolog only implements local scheduling and (thus) produces no results before the table is complete.
Based on the fact that Picat is mostly B-Prolog with a different syntax I assume the “-” comes from B-Prolog where it meant “Keep (only) the first answer”. That is implemented in SWI-Prolog as well, but note that first means little in the contest of tabling where the order in which answers are generated is not defined (unlike classical SLD resolution).
B and YAP also define @ (‘all’). This is not implemented in SWI-Prolog.
You can use
lattice(pred) to collect a set of paths where you ignore all cyclic paths. A small caveat is that the first path could in theory be cyclic (I guess) and the hook is only used to combine paths. Actually we need
foldl here. This still is not implemented in SWI-Prolog, but AFAIK
lattice are in fact synonyms in XSB.
lattice implies restrictions on the defined relation that guarantees logically correct results, but doesn’t verify/enforce whether this relation holds (I guess this is theoretically impossible).
Still, as long as lattice/foldl guarantees that the set of produced results is finite I think it should terminate. Not tried …
I tried that a little while ago and couldn’t get it work (I still ended up with infinite loops, but gave up at that point rather than digging into it). But things might have changed, so I can re-try.
I noticed in Constraint Solving and Planning with Picat that there’s an “
nt” mode (Section 4.2, page 81 of the PDF):
The last mode, Mn , can be
nt, indicating that the corresponding argument will not be tabled.
It’s not clear to me why this can only be used for the last mode; perhaps it’s because the last argument is presumed to be a return value?
Adding a cross reference for “lazy” and “eager” tabling from
I have little clue what this means. If you just want to ignore some argument just write a wrapper without the argument. Otherwise, tabling creates a table per call variant which stores the instances of this variant for which the predicate is true. Mode directed tabling or answer subsumption change this in the sense that for specified arguments we do not add all variants to the table, but instead maintain a single “aggregated” answer. There is a lot to say about the semantics. From a termination point of view this can turn an infinite number of anwers into a finite number.