Is there an easy way to view "stack traces" with the interpreter?

General
25

Thank you! Yeah, it would make sense that memoizing data would cause a lot of space to get used up.

In the long term, statically cataloging everything is, I think, the best idea, and then tabling works flawlessly. It’s not possible right now, and I can’t do much about that, but it is the best idea.

Until then, I was able to reduce the memory usage by having two versions of trait/N: one that has a Derivation parameter and one that does not. The one without a Derivation parameter is called much more frequently in practice, and used for basically all queries involving variables. The one with a Derivation is basically only called on atoms, and so tabling doesn’t memoize as much at a single time.

Thanks for all the time you took to discuss this :slight_smile:

26

It depends on the number of elements that have to be iterated through. As an example: If the number of elements is known, can append (to the start of a list) efficiently using e.g.:

?- T = [4, 5, 6], L = [1, 2, 3|T].
T = [4, 5, 6],
L = [1, 2, 3, 4, 5, 6].
27

Tabling is intriguing and not always intuitive if you come from “normal” Prolog. Unfortunately there is no good public text that explains how to use it under which conditions. Some hints:

  • You must table predicates that are subject to “left recursion” (call a variant of the original goal). If it concerns mutual recursion (a → b → c → a), tabling one of these is enough to make the program behave.
  • You must table predicates for which you want sound (Well Formed Semantics) negation using tnot/1.

That is for sure. Other predicates are optional as tabling does not modify the semantics for these. It is only memoization, so you trade between space and time. SWI-Prolog’s tabling overhead is (still) fairly large, so limit yourself to predicates that are slow to recompute. Use profile/1 to figure out your bottlenecks.

There are some funny things in tabling. If we have a recursive predicate, we normally first have the base clause(s) and then the recursive clause(s). Using tabling you can swap these around as it won’t loop anyway. In fact, it often leads to fewer variants stored in the table and thus less table space.

You may wish to install GitHub - JanWielemaker/my-prolog-lib: Personal SWI-Prolog utilities library · GitHub, which provides library(tdump) and library(tstat) that provide some toplevel utilities that show space time and status of tabled predicates.

edit these libraries are added to the most recent versions (stable and devel) of SWI-Prolog

29

There’s a note about tabling and DCGs in the XSB documentation, concerning potential quadratic behaviour (this would also apply to anything that uses difference lists and possibly also to anything that uses regular lists and append/3):

I don’t know if this also applies to SWI-Prolog.

30

I think yes. XSB has a work-around for some of this called interning. That is not (yet) implemented in SWI-Prolog.

32

All theorems talk about one single subject.

I should clarify that I am deliberately trying to avoid using this assumption. The main point of this implementation is to make it possible for this to not be true, which is something that I certainly wasn’t clear about. My bad!

I’m going to support at least relation(X, Y, P, V) so that you can express theorems like.

trait(X, lpc, true) :- relation(X, Y, open_subset, true), trait(Y, lpc, true).

If this feature was added, it would be used quite often, because theorems like this are a common scenario, as are proofs that use theorems like this. Having two variables might dash the hopes of not using lots of space because now the search space itself is “quadratic” in a way, in addition to being more “entangled” (a proof of something for one space can cause you to generate a proof of something for another space)—but that’s okay.

I think I get what you’re saying about this overall, though: have Prolog derive the theorems generally rather than immediately trying to instantiate them.

I don’t see how that helps, though, even in the case where we assume all theorems only have one variable in them—when you derive a theorem, you’d need to find the assumptions of the theorem, and that would lead to the same explosion (it’s necessary and common in pi-Base to have “A and B implies C”, and sometimes we even have a conjunction of three or four assumptions). But maybe it’s possible to derive, say, just theorems with a single assumption trait(X, p1, v1) :- trait(X, p2, v2), and that would still allow for a decent amount of sharing between theorems?

I also don’t quite understand what you meant when you said have only a single fact trait('space', _, _, asserted). This looks like you created a space which has every single property and every single value. I think that is what you intended to have, so that way this “fake space” could be used to derive any theorem. Does that sound at least somewhat right?

33

meant to reply to @peter.ludemann

Yes, it’s that. When you prove a goal, you prove a subgoal, which copies the subgoal’s list into a table (or at least copies the list after each append). So requesting a proof, and getting one, of length n, would seemingly cause the entire proof tree to be copied several times and result in n^2 complexity.

I need to spend some time thinking about XSB’s
solution.

But ignoring that for now, I think storing the proofs as a tree as @anon37422618 suggested is a great idea. If Prolog lists are implemented as something like a linked list, then append is avoided, and the space complexity would become linear (that is, assuming that Prolog does not decide to make a deep copy of everything before putting it in the table).

34

Yes, it’s that. When you prove a goal, you prove a subgoal, which copies the subgoal’s list into a table. So requesting a proof, and getting one, of length n, would seemingly cause the entire proof tree to be copied several times and result in n^2 complexity.

I need to spend some time thinking about XSB’s
solution.

But ignoring that for now, I think storing the proofs as a tree as @anon37422618 suggested is a great idea. If Prolog lists are implemented as something like a linked list, then the space complexity could become linear (That is, assuming that Prolog does not decide to make a deep copy of everything before putting it in the table.)

Now the suggestion of not instantiating variables makes more sense—we basically want to store the implication graph, and then, for fixed spaces, the property will either be asserted (represented by a leaf of the tree), or we query the graph to find out what to try next.

36

It will. The table space is disjoint from the Prolog stacks. It must be as the data needs to survive backtracking. Tables are stored as tries. Actually, as a trie of tries, i.e., the outer trie stores goal variants and the inner tries store answers.

Possibly you can find some way to not store the entire proof, but individual nodes from which you can restore the proof? Not sure how, but that would be my line of thinking.

37

Yeah; I think that the current implementation does something entirely different from the approach I’m taking!

38

Got it. Hmm.

The problem is that the partial derivations do need to be tabled completely: otherwise the issue of cycle detection comes back.

Here would be a very beautiful world that probably has problems. I’m not going to implement it but I think the fact it should work is really cool.

Partial derivations would be stored like you’d expect. So implies(trait(X, p, v), trait(X, p2, v2), D) would have some value for D in the table: say

