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

General
1

Hi everyone! I’m Sean, and I think Prolog is really cool. I am helping to make a deductive database and think Prolog is a great tool for the job.

I have an unusual requirement, though. I don’t just need to be able to query facts, but also query for the deduction path Prolog took to get to a fact. So basically, I want to see what Prolog’s derivation steps were: each rule that it took which helped it get toward the goal. (Not the ones that failed and it just backtracked out of, but the ones that actually helped it get to the goal).

I can implement this in Prolog myself, but I’d assume it would be much more elegant and fast if the interpreter did it. I know the interpreter has a trace function—is there any way to perhaps use that to get a derivation of some fact?

2

Not unusual at all.

You should check out trace/1 and trace/2 as a start. Maybe only trace the exit port?

Others might suggest meta-interpreters.

But surely there is a lot of existing literature on the topic, with solutions that go way beyond just printing a trace.

3

Thank you so much! Yes, there surely has to be work on this. I just haven’t managed to find it yet. A meta-interpreter was what I was thinking at first and I tried to build something myself, but I realized that maybe there’s no reason to do that.

The thing I need is 1) stack tracing 2) forbidding a predicate from calling itself with exactly the same arguments, even through another predicate in between. 1) is quite necessary for 2). I think I figured out most of a solution so I’ll put it here.

You helped a lot. trace/1 does not have what I need, but its source code sure does.

wrap_predicate/4 lets you run a hook before/after a predicate. The tracer uses this to print stuff, but I can use it to set some global variables and get what I want as a list.

b_setval/2 sets a global variable that resets on backtracking, which lets me create a list of clauses and heads that I’ve already tried. This should let me do stack traces/checking for cycles.

prolog_frame_attribute/3 gives me access to the currently running clause, which is great. This being said, it is decompiled and so may not be the exact clause that I started with.

That last part is the only part where I’m still unsure—I do need the exact clause, because the structure of each clause is an important part of the database itself (maybe someone knows if there’s a library that lets you efficiently get the exact clause?). But overall, this task is looking extremely manageable. Thank you!

4

Would tabling do what you want?

5

Possibly. I’d have to try it. But it depends.

xyz :- one_path.
xyz :- another_path.

If I need to get every possible non-cyclic derivation of xyz, then tabling shouldn’t work because every time I call xyz, it just says true because it’s memoized, I think? If I only need one, then tabling should work. But whether I need every derivation or one derivation, I need to be able to see some derivation path.

6

Turns out there’s a very easy solution if you let the compiler do it for you. It likely is not efficient and may hurt a Prolog expert’s heart (sorry!), but it at least does what it needs to.

My rules look roughly like:

trait(thing, prop, value) :- stuff.

So I can use term_expansion to get the exact value of my clause at compile time, then append that clause to a list. Example:

term_expansion((trait(X, P, V) :- Body), (trait(X, P, V) :- b_getval(stack, Stack),
b_getval(derivation, Derivation),
maplist(dif(trait(X, P, V)), Stack), % cycle checking!
b_setval(stack, [trait(X, P, V)|Stack]),
b_setval(derivation, [(trait(X, P, V) :- Body)|Derivation]),
Body,
b_setval(stack, Stack),
)).

prove(trait(X, P, V), Derivation) :- b_setval(stack, []),
b_setval(derivation, []),
trait(X, P, V),
b_getval(derivation, Derivation).

And, while quite clunky and probably not great on space efficiency, it does do exactly what it’s supposed to. Note that the bodies are always short, never more than a conjunction of three things.

7

The original clause is not in the Prolog DB. There is library(prolog_clause), providing clause_info/5 that tries to recover the position information of a clause and the variable names. That is used by the source level debugger. It is essentially heuristic though: it decompiles the clause and reads the original clause from the file and then tries to link these together based on knowledge about possible transformations the compiler and some libraries might perform.

P.s. Great work!

8

To be meaningful, include variables in the tabled predicates, so that the variables can be instantiated.

With zero variables involved, there is just predicate success or failure.

9

My bad. It was meant to be an example, but it was a bad example :slight_smile: My real clauses have variables, in the head and body.

But about tabling, since someone mentioned that earlier: tabling makes the derivations completely gone, so maybe tabling means that you never actually call anything? (This is true even on the first run of the system—the derivation list is [].)

It does indeed avoid infinite recursion though! Maybe this form of tabling would be useful, but they say it isn’t always sound?

Update: Now that I understand what this code should do, I can reimplement it without using global variables. Tabling would then work, though I’m not sure what use it would have.

I know that I could just tell Prolog “these N atoms are the only objects in existence”, but that’s inelegant and Prolog will just try every individual atom when it gets stuck. So I decided to do something more clever and fun even if it’s slower.

Like Datalog, right now I only use atoms inside functors. There is nothing nested like trait(special(X), lpc, true)). So every time Prolog unifies one of my variables, it only can turn one capital letter into another capital letter (making two variables equal) or an atom. Pigeonhole principle says (I think?) that the only way we can get infinite recursion is if one clause ends up calling itself with the same pattern of variables (even if the variables are not identical to the original).

