Part 1/2: prove(Goal)

Here is the standard vanilla pure Prolog interpreter:

prove(true) :- !.
prove((A,B)) :- !,prove(A),prove(B).
prove(A) :- clause(A,B),prove(B).

The gist is that any Prolog goal is either of the form Head :- Body, or it is a concatenation of goals. I can recursively parse any given goal down to the form Head :- true, which prove(B) in the final clause will end up resolving against the first clause.

The parser works fine with user defined predicates, but it won’t work with built-ins or optimised predicated which ship with SWI Prolog. That given, ?- prove(Goal). should work just like ?- Goal. for pure Prolog.

The first step is to make prove/1 stochastic, which I do by adding one line to the final clause:

prove(true) :- !.
prove((A,B)) :- !,prove(A),prove(B).
prove(Head) :-
    clause(Head,Body),
    (p(Head,P)->(random(X),1-P<X);true),
    prove(Body).

Whenever the head of a clause is encountered during unification, I check if p/2 applies to it, and if so, I make sure it fails at the rate (1-P) given by p(Head,P).

Part 2/2: sim(Goal,N,P)

The simulator performs a stochastic simulation of the proving process parameterised by the p/2 predicates. It is tantamount to running the prover many times and reporting the success fraction:

sim(_,0,S,S) :- !.
sim(Goal,N0,Acc0,S) :-
    (prove(Goal)->Acc is Acc0+1;Acc is Acc0),
    N is N0-1,
    sim(Goal,N,Acc,S).
sim(Goal,N,P) :-
    sim(Goal,N,0,S),
    P is S/N.

SYNTAX

The interpreter is limited to pure Prolog: no meta predicates, built-ins or “optimised” predicates (e.g. member/2) because they all break clause/2. It is straightforward to expand the coverage of the interpreter, but not necessarily desirable.

Probabilities are assigned using p(Goal,P).

SEMANTICS

p/2 specifies the probability that a clause gets unified during the proof process. Each instance of p/2 is applied independently. Therefore, to interpret the results, the programmer must taken into account both the assigned probabilities and the proof process.

Here is a transitive meeting example to illustrate the point.

meets_(sarah,lucy).
meets_(lucy,steve).
meets_(lucy,kolmogorov).
meets_(steve,chris).
meets_(steve,kolmogorov).
meets_(chris,kolmogorov).
meets(X,Y) :- meets_(X,Y).
meets(X,Y) :- meets_(X,Z),meets(Z,Y).

p(meets_(sarah,_),0.25).
p(meets_(steve,chris),0.5).
p(meets_(_,kolmogorov),0.1).

Who could possibly meet Kolmogorov?

?- setof(X,meets(X,kolmogorov),People).

People = [chris, lucy, sarah, steve].

How likely are they the meet him? The p/2 assignments above should be interpreted as follows:

• P=0.25 of Sarah meeting any particular person.
• P=0.3 of Chris and Steve meeting.
• P=0.1 of Kolmogorov meeting any particular person.

Taking Lucy as an example, she might meet Kolmogorov in 3 ways:

1. Directly, P=0.1.
2. Steve -> Kolmogorov, P=0.1.
3. Steve -> Chris -> Kolmogorov, P=0.5*0.1=0.05.

One may therefore expect P for Lucy meeting Kolmogorov to be \(0.1+0.1+0.05=0.25\), but that is not the case because these assignments are not a partition of all the possibilities:

?- sim(meets(lucy,kolmogorov),10000,P).
P = 0.231071.

What I’m actually approximating is the probability that the prover will be able to unify meets(lucy,kolmogorov) in at least one of the three ways above. The probability of failing to unify is: \[(1-0.1)*(1-0.1)*(1-0.05) = 0.7695\] therefore we should expect sim/3 to converge to \(1-0.7695 = 0.2305\) in the example; just as it does.

Now, look what happens if I assign probabilities to the meets/2 predicate rather than meets_/2:

...
p(meets(sarah,_),0.25).
p(meets(steve,chris),0.5).
p(meets(_,kolmogorov),0.1).

?- sim(meets(lucy,kolmogorov),10000,P).
P = 0.109619.

Certainly not what I want. Restrictions (p/2) on the recursive meets/2 call results in unintuitive backtracking behaviour and ultimately incorrect answers.