[theorem(trait(Y, p, v), trait(Y, intermediate, v)), theorem(trait(Y, intermediate, v), trait(Y, p2, v2)]

Here I’m using Y to represent a variable which is internal to the table.

Upon querying, we make a copy of this list with a fresh variable, and never unify the table variable Y with our input. Makes sense.

But in the table, if I look for implies(trait(X, intermediate, v), trait(X, p2, v2), D), then the table would have stored
[theorem(trait(Y, intermediate, v), trait(Y, p2, v2)]
with the same internal Y. That would allow for linear space complexity.

As far as I’m aware, this is sound, because every time we get a value from the table we deep-copy it anyway. And if we finished doing subgoal/n and goal/n backtracks, oh well, no goal/n for the table, but subgoal/n is doing just fine. After each subgoal finishes, we copy its value out for our use, then use it, and then, if our main goal succeeds, (somehow) copy the main goal’s value, keeping track of the subgoal’s value within it, and re-unify that subgoal’s value with the value from the table. Then put the main goal value (which has now been copied, and so the only thing it shares with is the subgoal value from the table), into the table. And we’re still disjoint from the stacks.

I don’t know the most general terms in which this optimization can be phrased, but it’s interesting. Of course it costs an extra unification.

Of course, that isn’t the real world. So I’ll think about other options later.

Edit: Well when I put it like that, it seems pretty clear that nodes totally would work. Oops!

In fact, all a node would be is just the clause that was used (and perhaps variable instantiations). So if I queried some trait—if it was successful, it would provide me the clause that it used to derive the trait. From there, I call each node in the body, which calls each node in its body, etc. to reconstruct a tree. If the proof fails, no node is returned.

40

Did it.. Probably not the best job, but I did implement nodes. Not quite sure if it saves space for the average user.

The trick’s clever though. Theorems are (after expansion) derived(trait(X, property, value), id, CallerInfo) :- stuff. ID is a (mostly) unique ID for the clause; CallerInfo is an out parameter containing the IDs of the next clauses you need to call to get a successful derivation. You then can write a loop that queries a theorem,

I think, because tables are stored based on call variants, though, you need to make sure the ID parameter is ground. Certainly I’ve gotten incorrect results when the ID isn’t ground, so I just ground it.

I’ll let y’all know what the current implementation uses, since @anon37422618 mentioned a lot of other algorithms. Probably it’ll be efficient to implement whatever’s being used now.

42

True. Best is to use modules. Then you can export your entry points, making it a lot easier to understand the code and they become bold and blue.

Well, the cross referencer does run term expansion if it can. So, it is wise to run the development tools while the code is loaded. This does not work for SWISH. Works fine for local development. If for some reason you frequently need to restart Prolog (due to side effects of running the program), I usually run two Prolog instances: one with the code loaded for editing and one to run the code.

Then there are some tricks such as if you want term expansion to generate clauses for e.g., p/4, use something like this, i.e., expanding the same predicate as it produces.

term_expansion(p(dummy, _, _, _), Clauses) :- ...

p(dummy,_,_,_).

If you really want, the library(prolog_colour) has hooks that allow you to make it understand what you are doing and (re-)define the style for identified fragments. An extensive example of this is in library(http/html_decl). Not worth the trouble for a simple program, but worth considering if you define some infrastructure you’ll be developing for an extensive period of time. You can also use that with SWISH, but only if you run your own server, so you can load these extensions.

43

Thanks, but I’m talking about something a little different, and I don’t care too much about the color red.

It has to do with these scary red messages: right here. They say my code doesn’t exist, then happily query from it.

Meanwhile, SWI-Prolog on Windows displays nothing of this sort.

44

Might be a SWISH issue. Can you post a link to the program on SWISH ?

46

The public version does not. If you run your own server you can do more, but the public version is fully stateless.

Yes, Tinker can do this. It offers a virtual filesystem from Emscripten and browser storage based persistency for part of that.

But then, this does not add anything new compared to using term expansion. Note that if term expansion requires more context, you can have one term expansion rule that simply asserts the terms read, mapping them to [] and then you expand end_of_file by translating all asserted terms and return a list of clauses (and/or directives). That is, for example, how CHR works in SWI-Prolog (while originally it was a transpiler).

49

In a way, you could say tabling turns backward chaining into forward chaining for the minimal cases needed to make left-recursion terminate. I.e., It delays the left-recursive calls and when answers come from the other clauses it resumes the delayed goals with these answers (from the table).

That also holds for tabled negation: if you can’t solve it now, delay the tnot/1 goal until some answer has been added to a table that allows you to solve it. For negation, that implies if an answer is added to the table, the negation fails. If the table is completed without an answer the negation succeeds. This resolves a lot of cases and can be considered forward chaining. We may end up with mutually dependent negations that cannot be resolved. Then we have some additional logic to decide or decide the negation and its dependent goals are undefined.

At least, that is how I try to understand tabling at a conceptual level. It also explains that the termination conditions are the same as with forward chaining, i.e., any program for which every goal has a finite number of answers terminates. In other words, the only way to get non-terminating programs is by having a goal that has an infinite number of answers like any integer (given unbounded integers), any list, etc.

51

Tabling (as discussed here recently) stores its tables in tries. The structure is a trie of tries, where the outer trie maps goal (variants) to answer tries. Adding an answer to a trie if it is not there is typically faster than a dynamic DB query and assert as the query and adding is one pass and in this case adding the new path is just adding one new atom to a hash table.

There is more, as tabling only pushes new answers through the delayed goals why you go over the whole lot until nothing can be added. But, the tabling approach has a high price in suspending and resuming computations. There are two ways to do that. XSB goes back in history, runs the suspended goal and then forwards again to the current state. SWI-Prolog uses delimited continuations, which effectively copies a part of the stack and restores this to run the suspended goal.

Your approach also gets more complicated with more complex goal dependencies.

53

No. The trie implementation is fairly competitive to XSB. The issue is that the logic for turning a normal predicate into a tabled predicate is all in Prolog for SWI-Prolog and much more low-level in XSB. As a result overhead of tabled calls is much higher than for XSB. That could be resolved by using a dedicated predicate supervisor rather than the generic predicate wrapper supervisor and make this dedicated supervisor figure out the involved table and its status.

The initial SWI-Prolog tabling implementation was all in Prolog by Benoit Desouter, proving delimited continuations is a building block to implement tabling with little impact on the Prolog VM. In the current implementation you can still recognise the design, although a lot of the Prolog code by Benoit was moved to C and I implemented most of the XSB features. This progressed pretty fast thanks to weekly telcos with Theresa Swift and David Warren from XSB (and Benjamin Grossof providing the resources to make this happen).

The suspension mechanism has been compared in the literature (for stack copying, but that is essentially what SWI-Prolog does). Bottom line is that it is easy to create programs where either of them is better and thus it is hard to assign a clear winner. You can easily see why, SWI-Prolog depends mostly on the depth and size of environment stack frames that propagates from one tabled call to the next, while XSB mostly depends on the number of bindings created between these two points.

55

Only left recursion. If it killed all infinite recursion it would cause incompleteness.

Not clear. If there are new variables something’s changing them and that something can eventually result in termination.