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!

1 Like
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.

2 Likes
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!

1 Like
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:

13

You could also use term_expansion/2 to change trait/3 into trait/6:

/* Expand Clause */
term_expansion(trait(X, P, V), trait(X, P, V, I, I, _)) :- !.
term_expansion((trait(X, P, V) :- Body), (trait(X, P, V, 
            [(trait(X, P, V) :- Body)|I], O, S) :- Body2)) :-
   add_args(Body, Body2, I, O, [trait(X, P, V)|S]).

/* Expand Body */
add_args(true, true, I, I, _) :- !.
add_args((A,B), (X,Y), I, O, S) :- !,
   add_args(A, X, I, H, S),
   add_args(B, Y, H, O, S).
add_args(trait(X, P, V), trait(X, P, V, I, O, S), I, O, S) :- !.
add_args(X, X, _, _, _).

Seems to work:

/* Only Self Avoiding Walk (SAW) proof branches */
trait(X, P, V, _, _, S) :- member(G, S), 
    G =@= trait(X, P, V), !, fail.

/* Clauses with cyclic data */
trait(alice, likes, bob).
trait(bob, likes, clara).
trait(clara, likes, bob).
trait(X, trans, Y) :- trait(X, likes, Y).
trait(X, trans, Y) :- trait(X, likes, Z), trait(Z, trans, Y).

/* Query over cyclic data */
?- trait(alice, trans, clara, D, [], []).
D = [(trait(alice, trans, clara):-trait(alice, likes, bob), 
     trait(bob, trans, clara)), 
(trait(bob, trans, clara):-trait(bob, likes, clara))] ;
false.
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.

17

Are you refering to the dif/2 solution? Which could work
in the less common case if all queries and all subgoals were
ground. It creates quadratic many dif/2 constraints:

Many of the dif/2 constraints get triggered when the trait/3
goals get satisfied, slowing it down. dif/2 can also not detect
alpha conversion, i.e. that proving ∃Y P(Y) while proving

∃X P(X) is redundant, so that it has less fast failure properties
and can lead to infinite loops. One can easily check that dif/2
is more permissible, than loop checking with (=@=)/2:

?- \+ p(X) =@= p(Y).
false.

?- dif(p(X), p(Y)).
dif(Y, X).

Another name for alpha conversion is variant term. Tabling can
even do more than only alpha conversion detection, for example
SWI-Prolog has also an option to detect subsumption.

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.

20

Its a difference list, as used in Definite Clause Grammars
(DCG). You can use “threading” of input/output arguments
to collect items, like the clause that was selected, and that

you want to have collected as was done in your original
b_getvat/b_setval derivation. But you could also build
something else, by using a different expansion. Like a

tree for example, instead of a list.