So in my term_expansion, I gave each clause an ID (the ID used in the database, which I’d want to have access to anyway), and put the ID plus the head of the clause on the stack. Then instead of checking if this clause head has been seen before, I first check if the clause ID has been seen in some OldHead before (i.e. same clause) and then if it has, check to see if OldHead =@= CurrentHead.

10

It would be interesting to see a minimal example of the problem case, and what the intended solution looks like :slightly_smiling_face:

11

You mean the problem with my code or the problem that my code is trying to solve?

12

The problem that your code is trying to solve :slightly_smiling_face:

14

Sure. If you want full concreteness I can tell you the exact use case of this code.

So the database is a collection of objects, properties for each object, and theorems about the properties. Each theorem is a Horn clause. An example theorem (note the real database is not in Prolog—it’s in JSON, but it is exactly this kind of thing):

trait(X, connected, true) :- trait(X, path_connected, true).

Since every theorem in the database is quantified in exactly this way, the database as it is now doesn’t even make mention of a variable, storing something closer to:

trait(connected, true) :- trait(path_connected, true).

but that’ll have to change one day.

An example property (same as it would be stored in the database):

trait(reals, path_connected, true).

The (real) database has over 200 objects and over 200 properties, so instead of storing every single property for every single object, it deduces them from the theorems it has. The key is that it can provide you a deduction upon request. You can also query what objects have a given property, and what properties a given object has (these don’t require derivations).

You also can query trait(obj_atom, prop_atom, V) and get the truth value of a property if there’s any info, including a derivation if you want. All of this is quite fast on the current implementation, which I did not make.

The exact query need not be trait/3 or anything in particular.

There’s been talk of increasing the database’s expressive power in terms of what theorems it can produce (e.g. having two quantified variables) and I thought Prolog might work well for this, since the original database literally is already a database of Horn clauses. So I wanted to try and, for fun, recreate the database and its deduction feature in Prolog. That’s the very concrete thing I am coding. My existing solution that I described does seem to work, but incredibly slowly (it takes forever and a day to finally realize you’ve walked through a cycle, though it does look like the code is not recursing infinitely, and recursion depth limits do work eventually).

15

This is awesome! I realized this too—the global variables are unnecessary and probably inhibit PL’s ability to reason about the code. Thanks!!

16

call_with_depth_limit/3 causes deeper calls to fail. For example:

p :- p.
p :- write(hello).

This loops in Prolog, but not when using a depth limit:

?- call_with_depth_limit(p, 100, X).
hello
X = 101 .

If you properly want to handle cycles (left recursion), tabling is your best option.

18

Hi! Thanks so much for responding.

Yes, I ended up using =@=; thank you for the great suggestion! I have another optimization I need to implement, so I don’t have any new news to report. I haven’t implemented trait/6 yet, but I am excited to.

However, subsumption seems like it’s very cool and like it could help. I’d need to play around more. Maybe it’s possible to have both subsumption and mode directed tabling at the same time—mode directed tabling would be so that we can still get a derivation for a trait without having cycle issues, and subsumption would ideally also speed things up. Thanks again!

19

This looks awesome! I’m just a little confused on what I and O are. I think I is a proof, but am more confused about what O is doing.

21

That’s really neat. I’ll try something like this and let you know how it goes.

I’d be curious how to table such a thing, though. For a regular list, I know how to use answer subsumption, but not for a difference list.

Also, if anyone likes topology and wants to see what this actually is, check out https://topology.pi-base.org. Contributing is a lot of fun (usually in the form of adding new properties/spaces or proofs for existing spaces to have some property). I am not a lead maintainer of the project, though, and so this is just an avenue of exploration and fun.

22

This is running great right now! Thank you to everyone who encouraged tabling. It made a gigantic difference.

I still wasn’t able to use a difference list; I used a regular old list that I called “append” with (is that severely less efficient? I bet tabling lessens that impact anyway). But even with that inefficiency, it’s still extremely fast, especially after the first run where tables are generated.

I noticed that I was running out of private table space, and I’m going to look for a flag to increase the table space limit. For my use in this project, though, I also found a workaround. I ran out of table space specifically when I was trying to find every object with a given property (i.e. trait(X, p000001, V)), which makes sense, considering that all of these theorems are quantified over the space X. So I have a space_declared predicate that tells me all the spaces that I have in the database, and any findall query first will call space_declared to force Prolog to not worry about anything other than those 200-ish spaces. I said I wouldn’t do it, but with tabling it’s not so bad.

23

Also, I may have found a SWISH bug? It doesn’t happen on the local interpreter: I get no errors there.

neg and many other procedures are said to not exist, and yet can be called no problem: neg(A, B). works just fine. The term expansions work too. It all works, but there’s an error nonetheless.