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

General
83

I promised an example of the way Meta-Interpretive Learning works so that we have something more concrete to talk about. The following is from my own Meta-Interpretive Learning System, Louise:

58 ?- list_mil_problem(ancestor/2).
Positive examples
-----------------
ancestor(stathis,kostas).
ancestor(stefanos,dora).
ancestor(kostas,stassa).
ancestor(alexandra,kostas).
ancestor(paraskevi,dora).
ancestor(dora,stassa).
ancestor(stathis,stassa).
ancestor(stefanos,stassa).
ancestor(alexandra,stassa).
ancestor(paraskevi,stassa).

Negative examples
-----------------
:-ancestor(kostas,stathis).
:-ancestor(dora,stefanos).
:-ancestor(stassa,kostas).
:-ancestor(kostas,alexandra).
:-ancestor(dora,paraskevi).
:-ancestor(stassa,dora).
:-ancestor(stassa,stathis).
:-ancestor(stassa,stefanos).
:-ancestor(stassa,alexandra).
:-ancestor(stassa,paraskevi).

Background knowledge (First Order)
----------------------------------
parent/2:
parent(stathis,kostas).
parent(stefanos,dora).
parent(kostas,stassa).
parent(alexandra,kostas).
parent(paraskevi,dora).
parent(dora,stassa).

Background knowledge (Second Order)
-----------------------------------
(Identity) ∃.P,Q ∀.x,y: P(x,y)← Q(x,y)
(Tailrec) ∃.P,Q ∀.x,y,z: P(x,y)← Q(x,z),P(z,y)

true.

So what we have here essentially is a higher-order definite program that comes in two parts: one part is a set of first-order definite program clauses, which is basically a Prolog program. The other part is a set of second-order definite program clauses, which we can see as a second-order Prolog program. In practice the second-order program is datalog (no fucntion symbols) but the first-order program is really an unrestricted Prolog program. That’s in practice.

Unlike Prolog we also have two sets of training examples: positive and negative. The “:-” in the negative examples is just a reminder, they’re not meant to be executed as directives!

Now, with the above loaded in memory, we can ask Louise to learn a program:

61 ?- learn(ancestor/2).
ancestor(A,B):-parent(A,B).
ancestor(A,B):-ancestor(A,C),ancestor(C,B).
true.

And as you see it learns a bog-standard ancestor/2 definition based on parent. It’s a left-recursive definition though. So what’s going on here?

The version of Louise I use is the one that is bundled as an example with Vanilla:

Vanilla is a Meta-Interpretive Learning engine. If you navigate to the src/vanilla.pl module you 'll see that the main exported predicate is the called prove; and if you squint a bit and tune out the debug statemetns, you’ll start to discern the good, old, familiar structure of a “vanilla” Prolog meta-interpreter:

prove(true,_K,_MS,_Ss,_Os,Subs,Subs):-
	!
    ,debug(prove_steps,'Reached proof leaf.',[])
	,debug(prove_metasubs,'Metasubs so-far: ~w',[Subs]).
prove((L,Ls),K,MS,Ss,Os,Subs,Acc):-
	debug(prove_steps,'Splitting proof at literals ~w -- ~w',[L,Ls])
	,prove(L,K,MS,Ss,Os,Subs,Subs_)
	,prove(Ls,K,MS,Ss,Os,Subs_,Acc).
prove((L),K,MS,Ss,Os,Subs,Acc):-
     L \= (_,_)
	,L \= true
    ,debug(prove_steps,'Proving literal: ~w.',[L])
	,clause(Os,L,K,MS,Ss,Subs,Subs_,Ls)
	,debug(prove_metasubs,'New Metasubs: ~w',[Subs_])
    ,debug(prove_steps,'Proving body literals of clause: ~w',[L:-Ls])
    ,prove(Ls,K,MS,Ss,Os,Subs_,Acc).

That’s what’s doing the learning! It’s a Prolog meta-interpreter. It’s equipped with a few extra arguments, mainly for book-keeping and for depth-limiting. Taking the arguments one by one from the left:

  • The stack of literals (L,Ls) is the set of positive examples.
  • K is an upper limit on the number of substitutions in Subs, effectively limiting the number of clauses that can be added to a learning program.
  • MS is a list of Second-Order Definite Clauses from the Second-Order Background Knowledge (we don’t write those to the dynamic database).
  • Ss is a set of predicate symbols, that include the predicate symbols in the positive examples and the first-order background knowledge, and may include one or more invented predicate symbols (those are predicates that are not defined either in the background knowledge or the examples).
  • Os is a list of options.
  • Subs is an accumulator of substitutions of second-order variables in the Second-Order Background Knowledge.
  • The final argument is the “binder” variable that binds to the accumulator of second-order substitutions when the proof succeeds.

In the third clause of the prove/6 meta-interpreter, where you expect to find a call to clause/2, there’s this call to a predicate clause/8 instead:

,clause(Os,L,K,MS,Ss,Subs,Subs_,Ls)

This is a variant of clause/2 that allows fetching of the bodies of clauses not only from the first-order background knowledge, but also two other sets of clauses:

a) the second-order clauses stored in MS, and,
b) the substitutions of the second-order variables in MS, stored in Subs.

When a clause, M, is fetched from MS, then L, the literal we are trying to prove, is bound to the head of M and then the body literals of M (with some of their variables now bound by unification) are placed on top of the meta-interpreter stack and the proof continues.

When a substitution S is fetched from Subs, first it is expanded to a full clause by unification with the corresponding second-order clause in MS, and then its head is unified with L and its body placed on the meta-interpreter stack for the proof to continue.

So what this meta-interpreter is doing is carrying out an SLD-Resolution proof of the positive examples with both first- and second-order definite program clauses, and also with the clauses of a program that is being learned, as it is being learned.

There are two dangerous situations here that can cause infinite recursion:

a) A second-order definite clause in MS can infinitely resolve with itself.
b) A first-order definite clause expanded from a substitution in Subs can infinitely recurse with itself or another clause expanded from Subs.

To avoid the first danger, infinite self-recursion of second-order definite clauses, the argument K is used to limit the length of Subs. That happens in clause/8 and it stops infinite self-resolution.

To avoid the second danger, Vanilla uses two methods.

The first method is tabling. prove/6 can be tabled by switching a flag on or off, like I described above. When the flag is on, prove/6 will happily prove left-recursive programs like the ancestor/2 version I list above.

The second method is to prevent clause/8 from fetching clauses from the expanded substitutions in Subs. This is done with a flag in a configuration file. At that point we can also safely turn off tabling.

What happens if we switch the flag that fetches clauses from Subs and turn tabling off? This is what happens:

63 ?- learn(ancestor/2).
ancestor(A,B):-parent(A,B).
ancestor(A,B):-parent(A,C),ancestor(C,B).
true.

So now Louise learns a recursive definition of ancestor/2 but not a left-recursive one. This is the effect of the combination of depth-limiting provided by the argument K of prove/6 and the fact that the program we’re learning can’t resolve with itself until it’s fully learned.

OK. That’s a lot to take in and you have work to do, but I hope it helps better understand how Meta-Interpretive Learning works and why I don’t think it’s possible to apply the call-graph method you suggested. I also hope it explains where the depth limits and tabling come in.

I haven’t explained the use of negative examples, and how predicate invention works, to keep things short…er. Ask me if you are curious to know, I’m happy to explain.

Oh and, I forget to say: Happy Easter to those who celebrate it. I’m Greek so our Easter is later :slight_smile: